# Deciding the Confluence of Ordered Term Rewrite Systems

3 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : A term rewrite system (TRS) terminates if, and only if, its rules are contained in a reduction ordering $>$. In order to deal with {\em any\/} set of equations, including inherently non-terminating ones (like commutativity), TRS have been generalized to {\em ordered\/} TRS $(E,>)$, where equations of $E$ are applied in whatever direction agrees with $>$. The confluence of terminating TRS is well-known to be decidable, but for ordered TRS the decidability of confluence has been open. Here we show that the confluence of ordered TRS is decidable if $>$ belongs to a large class of path orderings (including most practical orderings like LPO, MPO, RPO (with status), KNS and RDO), since then {\em ordering constraints\/} for $>$ can be solved in an adequate way. For ordered TRS $(E,>)$ where $E$ consists of {\em constrained equations\/}, confluence is shown to be undecidable. Finally, also {\em ground reducibility\/} is proved undecidable for ordered TRS.
Keywords :
Type de document :
Article dans une revue
ACM Transactions on Computational Logic, Association for Computing Machinery, 2003, 4 (1), pp.33-55
Domaine :

https://hal.inria.fr/inria-00099508
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 09:37:57
Dernière modification le : mardi 13 mars 2018 - 14:24:05

### Identifiants

• HAL Id : inria-00099508, version 1

### Citation

Hubert Comon-Lundh, Paliath Narendran, Robert Nieuwenhuis, Michaël Rusinowitch. Deciding the Confluence of Ordered Term Rewrite Systems. ACM Transactions on Computational Logic, Association for Computing Machinery, 2003, 4 (1), pp.33-55. 〈inria-00099508〉

### Métriques

Consultations de la notice