Submitted by Simona Ronchi Della Rocca
Statement. For every , determine the set of terms which can be typed in the stratiﬁed polymorphic type assignment system of order .
Problem Origin. First posed by Paola Giannini and Simona Ronchi Della Rocca
Giannini and Ronchi Della Rocca, in [Giannini and Ronchi Della Rocca, 1994], deﬁned a complete stratiﬁcation of the polymorphic type assignment system for -calculus, indexed by integers. The stratiﬁcation of order is obtained by restricting the rule for eliminating the universal quantiﬁer in the following way:
It turns out that has the same typing power of the Curry type assignment system, and assigns types to all and only the normal forms. Find a characterization of the set of terms typable in the system indexed by , for .
[Giannini and Ronchi Della Rocca, 1994] Giannini, P. and Ronchi Della Rocca, S. (1994). A type inference algorithm for a complete stratiﬁcation of the polymorphic type discipline. Information and Computation, 110:115 – 173.