Investigations on termination of equational rewriting

Abstract : This paper is a report of detailed investigations on the termination problem of rewriting modulo equational theories. We present here three approachs of this problem. We point out the difficulties and explain how the methods fail, giving some ideas issued from a rigorous observation of the failing processes. The first part is a new approach of the classical associative commutative (AC in short) orderings using the cooperation on abstract relations. We point out this proof method is not easy, because of an infinity of critical pairs to be considered. The second work consists in adapting the AC orderings with flattening to ensure termination modulo a large class of permutative theories. But the characterization of this class points out nothing other than the theories included in AC, for which the AC termination methods can be used. So we deduce, AC is the maximal class working with flattening. In the third chapter of this report, we propose a new AC ordering, replacing both flatening and distributing transformations by a single powerful transformation. We exhibit a counter-example to show that this method does not provide an F-compatible ordering.
Type de document :
Rapport
[Research Report] RR-0732, INRIA. 1987
Liste complète des métadonnées

https://hal.inria.fr/inria-00075820
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 19:05:54
Dernière modification le : samedi 17 septembre 2016 - 01:06:51
Document(s) archivé(s) le : vendredi 13 mai 2011 - 15:30:44

Fichiers

Identifiants

  • HAL Id : inria-00075820, version 1

Collections

Citation

Isabelle Gnaedig. Investigations on termination of equational rewriting. [Research Report] RR-0732, INRIA. 1987. 〈inria-00075820〉

Partager

Métriques

Consultations de la notice

73

Téléchargements de fichiers

48