| Well-foundedness of the Recursive Path Ordering in Coq |  |
Abstract:
One of the important methods to prove termination of term rewriting is based on Dershowitz' recursive path ordering (RPO).
A rewrite system is terminating if we have l > r in the RPO for every rewrite rule l -> r. A key step in the correctness
proof of this method is to show that RPO is well-founded. Originally this is shown using Kruskal's Tree Theorem. An
alternative is to proceed by induction on the definition of terms. We discuss a formalization of the latter proof in Coq.
Higher-order rewriting, where bound variables may be present, for a long time lacked methods to prove termination.
An important step forward was the generalization of RPO to the higher-order case (HORPO) by Jouannaud and Rubio. As in
the first-order case, a key step is to show well-foundedness of the ordering. There is no suitable higher-order version
of Kruskal's Tree Theorem; the proof by Jouannaud and Rubio proceeds by induction on the definition of terms and uses
the computability predicate. We discuss a formalization of the proof of well-foundedness in Coq. The formalized proof
for the first-order case is actually found as a specialization of the proof for the higher-order case.
This is work in progress.
Well-foundedness of the Recursive Path Ordering in Coq
In
Dutch Proof Tools Day 2004,
Nijmegen, The Netherlands.
BibTeX:@inproceedings{rpo-PTD-04,
author = {Nicole de Kleijn and Adam Koprowski and Femke van Raamsdonk},
title = {Well-foundedness of the Recursive Path Ordering in {Coq}},
booktitle = {Dutch Proof Tools Day 2004},
year = {2004},
pages = {53--68},
} | 
