[Submit a comment] [RTALooP home] [Index] [Previous] [Next]

[Postscript] [PDF] [BibTeX Source] [LaTeX Source]

Problem #4 (Solved !)

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].

Remark

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 σ.

References

[Bar91]

Henk Barendregt. Lambda calculi with types. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science. Oxford University Press, Oxford, 1991. To appear.

[Hue90]

Gérard Huet, editor. Logical Foundations of Functional Programming. University of Texas at Austin Year of Programming. Addison-Wesley, Reading, MA, 1990.

[Wel94]

Joe B. Wells. Typability and type checking in the second-order λ-calculus are equivalent and undecidable. In Samson Abramsky, editor, Ninth Symposium on Logic in Computer Science, Paris, France, July 1994. IEEE.

[Submit a comment] [RTALooP home] [Index] [Previous] [Next]

[Postscript] [PDF] [BibTeX Source] [LaTeX Source]