Coq formalization of the higher-order recursive path ordering
Adam Koprowski · Applicable Algebra in Engineering Communication and Computing · 2009
The recursive path ordering ( RPO ) is a well-known reduction ordering introduced by Dershowitz, that is useful for proving termination of term rewriting systems (TRSs). Jouannaud and Rubio generalized this ordering to the higher-order case thus creating the higher-order recursive path ordering ( HORPO ). They proved that this ordering can be used for proving termination of higher-order TRSs, which essentially comes down to proving well-foundedness of HORPO . This result entails well-foundedness of RPO and termination of simply typed lambda calculus (as the β -reduction relation is included in HORPO ). This paper describes our undertaking of providing a complete, axiom-free, fully constructive formalization of those results in the proof assistant Coq . The formalization can be divided into three parts: finite multisets and two variants of multiset extensions of a relation, simply typed lambda calculus with termination of β -reduction as the main result, HORPO with a proof of its well-foundedness; also decidability of HORPO has been proved and, due to its constructive nature, a certified algorithm to verify whether two terms can be oriented with HORPO can be extracted from the proof.