[Next] [Previous] [Up]

#### Problem # 14

Submitted by Simona Ronchi Della Rocca

Date: 1994

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

[PRINT this PROBLEM]

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:

where the level of a variable in a type is deﬁned as follows:
- if does not occur free in , then the level of in is ;
- the level of in is ;
- the level of in is the level of in ;
- the level of in is , where and
are respectively the levels of in and respectively.

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
.

##### References for # 14

[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.

[Next] [Previous] [Up]

Last modified: July 21, 2014