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

Higher-order unification has been shown to be undecidable [Huet 1973]. Miller discovered the pattern fragment and subsequently showed that higher-order pattern unification is decidable and has most general unifiers [1991]. We extend the algorithm to higher-order rational terms (a.k.a. regular Böhm trees [Huet 1998], a form of cyclic \(\lambda\) -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.