(HO)RPO Revisited
| dc.creator | Blanqui, Frédéric | |
| dc.date | 2006-09-08 | |
| dc.date.accessioned | 2026-07-07T07:23:49Z | |
| dc.date.available | 2026-07-07T07:23:49Z | |
| dc.description | 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. | |
| dc.identifier | https://arxiv.org/abs/cs/0609037 | |
| dc.identifier | http://arxiv.org/abs/cs/0609037 | |
| dc.identifier.uri | http://salesiana.dossiersoluciones.com/handle/123456789/116123 | |
| dc.subject | Logic in Computer Science | |
| dc.title | (HO)RPO Revisited | |
| dc.type | text |