August 1995, 141pp, DPhil thesis.
This thesis is primarily concerned with the algebraic semantics of non-terminating term rewriting systems.
The usual semantics for rewrite system is based in interpreting rewrite rules as equations and rewriting as a particular case of equational reasoning. The termination of a rewrite system ensures that every term has a value (normal form). But, in general we cannot guarantee this. The research that has been done on non-terminating rewrite systems is centered on seeking semantics for these systems where the usual properties of confluent systems (like uniqueness of normal forms) still hold. These approaches extend the original set of terms (with infinite terms) in such a way that every term has a value.
We propose a new semantics for rewrite systems based on interpreting rewrite rules as in-equations between terms in an ordered algebra. We show that a variant of equational logic --- inequational logic --- is an institution and we further prove that rewriting is a sound and complete proof system for this logic.
For the case of confluent systems, we show that the algebra of normal forms in a terminating system is a uniquely minimal covering of the term algebra. In the non-terminating case, the existence of this minimal covering is established in the completion of an ordered algebra formed by rewriting sequences. We thus generalize the properties of normal forms for non-terminating systems to this minimal covering. These include the existence of normal forms for arbitrary rewrite systems, and their uniqueness for confluent systems, in which case the algebra of normal forms is isomorphic to the canonical quotient algebra associated with the rules when seen as equations. This extends the benefits of algebraic semantics to systems with non-deterministic and non-terminating computations. We first study properties of abstract orders, and then instantiate these to term rewriting systems.
Furthermore, we review the theory of rewriting systems without any restriction on the form of the rules. In this review we include a comparison between several definitions of concurrent rewriting.