Type inhabitation problem

From Wikipedia, the free encyclopedia

In simply typed lambda calculus, the type inhabitation problem is the following problem: given a type $τ$ , does there exist a $λ$ -term M such that $\Gamma \vdash M : \tau$ for some type environment $Γ$ ? If the answer is positive, M is said to be an inhabitant of $τ$ .

Since types in simply typed lambda calculus correspond to formulae of minimal implicative logic (see Curry-Howard isomorphism), a type has an inhabitant if and only if it is a tautology of minimal implicative logic.

Richard Statman proved that the type inhabitation problem is PSPACE-complete.