Type inhabitation

In type theory, a branch of mathematical logic, in a given typed calculus, the type inhabitation problem for this calculus is the following problem:[1] given a type \tau and a typing environment \Gamma, does there exist a \lambda-term M such that \Gamma \vdash M : \tau? With an empty type environment, such an M is said to be an inhabitant of \tau.

Relationship to logic

In the case of simply typed lambda calculus, a type has an inhabitant if and only if its corresponding proposition is a tautology of minimal implicative logic. Similarly, a System F type has an inhabitant if and only if its corresponding proposition is a tautology of second-order logic.

Formal properties

For most typed calculi, the type inhabitation problem is very hard. Richard Statman proved that for simply typed lambda calculus the type inhabitation problem is PSPACE-complete. For other calculi, like System F, the problem is even undecidable.

See also

References

  1. Pawel Urzyczyn (1997). "Inhabitation in Typed Lambda-Calculi (A Syntactic Approach)" (PDF). Lecture Notes in Computer Science (Springer): 373–389.


This article is issued from Wikipedia - version of the Wednesday, October 16, 2013. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.