Constrained rewriting in recognizable theories

Tony Bourdier 1 Horatiu Cirstea 1
1 PAREO - Formal islands: foundations and applications
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Rewriting has long been shown useful for equational reasoning but its expressive power is not always appropriate for certain situations, as for instance for specifying partial functions and exceptions or when dealing with relations over terms. That is why some generalizations of rewriting, such as ordered rewriting, class rewriting, strategic rewriting, conditional or constrained rewriting, have emerged. In particular, constraints over terms are very suitable to define sets of terms thanks to logic formulae. Most of the works on constrained rewriting focus on order, equality, disequality and membership constraints. We extend in this paper the usual notion of constrained rewrite systems by constraining rules not only with classical constraints but with any first order formula and perform rewriting according to an interpretation of functional and predicate symbols. We then show that the specification of such interpretations with tree automata offers us a framework sufficiently powerful to build an algorithm for solving a particular case of constrained matching.
Type de document :
Pré-publication, Document de travail
2010
Liste complète des métadonnées

Littérature citée [19 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00456848
Contributeur : Tony Bourdier <>
Soumis le : samedi 17 avril 2010 - 19:24:41
Dernière modification le : jeudi 11 janvier 2018 - 06:22:10
Document(s) archivé(s) le : jeudi 23 septembre 2010 - 12:55:18

Fichier

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

Identifiants

  • HAL Id : inria-00456848, version 2

Collections

Citation

Tony Bourdier, Horatiu Cirstea. Constrained rewriting in recognizable theories. 2010. 〈inria-00456848v2〉

Partager

Métriques

Consultations de la notice

248

Téléchargements de fichiers

107