类型居留问题

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

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

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

这是一篇與逻辑学相關的小作品。您可以通过编辑或修订扩充其内容。 查 论 编