(HO)RPO Revisited
Abstract
The notion of computability closure has been introduced for proving the termination of the combination of higher-order rewriting and beta-reduction. It is also used for strengthening the higher-order recursive path ordering. In the present paper, we study in more details the relations between the computability closure and the (higher-order) recursive path ordering. We show that the first-order recursive path ordering is equal to an ordering naturally defined from the computability closure. In the higher-order case, we get an ordering containing the higher-order recursive path ordering whose well-foundedness relies on the correctness of the computability closure. This provides a simple way to extend the higher-order recursive path ordering to richer type systems.
Cite
@article{arxiv.cs/0609037,
title = {(HO)RPO Revisited},
author = {Frédéric Blanqui},
journal= {arXiv preprint arXiv:cs/0609037},
year = {2007}
}