Abstract: Compositional Term Rewriting...

Compositional Term Rewriting:
An Algebraic Proof of Toyama's Theorem

Christoph Lüth

Universität Bremen - FB 3

This article proposes a compositional semantics for term rewriting systems, i.e. a semantics preserving structuring operations such as the disjoint union. The semantics is based on the categorical construct of a monad, adapting the treatment of universal algebra in category theory to term rewriting systems.

As an example, the preservation of confluence under the disjoint union of two term rewriting systems is shown, obtaining an algebraic proof of Toyama's theorem, generalised slightly to term rewriting systems introducing variables on the right-hand side of the rules.


Christoph Lüth, 25.10.96