(HO)RPO Revisited
<|reference_start|>(HO)RPO Revisited: 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.<|reference_end|>
@article{blanqui2006(ho)rpo,
    title={(HO)RPO Revisited},
    author={Fr'ed'eric Blanqui (INRIA Lorraine - LORIA)},
    journal={arXiv preprint arXiv:cs/0609037},
    year={2006},
    archivePrefix={arXiv},
    eprint={cs/0609037},
    primaryClass={cs.LO}
}