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

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

Zhibo Chen, Frank Pfenning · FoSSaCS · 2023 · logical-frameworks · DOI

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.

Cite

Cite as @chen-2023-a (helia, typst) · \cite{chen-2023-a} (LaTeX)

BibTeX

bibtex · 1 line

@inbook{chen-2023-a, title={A Logical Framework with Higher-Order Rational (Circular) Terms}, ISBN={9783031308291}, ISSN={1611-3349}, url={http://dx.doi.org/10.1007/978-3-031-30829-1_4}, DOI={10.1007/978-3-031-30829-1_4}, booktitle={Foundations of Software Science and Computation Structures}, publisher={Springer Nature Switzerland}, author={Chen, Zhibo and Pfenning, Frank}, year={2023}, pages={68–88} }

hayagriva YAML (typst)

yaml · 17 lines

chen-2023-a:
  type: chapter
  title: A Logical Framework with Higher-Order Rational (Circular) Terms
  author:
  - Chen, Zhibo
  - Pfenning, Frank
  date: 2023
  page-range: 68-88
  url: http://dx.doi.org/10.1007/978-3-031-30829-1_4
  serial-number:
    doi: 10.1007/978-3-031-30829-1_4
    isbn: '9783031308291'
    issn: 1611-3349
  parent:
    type: book
    title: Foundations of Software Science and Computation Structures
    publisher: Springer Nature Switzerland

Download: chen-2023-a.bib · chen-2023-a.yml

Cited by (1)

A Saturation-Based Unification Algorithm for Higher-Order Rational Patterns chen-2024-aTOCL · 2024

Higher-order unification has been shown to be undecidable. Miller discovered the pattern fragment and subsequently showed that higher-order pattern unification is decidable and has most general unifiers. We extend the algorithm to higher-order rational terms (a.k.a. regular Böhm trees, a form of cyclic λ-terms) and show that pattern unification on higher-order rational terms is decidable and has most general unifiers. We prove the soundness and completeness of the algorithm.

DOI · arXiv

Cites 29 works (1 here)

With notes (1)

A linear logical framework cervesato-nd-aLICS

DOI

External (28)

Polarized Subtyping (2022)
Towards a mixed inductive and coinductive logical framework (Tech. Rep. CMU-CS-21-144) (2021)
Mixed Inductive-Coinductive Reasoning: Types, Programs and Logic (PhD thesis) (2018)
On Subtyping-Relation Completeness, with an Application to Iso-Recursive Types (2017)
Cuts for circular proofs: Semantics and cut-elimination (2013)
On equal μ -terms (2011)
Sequent calculi for induction and infinite descent (2010)
Subtyping, Declaratively (2010)
Theory of finite or infinite trees revisited (2008)
Mechanizing metatheory in a logical framework (2007)
Extending logic programming with coinduction (PhD thesis) (2006)
Cyclic Proofs for First-Order Logic with Inductive Definitions (2005)
On equivalence and canonical forms in the LF type theory (2005)
A proof theory for generic judgments (2005)
A Concurrent Logical Framework II: Examples and Applications (2003)
A Concurrent Logical Framework I: Judgments and Properties (2003)
Coinductive Axiomatization of Recursive Type Equality and Subtyping (1998)
The Horn mu-calculus (1998)
Regular Böhm trees (1998)
Algorithms for Equality and Unification in the Presence of Notational Definitions (1998)
Twelf User's Guide, 1.2 edition (1998)
Cyclic lambda calculi (1997)
Lambda Calculus with Explicit Recursion (1997)
Subtyping recursive types (1993)
A Framework for Defining Logics (1993)
A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification (1991)
The Lambda Calculus: Its Syntax and Semantics (1985)
Fundamental properties of infinite trees (1983)