Computability Closure: Ten Years Later

Frédéric Blanqui 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
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 à 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.
Type de document :
Communication dans un congrès
Colloquium in honor of Jean-Pierre Jouannaud, Jun 2007, Cachan, France. 4600 (4600), 2007, LNCS. 〈10.1007/978-3-540-73147-4_4〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00161092
Contributeur : Frédéric Blanqui <>
Soumis le : lundi 9 juillet 2007 - 17:35:57
Dernière modification le : jeudi 8 février 2018 - 11:32:01
Document(s) archivé(s) le : jeudi 8 avril 2010 - 19:07:47

Fichiers

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Frédéric Blanqui. Computability Closure: Ten Years Later. Colloquium in honor of Jean-Pierre Jouannaud, Jun 2007, Cachan, France. 4600 (4600), 2007, LNCS. 〈10.1007/978-3-540-73147-4_4〉. 〈inria-00161092〉

Partager

Métriques

Consultations de la notice

209

Téléchargements de fichiers

95