2023/12/12 by Zhibo Chen, Frank Pfenning, Chen, Zhibo +1
Computer Science · #Logic, programming, and type systems #Natural Language Processing Techniques #semigroups and automata theory
paper · pdf · doi:10.48550/arxiv.2312.07263
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.