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.

We give a new presentation of Brzozowski’s algorithm to minimize finite automata using elementary facts from universal algebra and coalgebra and building on earlier work by Arbib and Manes on a categorical presentation of Kalman duality between reachability and observability. This leads to a simple proof of its correctness and opens the door to further generalizations. Notably, we derive algorithms to obtain minimal language equivalent automata from Moore nondeterministic and weighted automata.