Computability Closure: Ten Years Later
| dc.creator | Blanqui, Frédéric | |
| dc.date | 2007-07-10 | |
| dc.date.accessioned | 2026-07-07T08:14:49Z | |
| dc.date.available | 2026-07-07T08:14:49Z | |
| dc.description | 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 à 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. | |
| dc.identifier | https://arxiv.org/abs/0707.1372 | |
| dc.identifier | http://arxiv.org/abs/0707.1372 | |
| dc.identifier | Dans Colloquium in honor of Jean-Pierre Jouannaud, 4600 (2007) | |
| dc.identifier.uri | http://salesiana.dossiersoluciones.com/handle/123456789/133262 | |
| dc.subject | Logic in Computer Science | |
| dc.title | Computability Closure: Ten Years Later | |
| dc.type | text |