[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |
Originator:
Date: April 1991
Summary: Is it decidable whether a term is is typable in the second-order λ 2 calculus?
One of the outstanding open problems in typed lambda calculi is the following: Given a term in ordinary untyped lambda calculus, is it decidable whether it can be typed in the second-order λ 2 calculus? See [Bar91][Hue90].
This question has been solved in the negative. In [Wel94] J.B. Wells proves that given a closed, type-free lambda term, the question whether it is typable in second-order λ 2 calculus, is undecidable. Moreover, given a closed type-free lambda term M and a type σ, then it is also undecidable in second-order λ 2 calculus whether M has type σ.
[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |