Abstract: Monads and Modular Term Rewriting

Monads and Modular Term Rewriting

Christoph Lüth
Bremen Institute for Safe Systems, FB 3, Universität Bremen

Neil Ghani
The School Of Computer Science, University of Birmingham

Monads can be used to model term rewriting systems by generalising the well-known equivalence between universal algebra and monads on the category Set. In [Lü96], the usefulness of this semantics was demonstrated by giving a purely categorical proof of the modularity of confluence for the disjoint union of term rewriting systems (Toyama's theorem). This paper provides further support for the use of monads in term rewriting by giving a categorical proof of the most general theorem concerning the modularity of strong normalisation. In the process, we improve upon some technical aspects of the earlier work.

Christoph Lüth, 16.06.97