A Logical Framework with Higher-Order Rational (Circular) Terms

TL;DR

This paper introduces CoLF, an extension of the logical framework LF that incorporates higher-order rational terms, enabling natural formalization of circular proof systems with decidable equality and type checking.

Contribution

It presents CoLF, a novel logical framework with higher-order rational terms and mixed inductive and coinductive definitions, facilitating circular proof formalization.

Findings

Term equality and type checking are decidable in CoLF.

CoLF can express circular proof systems naturally.

Case studies demonstrate the framework's elegance and expressive power.

Abstract

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\"ohm 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.