HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
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 metadata

Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Tuesday, September 26, 2006 - 9:37:57 AM
Last modification on : Thursday, February 10, 2022 - 11:53:38 AM



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. ⟨10.1145/601775.601777⟩. ⟨inria-00099508⟩



Record views