| Coq formalization of the higher-order recursive path ordering |  |
Abstract:
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 beta-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 beta-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.
Coq formalization of the higher-order recursive path ordering
In
Applicable Algebra in Engineering, Communication and Computing (AAECC),
20(5-6),
pp. 379-425,
2009.
BibTeX:@article{horpo-aaecc-09,
author = {Adam Koprowski},
title = {{Coq} formalization of the higher-order recursive path ordering},
journal = {Applicable Algebra in Engineering, Communication and Computing (AAECC)},
year = {2009},
volume = {20},
number = {5-6},
pages = {379--425},
} | 
