Affiliations: Dipartimento di Informatica, Università di Torino,
c. Svizzera 185, 10149 Torino, Italy | Institute of Informatics, Warsaw University, ul.
Banacha 2, 02-097 Warsaw, Poland
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.
