Problem # 14

[Next] [Previous] [Up]

Problem # 14

Submitted by Simona Ronchi Della Rocca
Date: 1994
Statement. For every $n$ , determine the set of terms which can be typed in the stratiﬁed polymorphic type assignment system of order $n$ . $\text{[math]}$
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 $n ≥ 0$ is obtained by restricting the rule for eliminating the universal quantiﬁer in the following way:

Γ ⊢ M : ∀ α.σ the level of α in σ is ≤ n ---n--------------------------------------- Γ ⊢n M : σ[τ∕α]

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 $0$ ;
the level of $α$ in $α$ is $1$ ;
the level of $α$ in $∀β.τ$ is the level of $α$ in $τ$ ;
the level of $α$ in $τ1 → τ2$ is $max{n1, n2}+ 1$ , where $n1$ and $n2$ are respectively the levels of $α$ in $τ 1$ and $τ 2$ respectively.

It turns out that $⊢ 0$ has the same typing power of the Curry type assignment system, and $⊢1$ assigns types to all and only the normal forms. Find a characterization of the set of terms typable in the system indexed by $n$ , for $n ≥ 2$ .

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