Computability Closure: Ten Years Later - INRIA - Institut National de Recherche en Informatique et en Automatique Accéder directement au contenu
Communication Dans Un Congrès Année : 2007

Computability Closure: Ten Years Later

Résumé

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.
Fichier principal
Vignette du fichier
main.pdf (286.17 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

inria-00161092 , version 1 (09-07-2007)

Identifiants

Citer

Frédéric Blanqui. Computability Closure: Ten Years Later. Colloquium in honor of Jean-Pierre Jouannaud, Jun 2007, Cachan, France. ⟨10.1007/978-3-540-73147-4_4⟩. ⟨inria-00161092⟩
166 Consultations
98 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More