A Saturation-Based Unification Algorithm for Higher-Order Rational Patterns
Zhibo Chen, Frank Pfenning
TL;DR
This paper develops a saturation-based unification algorithm for higher-order rational terms, extending Miller's pattern unification to cyclic, regular Böhm trees by treating equalities through definitional expansion of depth-$k$ unfoldings. It first redefines first-order rational unification within a flattened framework, then generalizes to higher-order patterns, introducing contraction and recursion metavariables and a robust preprocessing and saturation machinery. The authors prove termination, soundness, and completeness, establishing that most general unifiers exist for the pattern fragment of higher-order rational terms and are obtainable via a canonical unifier from a saturated context. The work has significant implications for cyclic logic, CoLF-based type reconstruction, and systems with recursive (cyclic) terms, providing a principled foundation for robust unification in higher-order cyclic settings.
Abstract
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.