A Saturation-Based Unification Algorithm for Higher-Order Rational Patterns

Reference. A Saturation-Based Unification Algorithm for Higher-Order Rational Patterns

Zhibo Chen, Frank Pfenning · TOCL · 2024 · unification · DOI · arXiv

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.

Cite

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

BibTeX

bibtex · 1 line

@article{chen-2024-a, title={A Saturation-Based Unification Algorithm for Higher-Order Rational Patterns}, volume={26}, ISSN={1557-945X}, url={http://dx.doi.org/10.1145/3704265}, DOI={10.1145/3704265}, number={1}, journal={ACM Transactions on Computational Logic}, publisher={Association for Computing Machinery (ACM)}, author={Chen, Zhibo and Pfenning, Frank}, year={2024}, month=Dec, pages={1–33} }

hayagriva YAML (typst)

yaml · 18 lines

chen-2024-a:
  type: article
  title: A Saturation-Based Unification Algorithm for Higher-Order Rational Patterns
  author:
  - Chen, Zhibo
  - Pfenning, Frank
  date: 2024-12
  page-range: 1-33
  url: http://dx.doi.org/10.1145/3704265
  serial-number:
    doi: 10.1145/3704265
    issn: 1557-945X
  parent:
    type: periodical
    title: ACM Transactions on Computational Logic
    publisher: Association for Computing Machinery (ACM)
    issue: 1
    volume: 26

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

Cites 24 works (2 here)

With notes (2)

A Logical Framework with Higher-Order Rational (Circular) Terms chen-2023-aFoSSaCS · 2023

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.

DOI

System Description: Twelf — A Meta-Logical Framework for Deductive Systems pfenning_schrmann_1999CADE · 1999

DOI

External (22)

Nominal Unification and Matching of Higher Order Expressions with Recursive Let (2022)
Circular proofs as session-typed processes: A local validity condition (2019)
Well-founded recursion with copatterns and sized types (2016)
Cuts for circular proofs: Semantics and cut-elimination (2013)
Sequent calculi for induction and infinite descent (2011)
Subtyping, Declaratively (2010)
Nominal Unification Revisited (2010)
Representations of stream processors using nested fixed points (2009)
Efficient intuitionistic theorem proving with the polarized inverse method (2009)
Lecture Notes on Unification (2006)
Nominal unification (2004)
A Coverage Checking Algorithm for LF (2003)
Regular Böhm trees (1998)
Cyclic lambda calculi (1997)
Saturation-based theorem proving (abstract) (1996)
A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification (1991)
Efficient unification over infinite terms (1984)
An Efficient Unification Algorithm (1982)
Proving termination with multiset orderings (1979)
A unification algorithm for typed λ-calculus (1975)
The undecidability of unification in third order logic (1973)
A Machine-Oriented Logic Based on the Resolution Principle (1965)