查看“︁类型居留问题”︁的源代码

在[[简单类型lambda演算]]中，'''类型居留（Type inhabitation）'''问题是如下问题：给定一个类型 <math>\tau</math>，是否存在一个 <math>\lambda</math>-项 M 使得对于某个类型环境 <math>\Gamma</math> 有 <math>\Gamma \vdash M : \tau</math>？在空的类型环境中，如果回答是肯定的，则 M 被称为 <math>\tau</math> 的居留元（inhabitant）。

因为在简单类型的 lambda 演算中类型对应于极小蕴涵逻辑(参见 [[Curry-Howard同构|Curry-Howard 同构]])，一个类型有一个居留元，当且仅当它是极小蕴涵逻辑的重言式。

[[Richard Statman]] 证明了在简单类型λ演算中类型居留问题是 [[PSPACE-完全性]]的。

{{logic-stub}}
[[Category:Lambda演算]]
[[Category:类型论]]