Computability Closure: Ten Years Later
Fr\'ed\'eric Blanqui (INRIA Lorraine - LORIA)

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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsScientific Computing and Data Management · Distributed and Parallel Computing Systems
