合成守卫域理论中递归类型的指称语义

正如数学的任何其他分支一样，编程语言的指称语义应当在类型论中形式化，但将传统域论语义——最初在经典集合论中表述——适配到类型论已被证明颇具挑战。本文是在带有守卫递归的类型论中表述指称语义项目的一部分。其益处不仅在于给出更简单的语义及诸如充分性之类的性质证明，而且有望在未来扩展到具有高级特性（如通用引用）的语言，而这是传统域论技术所不及的。在守卫依赖类型论（GDTT）中，我们为 FPC（扩展了递归类型的简单类型 lambda 演算）开发了指称语义，使用 GDTT 的守卫递归类型来建模 FPC 的递归类型。我们利用同样使用守卫递归类型构造的语法与语义之间的逻辑关系，在 GDTT 中证明了模型的可靠性和计算充分性。该指称语义是内涵性的，在于它计数了计算一个项的值所需的解折叠-折叠归约次数，但我们构造了一个关系将外延相等项的指称相关联，即那些以不同步数计算出相同值的项对。最后我们展示了如何在类型论内执行项的指称语义，并证明执行一个布尔项的指称所计算的值与 FPC 的操作语义相同。