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:{{cite book |author=Pawel Urzyczyn |title=Typed Lambda Calculi and Applications |chapter=Inhabitation in typed lambda-calculi (A syntactic approach) |series=Lecture Notes in Computer Science |pages=373–389 |year=1997 |volume=1210 |publisher=Springer |doi=10.1007/3-540-62688-3_47 |isbn=978-3-540-62688-6 |chapter-url=https://doi.org/10.1007%2F3-540-62688-3_47}} 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
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
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.{{Cite book |last1=Sørensen |first1=Morten Heine |url=https://disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard.pdf |title=Lectures on the Curry-Howard Isomorphism |last2=Urzyczyn |first2=Pawel |date=2006 |publisher=Elsevier Science & Technology |isbn=978-0-08-047892-0 |edition=1 |series=Studies in Logic and the Foundations of Mathematics Ser |location=Oxford |archive-url=https://web.archive.org/web/20250314135009/http://disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard.pdf |archive-date=2025-03-14 |url-status=live}}