Products and Polymorphic Subtypes

Abstract

This paper is devoted to a comprehensive study of polymorphic subtypes with products. We first present a sound and complete Hilbert style axiomatization of the relation of being a subtype in presence of →, × type constructors and the ∀ quantifier, and we show that such axiomatization is not encodable in the system with →,∀ only. In order to give a logical semantics to such a subtyping relation, we propose a new form of a sequent which plays a key role in a natural deduction and a Gentzen style calculi. Interestingly enough, the sequent must have the form E⊢T, where E is a non-commutative, non-empty sequence of typing assumptions and T is a finite binary tree of typing judgements, each of them behaving like a pushdown store. We study basic metamathematical properties of the two logical systems, such as subject reduction and cut elimination. Some decidability/undecidability issues related to the presented subtyping relation are also explored: as expected, the subtyping over →,×,∀ is undecidable, being already undecidable for the →,∀ fragment (as proved in [15]), but for the ×,∀ fragment it turns out to be decidable.