类型居留问题

在简单类型lambda演算中，类型居留问题是如下问题: 给定一个类型τ，是否存在一个λ-项 M 使得对于某个类型环境γ有Γ M：τ? 如果回答是肯定的，则 M 被称为τ的居所。因为在简单类型的 lambda 演算中类型对应于极小蕴涵逻辑(参见Curry-Howard同构)，一个类型有一个居所，当且仅当它是极小蕴涵逻辑的重言式。在简单类型lambda演算中，类型居留问题是如下问题: 给定一个类型τ，是否存在一个λ-项 M 使得对于某个类型环境γ有 ? 如果回答是肯定的，则 M 被称为τ的居所。