将通用判断与递归定义相结合
摘要：编程语言的语义方面，例如它们的操作语义和类型分配计算，通过描述适当的证明系统来进行规定。最近的研究发现了两个证明论特性，可以直接基于逻辑进行关于这些描述的推理：将原子判断作为固定点（递归定义）处理和通过通用判断对绑定结构进行编码。然而，迄今为止包含这两个特性的逻辑将它们视为正交的：也就是说，它们不能提供定义本质上依赖于绑定处理的目标逻辑属性的能力。我们在直觉主义逻辑中，通过对自然数的归纳进行增强，提出了这些特性的新而简单的整合方法，并且我们证明了结果逻辑的一致性。整合的关键优势在于它不仅允许递归定义编码简单传统形式的原子判断，还可以捕捉与此类判断有关的通用属性。通过展示它如何提供优雅的处理涉及类型分配计算的证明中出现的目标逻辑上下文以及在可约性论证中起到作用的任意级联替换，来说明这种逻辑的实用性。
作者：Andrew Gacek, Dale Miller, and Gopalan Nadathur
论文ID：0802.0865
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2008-04-14