内涵性、内涵递归与 Gödel-Löb 公理

在类型化 $\lambda$-演算中使用必然性模态可以将其划分为两个区域。这可以被视为内涵数据与外延数据之分：第一个区域（模态区域）中的数据可作为代码获取，并且可以检查其描述。相比之下，第二个区域中的数据仅作为值按普通相等关系获取。这使我们能够在模态类型上添加非函数操作，同时保持一致性。在此背景下，Gödel-Löb 公理获得了一种新颖的构造性解读：它为程序员提供了一种非常强大的递归可能性，使其能够编写可访问自身代码的程序。这是一种计算反射，强烈地让人联想到 Kleene 第二递归定理。