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.