Ordered Rewriting and Confluence
One of the major problems in term rewriting theory is what to do with an
equation which cannot be ordered into a rule. Many solutions have been
proposed, including the use of special unification algorithms or of unfailing
completion procedures.
If an equation cannot be ordered we can still use any instances of it which
can be ordered for rewriting. Thus for example $x*y = y*x$ cannot be ordered,
but if $a,b$ are constants with $b*a > a*b$ we may rewrite $b*a -> a*b$.
This idea is used in unfailing completion, and also appears in the
Boyer-Moore system. In this paper we define and investigate completeness with
respect to this notion of rewriting and show that many familiar systems are
complete rewriting systems in this sense. This allows us to decide equality
without the use of special unification algorithms. We prove completeness by
proving termination and local confluence. We describe a confluence test
based on recursive properties of the ordering.
dvi
BibTeX:
<![CDATA[
@inproceedings{Martin-Nipkow-CADE-90,
author="Ursula Martin and Tobias Nipkow",
title="Ordered Rewriting and Confluence",
booktitle="Proc.\ 10th Int.\ Conf.\ Automated Deduction",
editor="M.E. Stickel",
year=1990,publisher=Springer,series=LNCS,volume=449,pages="366--380"}
]]></plaintext></p></div></div>