Problem # 5

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

[PRINT this PROBLEM]

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]

Last modified: July 21, 2014