[Next]  [Previous]  [Up]  

Problem # 5

Submitted by Paweł Urzyczyn
Date: 1993
Statement. Are there terms untypable in Fω  but typable with help of positive recursive types?


Consider an extension of simply typed lambda-calculus obtained by adding the construct μp τ  for types τ  containing only positive occurrences of p  , together with the rules:

Γ-⊢-M--: τ[p:=μp-τ-]              ---Γ-⊢-M--: μp-τ---
   Γ ⊢ M  : μp τ                  Γ ⊢ M  : τ[p:= μpτ ]
This system can assign types for terms untypable in F, e.g. the combinator 22K is typable, where 2 is the Church numeral [Urzyczyn, 1996]. Are there terms typable in this system that cannnot be typed in F
  ω  ? Note that 22K can be typed in Fω   [Urzyczyn, 1997]. Note also that λx.xx  , easily typable in system F, is clearly untypable with positive recursive types.

References for # 5

[Urzyczyn, 1996]    Urzyczyn, P. (1996). Positive recursive type assignment. Fundamenta Informaticae, 28(1-2):197–209.

[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