类型居留问题, 在简单类型lambda演算中, 类型居留, type, inhabitation, 问题是如下问题, 给定一个类型, displaystyle, 是否存在一个, displaystyle, lambda, 使得对于某个类型环境, displaystyle, gamma, displaystyle, gamma, vdash, 在空的类型环境中, 如果回答是肯定的, 被称为, displaystyle, 的居留元, inhabitant, 因为在简单类型的, lambda, 演算中类型对应于极小蕴涵逻. 在简单类型lambda演算中 类型居留 Type inhabitation 问题是如下问题 给定一个类型 t displaystyle tau 是否存在一个 l displaystyle lambda 项 M 使得对于某个类型环境 G displaystyle Gamma 有 G M t displaystyle Gamma vdash M tau 在空的类型环境中 如果回答是肯定的 则 M 被称为 t displaystyle tau 的居留元 inhabitant 因为在简单类型的 lambda 演算中类型对应于极小蕴涵逻辑 参见 Curry Howard 同构 一个类型有一个居留元 当且仅当它是极小蕴涵逻辑的重言式 Richard Statman 证明了在简单类型l演算中类型居留问题是 PSPACE 完全性的 这是一篇與逻辑学相關的小作品 你可以通过编辑或修订扩充其内容 查论编 取自 https zh wikipedia org w index php title 类型居留问题 amp oldid 74303867, 维基百科,wiki,书籍,书籍,图书馆,