Type inhabitation: Difference between revisions
No edit summary |
GreenC bot (talk | contribs) Move 1 url. Wayback Medic 2.5 |
||
| Line 1: | Line 1: | ||
In [[type theory]], a branch of [[mathematical logic]], in a given typed calculus, the '''type inhabitation problem''' for this calculus is the following problem:<ref>{{cite journal |title=Inhabitation in Typed Lambda-Calculi (A Syntactic Approach) |author=Pawel Urzyczyn |journal=Lecture Notes in Computer Science |pages=373–389 |year=1997 |publisher=Springer |url= |
In [[type theory]], a branch of [[mathematical logic]], in a given typed calculus, the '''type inhabitation problem''' for this calculus is the following problem:<ref>{{cite journal |title=Inhabitation in Typed Lambda-Calculi (A Syntactic Approach) |author=Pawel Urzyczyn |journal=Lecture Notes in Computer Science |pages=373–389 |year=1997 |publisher=Springer |url=https://doi.org/10.1007%2F3-540-62688-3_47}}</ref> given a type <math>\tau</math> and a [[typing environment]] <math>\Gamma</math>, does there exist a <math>\lambda</math>-term M such that <math>\Gamma \vdash M : \tau</math>? With an empty type environment, such an M is said to be an inhabitant of <math>\tau</math>. |
||
== Relationship to logic == |
== Relationship to logic == |
||
Revision as of 04:31, 13 February 2020
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
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
- ^ Pawel Urzyczyn (1997). "Inhabitation in Typed Lambda-Calculi (A Syntactic Approach)". Lecture Notes in Computer Science. Springer: 373–389.
This programming language theory or type theory-related article is a stub. You can help Wikipedia by expanding it. |
