Abstract:A term rewrite system (TRS) terminates if its rules are contained in a reduction ordering >. In order to deal with any set of equations, including inherently non-terminating ones (like commutativity),...A term rewrite system (TRS) terminates if its rules are contained in a reduction ordering >. In order to deal with any set of equations, including inherently non-terminating ones (like commutativity), TRS have been generalised to 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 ordering constraints for > can be solved in an adequate way, which holds in particular for the class of LPO orderings. For sets E of constrained equations, confluence is shown to be undecidable. Finally, ground reducibility is proved undecidable for ordered TRS.Read More
Publication Year: 2002
Publication Date: 2002-11-27
Language: en
Type: article
Indexed In: ['crossref']
Access and Citation
Cited By Count: 22
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot