B"ohm树理论和Sall''e猜想中的外延程度
摘要：B"ohm树间的外延等式将无类型λ演算的主要观察等价性进行了表征。众所周知，通过将头范式作为可观察项，得到的λ理论H*在菲范树相等的情况下等同于两个λ项，菲范树可以进行可数次可能无限eta扩展。类似地，在莫里斯的原始观察理论H+中，通过将β范式作为可观察项，只要两个λ项的菲范树在有限的可数次eta扩展下相等，它们就相等。 λ演算还具有一种强的外延性概念，称为“ω规则”，该规则已经成为许多研究的主题。将B"ohm树的理论在ω规则下进行封闭所得到的等价关系B-ω是否严格包含在H+中，一直是一个悬而未决的问题，这个问题起初是由Sall''e在七十年代提出的猜想。在本文中，我们证明了这两个之前提到的理论实际上是相等的，从而证明了Sall''e的猜想是错误的。 我们为证明后一种包含关系开发的证明技术足够通用，可以作为副产品为B"ohm树之间的最小外延等式提供了一种新的基于有界eta扩展的表征。综合这些结果，我们在B"ohm树理论中提供了不同的外延度的分类。
作者：Benedetto Intrigila and Giulio Manzonetto and Andrew Polonsky
论文ID：1802.07320
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22