[Next]  [Previous]  [Up]  

Problem # 12

Submitted by Paweł Urzyczyn
Date: 1993
Statement. Does the typability hierarchy of F ω  collapse on F1   ?


The type assignment system Fω  can be split into an infinite hierarchy of subsystems Fn  (see [Girard, 1986]), where F0   is the usual polymorphic lambda-calculus (system F  ), and F
 n  admits constructors of order n  . (A type is a constructor of order zero, a constructor of order one is a function acting on types, and a constructor of order n + 1  has arguments of order n  .) It is conjectured [Urzyczyn, 1997] that every pure lambda-term typable in F ω  is typable already in F1   .

Remark: An incorrect proof of the conjecture appeared in [Malecki, 1997].

References for # 12

[Girard, 1986]    Girard, J.-Y. (1986). The system F of variable types, fifteen years later. Theoretical Computer Science, 45:159–192.

[Malecki, 1997]    Malecki, S. (1997). Proofs in system Fω  can be done in system Fω1  . In van Dalen, D. and Bezem, M., editors, Computer Science Logic, volume 1258 of Lecture Notes in Computer Science, pages 297–315. Springer-Verlag.

[Urzyczyn, 1997]    Urzyczyn, P. (1997). Type reconstruction in Fω  . Mathematical Structures in Computer Science, 7(4):329–358.

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