[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 stratified polymorphic type assignment system of order n  .
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], defined a complete stratification of the polymorphic type assignment system for λ  -calculus, indexed by integers. The stratification of order n ≥ 0  is obtained by restricting the rule for eliminating the universal quantifier in the following way:

Γ ⊢  M  : ∀ α.σ  the level of α in σ is ≤ n
---n---------------------------------------
             Γ ⊢n M  : σ[τ∕α]
where the level of a variable in a type is defined as follows:

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 stratification of the polymorphic type discipline. Information and Computation, 110:115 – 173.


[Next]  [Previous]  [Up]  
© 2006 Dip. Informatica - Universita di Torino
Last modified: July 21, 2014