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\"{o}hm trees, 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.

翻译：高阶统一问题已被证明是不可判定的。Miller发现了模式片段，并进而证明了高阶模式统一是可判定的且具有最一般统一子。我们将该算法扩展至高阶有理项（又称正则Böhm树，一种循环λ项形式），并证明高阶有理项上的模式统一是可判定的且具有最一般统一子。我们证明了该算法的可靠性与完备性。