Semantics Of Non-Terminating Systems Through Term Rewriting

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 inequations 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..