Paper: Decision Problems in Ordered Rewriting (at LICS 1998)

Authors: Hubert Comon-Lundh Paliath Narendran Robert Nieuwenhuis Michaël Rusinowitch

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), 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

BibTeX

  @InProceedings{ComonLundhNarendran-DecisionProblemsinO,
    author = 	 {Hubert Comon-Lundh and Paliath Narendran and Robert Nieuwenhuis and Michaël Rusinowitch},
    title = 	 {Decision Problems in Ordered Rewriting},
    booktitle =  {Proceedings of the Thirteenth Annual IEEE Symposium on Logic in Computer Science (LICS 1998)},
    year =	 {1998},
    month =	 {June}, 
    pages =      {276--286},
    location =   {Indianapolis, IN, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }