(HO)RPO Revisited

TL;DR

This paper explores the relationship between computability closure and recursive path orderings, demonstrating their equivalence in the first-order case and extending higher-order orderings to richer type systems.

Contribution

It clarifies the connection between computability closure and recursive path orderings, enabling extensions to more complex type systems in higher-order rewriting.

Findings

First-order recursive path ordering equals an ordering derived from computability closure.

Higher-order recursive path ordering is contained within a new ordering based on computability closure.

Extension of higher-order recursive path ordering to richer type systems is possible.

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.