In type theory, a branch of mathematical logic, in a given typed calculus, the type inhabitation problem for this calculus is the following problem: given a type <math>\tau</math> and a type 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>.
| Property | Value |
|---|
| dbpprop:abstract
|
- In type theory, a branch of mathematical logic, in a given typed calculus, the type inhabitation problem for this calculus is the following problem: given a type <math>\tau</math> and a type 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>.
|
| rdfs:comment
|
- In type theory, a branch of mathematical logic, in a given typed calculus, the type inhabitation problem for this calculus is the following problem: given a type <math>\tau</math> and a type 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>.
|
| rdfs:label
| |
| skos:subject
| |
| foaf:page
| |
| is dbpprop:redirect
of | |
![[RDF Data]](/statics/sw-cube.png)
