Skip to Main content Skip to Navigation
Journal articles

Deciding the Confluence of Ordered Term Rewrite Systems

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.
Document type :
Journal articles
Complete list of metadatas
Contributor : Publications Loria <>
Submitted on : Tuesday, September 26, 2006 - 9:37:57 AM
Last modification on : Thursday, July 2, 2020 - 5:26:02 PM


  • HAL Id : inria-00099508, version 1



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⟩



Record views