类型居留问题

维基百科,自由的百科全书
跳到导航 跳到搜索

简单类型lambda演算中,类型居留(Type inhabitation)问题是如下问题:给定一个类型 ,是否存在一个 -项 M 使得对于某个类型环境 ?在空的类型环境中,如果回答是肯定的,则 M 被称为 的居留元(inhabitant)。

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

Richard Statman 证明了类型居留问题是 PSPACE-完全性的。