Computability Closure: Ten Years Later

TL;DR

This paper revisits the concept of computability closure, demonstrating its versatility in proving termination across various rewriting systems and its connection to known recursive path orderings.

Contribution

It extends the applicability of computability closure to beta-normalized rewriting, matching modulo theories, and higher-order data types, and relates it to existing reduction orderings.

Findings

Unified framework for termination proofs in higher-order rewriting.

Extension of computability closure to matching modulo theories.

Equivalence of the extended closure to known recursive path orderings.

Abstract

The notion of computability closure has been introduced for proving the termination of higher-order rewriting with first-order matching by Jean-Pierre Jouannaud and Mitsuhiro Okada in a 1997 draft which later served as a basis for the author's PhD. In this paper, we show how this notion can also be used for dealing with beta-normalized rewriting with matching modulo beta-eta (on patterns \`a la Miller), rewriting with matching modulo some equational theory, and higher-order data types (types with constructors having functional recursive arguments). Finally, we show how the computability closure can easily be turned into a reduction ordering which, in the higher-order case, contains Jean-Pierre Jouannaud and Albert Rubio's higher-order recursive path ordering and, in the first-order case, is equal to the usual first-order recursive path ordering.