类型栖息
编辑在类型理论（数理逻辑的一个分支）中，在一个给定的类型微积分中，这个微积分的类型栖息问题是如下问题：给定一个类型
与逻辑的关系
编辑在简单类型的λ微积分中，当且仅当一个类型的相应命题是最小隐含逻辑的同义反复时，它才有一个居民。同样地，当且仅当一个系统F类型的相应命题是直觉二阶逻辑的同义反复时，它才有一个居民。吉拉德悖论表明，类型的栖息地与具有库里-霍华德对应关系的类型系统的一致性密切相关。为了健全，这样的系统必须有无人居住的类型。
形式属性
编辑对于大多数类型计算，类型驻留问题是非常困难的。对于其他计算体，该问题甚至是不可解的。
内容由匿名用户提供，本内容不代表vibaike.com立场，内容投诉举报请联系vibaike.com客服。如若转载，请注明出处：https://vibaike.com/170868/