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 τ {\displaystyle \tau } and a typing environment Γ {\displaystyle \Gamma } , does there exist a λ {\displaystyle \lambda } -term M such that Γ ⊢ M : τ {\displaystyle \Gamma \vdash M:\tau } ? With an empty type environment, such an M is said to be an inhabitant of τ {\displaystyle \tau } .
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 τ {\displaystyle \tau } and a typing environment Γ {\displaystyle \Gamma } , does there exist a λ {\displaystyle \lambda } -term M such that Γ ⊢ M : τ {\displaystyle \Gamma \vdash M:\tau } ? With an empty type environment, such an M is said to be an inhabitant of τ {\displaystyle \tau } .
Source: Wikipedia "Type inhabitation" · CC BY-SA 4.0
Share this article: X · Bluesky