Monads and Modular Term Rewriting

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¨u96], this semantics was used to give a purely categorical proof of the modularity of confluence for the disjoint union of term rewriting systems. This paper provides further support for monadic semantics of rewriting by giving a categorical proof of the most general theorem concerning the modularity of strong normalisation. In the process, we improve upon the technical aspects of earlier work.

• Type: Conference
• Year: 1997
• Where: CTCS
• Authors: Christoph Lüth, Neil Ghani
• Keywords: Categorical Proof, CTCS 1997, Programming Languages, Term Rewriting Systems, Well-known Equivalence