Abstract

In conditional term rewrite systems certain properties change their intuitive meaning when compared to unconditional rewriting. This is due to the fact that in rewrite steps, the evaluation of the conditions is left implicit. For instance, termination of a conditional term rewrite system does not imply the absence of infinitely many steps in the conditions. For this reason, the notion of operational termination has been introduced in the past that also considers the evaluation of conditions. This paper investigates the case of confluence in conditional term rewrite systems and introduces the notion of operational confluence, a confluence property that also implies confluence of the evaluations of conditions.

BibTeX

@inproceedings{KG-IWC15,
 author    = "Karl Gmeiner",
 title     = "Operational Confluence of Conditional Term Rewrite Systems",
 booktitle = "Proceedings of the 4th International Workshop on Confluence",
 editors   = "Ashish Tiwari and Takahito Aoto",
 pages     = "18--22",
 year      = 2015
}