# Type inhabitation

From Wikipedia the free encyclopedia

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 and a typing environment , does there exist a -term M such that ? With an empty type environment, such an M is said to be an inhabitant of .

## Relationship to logic[edit]

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 intuitionistic second-order logic.

Girard's paradox shows that type inhabitation is strongly related to the consistency of a type system with Curry–Howard correspondence. To be sound, such a system must have uninhabited types.

## Formal properties[edit]

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[edit]

## References[edit]

**^**Pawel Urzyczyn (1997). "Inhabitation in typed lambda-calculi (A syntactic approach)".*Typed Lambda Calculi and Applications*. Lecture Notes in Computer Science. Vol. 1210. Springer. pp. 373–389. doi:10.1007/3-540-62688-3_47. ISBN 978-3-540-62688-6.