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