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

摘要

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 Toy-ama's theorem, generalised slightly to term rewriting systems introducing variables on the right-hand side of the rules.