In
type theory
In mathematics, logic, and computer science, a type theory is the formal presentation of a specific type system, and in general type theory is the academic study of type systems. Some type theories serve as alternatives to set theory as a fou ...
, a branch of
mathematical logic
Mathematical logic is the study of formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of formal ...
, in a given typed calculus, the type inhabitation problem for this calculus is the following problem:
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
The simply typed lambda calculus (\lambda^\to), a form
of type theory, is a typed interpretation of the lambda calculus with only one type constructor (\to) that builds function types. It is the canonical and simplest example of a typed lambda c ...
, a type has an inhabitant if and only if its
corresponding proposition is a
tautology of minimal implicative logic. Similarly, a
System F
System F (also polymorphic lambda calculus or second-order lambda calculus) is a typed lambda calculus that introduces, to simply typed lambda calculus, a mechanism of universal quantification over types. System F formalizes parametric polymorph ...
type has an inhabitant if and only if its
corresponding proposition is a tautology of
intuitionistic
In the philosophy of mathematics, intuitionism, or neointuitionism (opposed to preintuitionism), is an approach where mathematics is considered to be purely the result of the constructive mental activity of humans rather than the discovery of f ...
second-order logic
In logic and mathematics, second-order logic is an extension of first-order logic, which itself is an extension of propositional logic. Second-order logic is in turn extended by higher-order logic and type theory.
First-order logic quantifies on ...
.
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
Hard may refer to:
* Hardness, resistance of physical materials to deformation or fracture
* Hard water, water with high mineral content
Arts and entertainment
* ''Hard'' (TV series), a French TV series
* Hard (band), a Hungarian hard rock supe ...
.
Richard Statman proved that for
simply typed lambda calculus
The simply typed lambda calculus (\lambda^\to), a form
of type theory, is a typed interpretation of the lambda calculus with only one type constructor (\to) that builds function types. It is the canonical and simplest example of a typed lambda c ...
the type inhabitation problem is
PSPACE-complete In computational complexity theory, a decision problem is PSPACE-complete if it can be solved using an amount of memory that is polynomial in the input length (polynomial space) and if every other problem that can be solved in polynomial space can b ...
. For other calculi, like
System F
System F (also polymorphic lambda calculus or second-order lambda calculus) is a typed lambda calculus that introduces, to simply typed lambda calculus, a mechanism of universal quantification over types. System F formalizes parametric polymorph ...
, the problem is even
undecidable.
See also
*
Curry–Howard isomorphism
References
Lambda calculus
Type theory
{{type-theory-stub