论文标题
具有高阶合理（圆形）项的逻辑框架
A Logical Framework with Higher-Order Rational (Circular) Terms
论文作者
论文摘要
逻辑框架在演绎系统中提供了自然和直接的指定和推理方式。逻辑框架LF和随后的发展集中在限制性证明系统上，使这种逻辑框架中循环证明系统的形式化成为笨拙而尴尬的任务。为了解决这个问题，我们提出了COLF，这是LF的保守扩展，具有高阶合理术语以及混合的归纳和共同定义。在此框架中，如果两个术语展开到同一无限的常规Böhm树，则两个术语相等。术语平等和类型检查在COLF中都是可决定的。我们通过几个小案例研究来说明框架的优雅和表现力。
Logical frameworks provide natural and direct ways of specifying and reasoning within deductive systems. The logical framework LF and subsequent developments focus on finitary proof systems, making the formalization of circular proof systems in such logical frameworks a cumbersome and awkward task. To address this issue, we propose CoLF, a conservative extension of LF with higher-order rational terms and mixed inductive and coinductive definitions. In this framework, two terms are equal if they unfold to the same infinite regular Böhm tree. Both term equality and type checking are decidable in CoLF. We illustrate the elegance and expressive power of the framework with several small case studies.
