An Introduction to Categorical Rewriting

Christoph Lüth

(FB 3 — Mathematik und Informatik, Universität Bremen

                      cxl@informatik.uni-bremen.de)

Neil Ghani

(Department of Mathematics and Computer Science, University of Leicester

                            ng13@mcs.le.ac.uk)

Abstract: Term rewriting systems (TRSs) are widely used throughout computer science as they form an abstract model of computation. However, the concrete syntactic nature of term rewriting often obscures the underlying structure, and the usual semantics based upon relations lacks the structure to adequately model key concepts arising in more complex problems. A more abstract semantics at an intermediate level of abstraction between the syntax and the relational model is therefore needed. Generalising the categorical treatment of universal algebra, we model TRSs by monads. This way, we have for the first time been able to give categorical proofs of state of the art results in rewriting. This paper forms an introduction to our research, highlighting the new insights afforded by the categorical perspective and sketching the application of this semantics to modular rewriting.

1 Introduction

Term rewriting systems combine the flexibility and generality of universal algebra with the computational notion of reduction. They originally arose in the study of the λ-calculus and combinatory logic. More recently, they have played a prominent rôle in the design and implementation of logical and functional programming languages, the theory of abstract data types, and automated theorem proving. They have also found applications in recursion theory and algebra, as they are a Turing-complete model of computation which can be used to provide decision procedures.

The concreteness of TRSs has lead to a tendency to concentrate on the syntactical details of specific problems to the detriment of a wider understanding of the subject. Abstract models of TRSs have been developed to address this problem with the simplest being Abstract Reduction Systems (ARSs) based upon

1 Technical Report No. 2000/35, Department of Mathematics & Computer Science,

University of Leicester, University Road, Leicester LE1 7RH, England. \begin{matrix}c \\ ◯ \end{matrix} University of Leicester, 2000.

relations. While useful for certain results, ARSs lack sufficient structure to adequately model key concepts such as substitution, context, layer structure etc, and hence ARSs are mainly used as an organisational tool with the difficult results proved directly at the syntactic level.

Category theory has been used to provide a semantics for term rewriting systems at an intermediate level of abstraction between the actual syntax and the relational model. Research originally focused on structures such as 2-categories [Rydeheard and Stell, 1987, Seely, 1987], Sesqui-categories [Stell, 1994] and ordered categories [Jay, 1990, Ghani, 1995a] as models of TRSs. However, despite some one-off results [Ghani, 1995b, Rydeheard and Stell, 1987], these approaches have yet to make a lasting impact on term rewriting. Part of the problem seems to be that these semantics are for the most part term-generated, and we often end up translating the problem back into the syntax!

Our alternative approach starts from the observation that term rewriting systems can be regarded as generalisations of algebraic theories. Syntactically, algebraic theories declare term constructors, while TRSs declare term constructors and rewrite rules, thus both are presented via signatures. Semantically, algebraic theories are modelled by sets of terms while TRSs are modelled by pre-orders of terms. Categorically, algebraic theories are modelled as monads on the category of sets and so it is natural to model a term rewriting system by a monad over a more structured base category.

This work combines techniques from two rather distant areas, and few readers will be experts in both of them. Hence, we here give an introductory exposition of our research, suitable to a general audience of theoretical computer scientists. We assume no familiarity with term rewriting, and merely a passing knowledge of the basics of category theory, concepts such as categories, functors, natural transformations, limits and colimits, and adjunctions, which can be found e.g. in Chapter I–V of [Mac Lane, 1971].

The main contribution of this paper is an overview of the monadic semantics for TRSs, with an emphasis on examples and motivation, giving basic definitions and results while eliding the technical proofs which can be found in the references. Instead, we shall concentrate on where the categorical perspective gives new insights into rewriting and demonstrate how our ideas can be applied to modularity problems.

The structure of this paper is as follows: in the next section, we will present the modelling of algebraic theories by monads. [Section 3] will introduce the basics of TRSs and ARSs. In [Section 4], we will present the monadic semantics, and demonstrate how to use this semantics in modularity problems in [Section 5]. [Section 6] closes with a summary and an outlook.

2 Algebraic Theories and Monads

Since our approach generalises the categorical treatment of universal algebra, where algebraic theories are equivalent to monads on the category of sets, we will give a self-contained presentation of this equivalence here. However, since this standard material, we omit proofs and instead refer the reader to [Manes, 1976] or Chapter VI of [Mac Lane, 1971].

Definition 1 (Signature). A (single-sorted) signature consists of a function Σ : Nat → Set. The set of n-ary operators of Σ is defined Σ_{n} =^{def} Σ(n).

Definition 2 (Term Algebra). Given a signature Σ and a set of variables X, the term algebra T_{Σ}(X) is defined inductively:

{x ∈ X \atop 'x ∈ T_{Σ}(X)}  \begin{matrix}f ∈ Σ_{n} & t_{1}, … t_{n} ∈ T_{Σ}(X) \\ f(t_{1}, …, t_{n}) ∈ T_{Σ}(X) \end{matrix}

Quotes are used to distinguish a variable x ∈ X from the term 'x ∈ T_{Σ}(X). This will become important when analysing the layer structure on terms formed by the disjoint union of signatures.

Definition 3 (Equations and Algebraic Theories). Given a signature Σ,a Σ-equation is of the form X ⊢ t = s where X is a set and t, s ∈ T_{Σ}(X). An algebraic theory ⟨Σ, E⟩ consists of a signature Σ and a set E of Σ-equations.

The term algebra construction generalises from signatures to algebraic theories by mapping a set X to the term algebra quotiented by the equivalence relation ∼ generated from the equations

T_{A}(X) = T_{Σ}(X)/∼

The key idea of the categorical semantics is that the free term algebra construction, which for every set X gives us the set of terms of term T_{A}(X), extends to a functor T_{A} : Set → Set over the category Set of sets. Further, every variable x ∈ X gives a term 'x ∈ T_{A}(X), so the variables are given by a function η_{X} : X → T_{A}(X). Lastly, substitution takes terms built over terms and flattens them, as described by a function μ_{X} : T_{A}(T_{A}(X)) → T_{A}(X). These three pieces of data define a monad:

Definition 4 (Monad). A monad T = ⟨T, η, μ⟩ on a category C is given by an endofunctor T : C → C, called the action, and two natural transformations, η : 1 ⇒ T, called the unit, and μ : T T ⇒ T, called the multiplication of the monad, satisfying the monad laws: μ.T η = 1 = μ.η_{T}, and μ.T μ = μ.μ_{T}.

Lemma 5. For every algebraic theory A, T_{A} = ⟨T_{A}, η, μ⟩ is a monad.

The data from Def. 4 are actually enough to characterise term construction. Further, the category of algebras of this monad is equivalent to the category of models of A, justifying the claim that “universal algebra is the study of monads over Set” ([Manes, 1976], pg. 42).

In summary, monads provide an abstract calculus for algebraic theories where variables, substitution and term algebra (represented by the unit, multiplication and action of the monad) are taken as primitive concepts.

3 Term Rewriting Systems and Abstract Reduction Systems

This section reviews the basic concepts of term rewriting systems and abstract reduction systems. Further details may be found in [Baader and Nipkow, 1998, Klop, 1992].

Definition 6 (Rewrite Rules and TRSs). Given a signature Σ, a Σ-rewrite rule is of the form (Y ⊢ l → r) where Y is a set of variables and l, r ∈ T_{Σ}(Y). A term rewriting system R = ⟨Σ, R⟩ consists of a signature Σ and a set R of Σ-rewrite rules.

Usually one requires that l is not a variable and that the free variables of r are contained in the free variables of l, but semantically these restrictions are not necessary and hence omitted here. In the following examples, we denote the arity of an operation by subscripts; so f ∈ Σ(n) is denoted by f_{n}.We also use infix notation for binary operators:

Example 1 (Combinatory Logic). The TRS CL = ⟨Σ_{CL}, R_{CL}⟩ has Σ_{CL} = {S_{0}, K_{0},._{2}} and R_{CL} = {{x, y} ⊢ (K.x).y → x, {x, y, z} ⊢ ((S.x).y).z → (x.z).(y.z)}.

Example 2 (Addition). The TRS Add = ⟨Σ_{Add}, R_{Add}⟩ implements addition on the natural numbers and has Σ_{Add} = {0_{0}, S_{1}, +_{2}} and R_{Add} = {r_{1}, r_{2}} where

r_{1} = {x} ⊢ 0 + x → x
r_{2} = {x, y} ⊢ Sx + y → S(x + y)

A term rewriting system R induces a one-step reduction relation →_{R} on the terms. Formally, this is obtained by closing the rewrite rules under contexts and substitutions — for the exact definitions, see [Klop, 1992]. The many-step reduction relation ↠_{R} is the reflexive-transitive closure of the one-step reduction relation. For example, the addition TRS supports the following rewrites

\begin{matrix}S(0 + 0) + 0 & ↠ & S((0 + 0) + 0) \\ S0 + 0 & ↓ ↓ & \overline{↠} & S(0 + 0) & ↓ ↓ & \overline{↠} & S0 \end{matrix}

Notice that although the term S(0 + 0) + 0 can be reduced to two different terms, this choice is illusory as both reduce to S(0 + 0). Further, there are no infinite reduction sequences starting from the term S(0 + 0) + 0. These examples illustrate the two key properties of TRSs:

Definition 7 (Confluence and SN). A term rewriting system R = ⟨Σ, R⟩ is confluent iff ∀t, s_{1}, s_{2}. t ↠_{R} s_{1} ∧ t ↠_{R} s_{2} ∃u. s_{1} ↠_{R} u ∧ s_{2} ↠_{R} u. It is strongly normalising (SN) iff there is no infinite sequence t_{1} →_{R} t_{2} →_{R} t_{3} →_{R} . . ..

Example 1 is confluent, but not strongly normalising while Example 2 is confluent and strongly normalising. This may not be apparent at first sight, and indeed in general these properties are undecidable. Consequently a variety of proof tools have been developed which are helpful in certain cases. Some of these methods keep track of the redexes, the places in the term where a rewrite can be applied. Possibly the most famous example of redex tracking is the minimal developments technique used in λ-calculus [Hindley and Seldin, 1986]. Other, more ad-hoc methods include Knuth-Bendix Completion [Knuth and Bendix, 1970], reducibility, and ordering the operations or terms (reduction orders) to show termination. These methods are rather technical, often involving copious amounts of induction on the structure of terms, and tend to impose syntactic preconditions on term rewriting systems, such as left-linearity or orthogonality.

In order to remedy this situation, we turn to the semantics of term rewriting systems hoping to obtain a new ontology for rewriting. The simplest models of TRSs are the abstract reduction systems based upon relations; the advantages of this approach are its simplicity and versatility.

Definition 8 (Abstract Reduction Systems). An abstract reduction system (ARS) is a pair A = ⟨A, →_{A}⟩ consisting of a carrier set A and a binary relation →_{A}⊆ A × A, called the reduction or rewrite relation.

Every term rewriting system R = ⟨Σ, R⟩ defines an ARS whose carrier set is the set of terms T_{Σ}(V) where V is an infinite set of variables, and whose relation is the one-step reduction relation. Properties like confluence and strong normalisation can be (and usually are) defined on the level of ARSs. We can then prove lemmas and theorems about these properties at the level of relations, such as Newman’s Lemma (if an ARS is locally confluent and strongly normalising then it is confluent), or the Hindley-Rosen Lemma (if two ARS are confluent and commute, then their union is confluent).

The key point about these lemmas and their proofs is that they are formulated and proven at the level of relations. Nowhere do we need the fact that the carrier set consists of terms and that, for example, results may be proven by induction on term structure. Thus we may contrast the relational methodology of the ARS model to the combinatorial methodology inherent in direct reasoning.

While these lemmas are very useful, relations cannot express the key concepts of term rewriting like substitution, redex, context, layer and everything else relating to the term structure. Hence, ARSs are mainly used as an organisational tool, while the difficult results are proven directly at the syntactic level. Thus, the very simplicity which is the advantage of relational models is also its main limitation. What is needed is a semantics at an intermediate level of abstraction between the actual syntax and the relational model.

4 Categorical Models of Term Rewriting Systems

The key observation underlying our semantics for TRSs is that TRSs can be viewed as generalised algebraic theories. This generalisation occurs at both a syntactic and a semantic level. Syntactically, algebraic theories and TRSs are both presented via signatures — the former declares term constructors while TRSs declare term constructors and rewrite rules. Semantically, algebraic theories are modelled by sets with extra structure while TRSs are modelled by pre-orders with extra structure.

Given the satisfactory categorical treatment of algebraic theories by monads on Set presented in [Section 2], it is natural to model a term rewriting system by a monad over a more structured base category. In this section we formalise these comments, first with a concrete construction and then with a more abstract, and in many ways more illuminating, construction.

4.1 A Monadic Semantics for TRSs

We will now generalise the monadic semantics from algebraic theories to TRSs. Our aim is to model a TRS R = ⟨Σ, R⟩ by a monad T_{R}.

First, we have to decide on the base category of the monad. Since the main focus of rewriting is to prove properties of the many-step reduction relation, we choose to use the category Pre of pre-orders and monotone functions. Other possibilities are the category Cat of all small categories and functors, if we were interested in labelled many-step reduction or the category Rel of relations and monotone maps if one wanted to model the one-step reduction relation.

Next we consider the action of the monad T_{R}. Recall that if A is an algebraic theory, then T_{A} maps a set of variables to the free algebra over it. In general, the action is an endofunctor, and variables and theory must belong to the same category which in our case is Pre. Thus, the action T_{R} should map a pre-order of variables P to the pre-order of terms and rewrites built over P. The order structure on the variables can be thought of as reduction assumptions: if a → b, then whatever we substitute for a has to reduce to what we substitute for b.

Thus, we have two main differences from the traditional semantics: a TRSs is modelled by a particular kind of function rather than a relation; and we endow variables with an order structure. A third categorically inspired idea is that there is no fixed collection of variables, but that we have a term reduction algebra defined for every pre-order of variables.

Table 1: The Term Reduction Algebra for a TRS R = ⟨Σ, R⟩

Given a term rewriting system R = ⟨Σ, R⟩ and a pre-order X, the term reduction algebra T_{R}(X) is the smallest pre-order → on the terms T_{Σ}(X) satisfying the following rules:

[Var] {x → y in X \atop 'x → 'y}  [Cong] {f ∈ Σ_{n}, t_{1} → s_{1}, …, t_{n} → s_{n} \atop f(t_{1}, …, t_{n}) → f(s_{1}, …, s_{n})}
[Inst] {(Y ⊢ l → r) ∈ R, σ : Y → T_{R}(X) \atop lσ → rσ}

These considerations are summed in the definition of the term reduction algebra in [Tab. 4.1]. As with algebraic theories, this gives rise to a monad:

Lemma 9. Let R be a TRS. The map X ↦ T_{R}(X) extends to a monad T_{R} = ⟨T_{R}, η, μ⟩ on Pre.

Proof. The proof is the obvious generalisation of Lemma 5. Essentially, we have to show that the action, unit and substitution preserve the reduction order. Note how the clause [Var] guarantees that the unit is a monotone function.

Lemma 9 provides us with a categorical semantics for TRSs. This semantics is powerful enough to prove non-trivial modularity results, but in a number of ways, it is still unsatisfactory and can be improved on. Firstly, the semantics is still term-generated; proofs about it will still use induction on the term structure; secondly, the semantics has been constructed based on a number of choices, like that of the base category, and if we change any of these, we have to start the construction from scratch again; and thirdly, the construction does not generalise easily to other forms of rewriting. These deficiencies are answered by the theory of enriched monads.

4.2 TRSs and Enriched Monads

As we have seen, algebraic theories are modelled by monads over Set while TRSs are modelled by monads over Pre. These results are instances of a general theory developed by Kelly and Power [Kelly, 1982, Kelly and Power, 1993] which shows how monads over categories other than Set give rise to a generalised notion of algebraic theories. For any such category C, this theory provides us with suitably generalised notions of signature, term, and equations (Def. 10, 11 and 12 below). Technically, we enrich the monads [Kelly, 1982], and this imposes certain conditions on C, but since this paper is tutorial in nature, we omit these here; we also make several simplifications to keep technicalities at a minimum. [Robinson, 1994] gives a gentle introduction but more exact introduction into this theory. [Section 5] dealing with the application of our semantics to modular rewriting is independent of this material and hence may be read first.

Recall from definition 1 that a signature is a function Σ : Nat → Set which maps each arity n to the set of operations Σ(n) of that arity. To define signatures for a category C we replace a set of operations by a C-object of operations, i.e. change the codomain of Σ to C. This will be the general theme: we systematically replace everything specific to Set by C. As for the domain of Σ, the key point is that the natural numbers represent the isomorphism classes of finite sets (i.e. objects of the base category). Hence, we replace Nat by the finitely presentable objects of C:

Definition 10 (Generalised Signatures). If C is a category, then a C-signature is a map Σ : |C_{fp}| → C.

A pre-order is finitely presentable iff its carrier set is finite. Hence if we present a TRS as a generalised signature Σ, the signature will map a finite pre-order P to a pre-order Σ(P) of operations of that arity. The carrier set of Σ(P) can be thought of as term constructors and the order relation as rewrite rules. This is another instance where the categorical approach differs from the traditional one where rewrite rules are more often viewed as oriented equations rather than constructors in their own right.

We write 1, 2, … for the finite discrete pre-orders, the elements of which we denote as x_{1}, x_{2}, . . ..

Example 3 (Addition cont’d). In the generalised signature R for the addition TRS, the term constructors retain their arities, while the two rewrite constructors have arity 1 and 2, respectively. Hence, we have

R(∅) = (0)
R(1) = (S s_{1} ⟶^{r_{1}} t_{2})
R(2) = (+ s_{2} ⟶^{r_{2}} t_{2})
R(X) = () otherwise

Since the arity of the rewrite rule 0 + x_{1} → x_{1} is the discrete 1-element preorder, we have represented it by an arrow in R(1). But of course arrows need sources and targets, and hence the carrier set of R(1) has three elements and thus declares three term constructors. To model a TRS as a generalised signature we extend the signature of the TRS with a term constructor for the source and target of every rewrite rule r_{i} (which above are denoted by s_{i} and t_{i}). We shall later use equations to enforce that e.g. the target of rule r_{2} equals S(x_{1} + x_{2}).

Importantly, arities can be non-discrete. Syntactically, this means we allow generalised rewrite rules, given as (Y ⊢ l → r) where Y is a pre-order and l, r ∈ T_{A}(Y).

The next step is to generalise the term algebra construction from Def. 2. The term algebra over a set X can be seen as the limit of the sets T_{n}(X) of terms of depth at most n. The terms of depth 0 are just the variables while terms of depth n+1 are formed by applying operations of arity m to m-tuples of terms of depth n. Thus, the terms of depth n + 1 are pairs of f ∈ Σ(m) and maps m → T_{n}(X). Equivalently, the terms of depth n+1 are given by Set(m, T_{n}(X))×Σ(m), where Set(m, T_{n}(X)) is the set of maps from m to T_{n}(X). Abstracting away from the category Set, we obtain the following:

Definition 11 (Generalised Term Algebra). For a C-signature Σ : |C_{fp}| → C, the term algebra T_{Σ}(X) over an object X of C is where

T_{Σ}(X) =^{def} colim_{n<ω} T_{n}(X)
T_{0}(X) =^{def} X
T_{n+1}(X) =^{def} X + ∑_{c∈Cfp} C(c, T_{n}(X)) × Σ(c)

Example 4 (Addition cont’d). Let P be the pre-order (a→b). Leaving away those arities c for which Σ(c) is empty, we get

T_{1}(P) = P + Pre(∅, P) × Σ(∅) + Pre(1, P) × Σ(1) + Pre(2, P) × Σ(2)

Now Pre(∅, P) = 1, Pre(1, P) = P and Pre(2, P) = P × P. Hence T_{1}(P) is the preorder with the following elements and order structure:

[figure: a; S(a); s_{1}(a); t_{1}(a); 0; b; S(b); s_{1}(b); t_{1}(b); a + a; a + b; b + a; b + b; s_{1}(a, a); s_{1}(a, b); t_{1}(a, a); t_{1}(a, b); s_{1}(b, a); s_{1}(b, b); t_{1}(b, a); t_{1}(b, b)]

Finally, we need to replace the term constructors representing the source and target of rewrites with the intended terms. Intuitively we would like to write

s_{1}(x) = 0 + x t_{1}(x) = x s_{2}(x, y) = Sx + y t_{2}(x, y) = S(x + y)

Thus, we have to move from generalised signatures to generalised algebraic theories. As with signatures, equations have arities and the collection of all equations of a given arity are required to form an object of C.

Definition 12 (Generalised Algebraic Theory). A generalised algebraic theory A = ⟨Σ, E⟩ is given by a generalised signature Σ, and a set of equations, which are given by a function E : |C_{fp}| → C together with a family of pairs of maps

{E(c)  [figure: σ_{c}; τ_{c}] T_{Σ}(c)}_{c∈|Cfp|}

The idea is that E specifies the shape of the equations while the maps σ and τ can be thought of as exhibiting a subobject of T_{Σ}(c) × T_{Σ}(c), i.e. pairs of terms, just like usual equations.

In the addition example there are two equations between terms of arity 1 and two equations between terms of arity 2, hence E(1) = E(2) = (∘ ∘). The maps σ_{1} and τ_{1} now pick out a pair of elements of T_{Σ}(1), and similarly σ_{2} and τ_{2}. Therefore we define:

\begin{aligned}σ_{1}(∘ ∘) & = & (s_{1}(x_{1}) & t_{1}(x_{1})) \\ τ_{1}(∘ ∘) & = & (0 + x_{1} & x_{1}) \\ σ_{2}(∘ ∘) & = & (s_{2}(x_{1}, x_{2}) & t_{2}(x_{1}, x_{2})) \\ τ_{2}(∘ ∘) & = & (Sx_{1} + x_{2} & S(x_{1} + x_{2})) \end{aligned}

Just as for usual algebraic theories, the semantics of such a generalised algebraic theory is constructed as the quotient of the term algebra by the equations. Categorically, quotients are defined by coequalisers and hence the monad T_{A} is presented as the coequaliser of the two maps σ and τ or, in other words the smallest monad which makes these maps equal.

We finish this section with a crucial observation about our semantics, namely that it is constructed categorically, and hence we can reason about it categorically. This contrasts, for example, with the 2-categorical semantics of a TRS where the theory of a TRS is constructed syntactically. It is also more amenable to generalisations, e.g. the equations do not have to be between a source or target and a term, we can have equations between any two terms, allowing for equational rewriting.

5 Monads and Modularity

Modularity seeks criteria under which structured TRSs inherit properties from smaller (and hence easier to reason about) subsystems. Formally, a property P is modular for a structuring operation ⊕ iff

R_{1} ⊕ R_{2} ⊧ P iff (R_{1} ⊧ P and R_{2} ⊧ P)

There is a host of results in the literature about modularity. For example, confluence is modular with respect to the disjoint union, but strong normalisation is only modular under strong syntactic conditions. Neither property is modular for the non-disjoint union of TRSs (see [Baader and Nipkow, 1998] for a survey of results and further references).

To attack the modularity of P for ⊕ categorically, we have to

1. Give a semantics of rewriting by representing R as a monad T_{R};

2. Find a monadic version of the property P as a property P′ on monads;

3. Represent ⊕ by an operation on monads;

4. Show that the operation on monads preserves P′.

Along the way, we have to show that each of these steps is correct. Then we have reduced the syntactic modularity to a semantic modularity problem.

5.1 Semantics of Rewriting

This paper has sketched a semantics for TRSs as monads over the category Pre of pre-orders. However there are numerous generalisations of TRSs which are widely studied in the literature. The Kelly-Power framework also allows the modelling of equational rewriting and conditional rewriting. A rather more distant area, which is currently being investigated, is infinitary rewriting via a co-algebraic semantics.

To show correctness of this step, we show that for a discrete pre-order X, the term reduction algebra T_{A}(X) is isomorphic to the many-step reduction algebra ↠_{R} [Lüth, 1998, Lüth and Ghani, 1997].

5.2 Monadic Version of Rewriting Properties

Properties such as confluence and strong normalisation are easily formalised for pre-orders. Then a monad T satisfies a property P if its action T preserves it, i.e. T ⊧ P iff (X ⊧ P implies T (X) ⊧ P). To show correctness of this definition we have to show it is equivalent to the usual formulation of these properties, i.e. T_{R} ⊧ P iff R ⊧ P. This may not be totally straightforward, and depends upon showing that the variable rewrites do not interfere with the rewrites generated by the rewrite rules. For confluence and strong normalisation, this equivalence has already been established in [Lüth, 1998, Lüth and Ghani, 1997].

5.3 Combining Monads

A semantics is called compositional if it is compatible with the structuring operations — the semantics of the whole can be built from the semantics of its parts. Here, the semantics for TRSs is a left adjoint, with the right adjoint given by the internal language. Most structuring operations (such as the disjoint and non-disjoint union) are colimits, and since left adjoints preserve colimits, our semantics is always compositional.

Our research has so far concentrated upon the simplest structuring operation, namely the disjoint union of TRSs which categorically is the coproduct. Hence we need a concrete construction of the coproduct of two monads. As motivation, consider the terms built in the disjoint union of two (ordinary) signatures Ω, Σ. Such terms have an inherent notion of layer, that is one can decompose a term constructed from symbols in the union of two disjoint signatures into a term constructed from symbols in only one signature and strictly smaller subterms whose head symbols are from the other signature. Thus terms built from operations of Ω + Σ are contained in

T_{Ω+Σ}(X) = \begin{matrix}X + T_{Ω}(X) + T_{Σ}(X) + T_{Ω}T_{Σ}(X) + T_{Σ}T_{Ω}(X)+ \\ T_{Ω}T_{Σ}T_{Ω}(X) + T_{Σ}T_{Ω}T_{Σ}(X) + … \end{matrix}  (1)

However this disjoint union is too large as e.g. each component of the sum in equation (1) contains a separate copy of the variables X. Therefore, this sum is quotiented by taking the colimit of a diagram D_{X}; abstractly, D_{X} can be seen as the description of a way in which rewrites from the component systems are combined.

For this construction it is crucial that the monadic semantics allows to build terms over other terms. In this way, the concept of a monad precisely captures the notion of layers which is central to modularity proofs.

5.4 Monadic Modularity Proofs

We have now reduced modularity P for a structuring operation ⊕ on term rewriting systems to the equivalent problem of modularity of a property P′ for a structuring operation of monads. For the coproduct of monads, we know how to express this coproduct pointwise as the colimit of a diagram D_{X} at every pre-order at X.

By reducing a syntactic problem to a semantic one, we can apply the methods of category theory. Since the monadic properties are defined in terms of preservation of a property of the objects of the base category, we know by induction that all the objects of the diagram D_{X} — all summands of (1) — satisfy P′. It remains to be shown that it is preserved by passing to the colimit. Since any colimit can be given by coproducts and coequalisers, this means that proving that e.g. the colimit of D_{X} preserves confluence can be reduced to proving that coproducts and coequalisers (in Pre) preserve confluence. For coproducts this is easy, while for coequalisers this requires some work. Here, the variable rewrites come in very useful as they allow to specify the rewrites in the lower layers, and thus abolish the distinction between inner and outer reductions [Klop et al., 1994]. This way, categorical modularity proofs for confluence and SN have been given in [Lüth, 1998, Lüth and Ghani, 1997].

To sum up this section, we have demonstrated how the monadic approach can be used for modularity problems. The semantics gives us a clear road-map how to approach the problem, by reducing the syntactic modularity problem to a semantic one.

6 Conclusion and Outlook

This paper has started with the claim that term rewriting needs a semantics at an intermediate level of abstraction between the reductions generated by the syntax, and abstract reduction systems based on relations. By following through the analogy between universal algebra and term rewriting systems, we gave a semantics for term rewriting systems, both in an explicit form (the term reduction algebra) and a more general form (generalised algebraic theory) based on enriched monads.

This semantics has also provided us with new insights, and different perspectives of rewriting. Some of these have turned out to be useful in proofs, such as the functionality of the semantics, the variable rewrites and the compositionality; some of these remain mere observations at the moment, such as considering rewrite rules as constructors rather than oriented equations, and the rôle of the variables and the arities. Finally, the semantics also gives us new syntactical insights, such as the generalised rewrite rules and the quotes which distinguish a term from a variable and considerably simplify syntactic proofs of modularity.

For future work, the flexibility of the framework allows many generalisations, some of which (conditional and equational rewriting) have already been intimated above; others include formalising graph rewriting and persistence problems. As for modularity, structuring operations other than the coproduct can be considered.

Of course, the monadic semantics has its limitations. Presently variable bindings and higher-order rewriting systems fall out of their scope, though there are indications how to cover the former [Fiore et al., 1999].

References

[Baader and Nipkow, 1998] Baader, F. and Nipkow, T. (1998). Term Rewriting and All That. Cambridge University Press.

[Fiore et al., 1999] Fiore, M., Plotkin, G., and Turi, D. (1999). Abstract syntax and

variable binding. In Proc. LICS’99. To appear. [Ghani, 1995a] Ghani, N. (1995a). Adjoint Rewriting. PhD thesis, University of Edin-

burgh. [Ghani, 1995b] Ghani, N. (1995b). βη-equality for coproducts. In Second Conference

on Typed Lambda Calculus and its Applications, Edinburgh. [Hindley and Seldin, 1986] Hindley, J. R. and Seldin, J. P. (1986). Introduction to

Combinators and λ-Calculus. Number 1 in London Mathematical Society Student Texts. Cambridge University Press.

[Jay, 1990] Jay, C. B. (1990). Modelling reductions in confluent categories. In Proceed-

ings of the Durham Symposium on Applications of Categories in Computer Science. [Kelly, 1982] Kelly, G. M. (1982). Basic Concepts of Enriched Category Theory, vol-

ume 64 of London Mathematical Society Lecture Note Series. Cambridge University Press.

[Kelly and Power, 1993] Kelly, G. M. and Power, A. J. (1993). Adjunctions whose counits are coequalizers, and presentations of finitary monads. Journal for Pure and Applied Algebra, 89:163– 179.

[Klop, 1992] Klop, J. W. (1992). Term rewriting systems. In Abramsky, S., Gabbay, D. M., and Maibaum, T. S. E., editors, Handbook of Logic in Computer Science, volume 2 (Background: Computational Structures), pages 1–116. Oxford University Press.

[Klop et al., 1994] Klop, J. W., Middeldorp, A., Toyama, Y., and de Vrijer, R. (1994).

A simplified proof of Toyama’s theorem. Information Processing Letters, 49:101–109. [Knuth and Bendix, 1970] Knuth, D. and Bendix, P. (1970). Simple word problems in

universal algebra. In Leech, J., editor, Computational Problems in Universal Algebras, pages 263–297. Pergamon Press.

[Lüth, 1998] Lüth, C. (1998). Categorical Term Rewriting: Monads and Modularity.

PhD thesis, University of Edinburgh. [Lüth and Ghani, 1997] Lüth, C. and Ghani, N. (1997). Monads and modular term

rewriting. In Moggi, E. and Rosolini, G., editors, Category Theory and Computer Science, number 1290 in Lecture Notes in Computer Science, pages 69– 86, Santa Margherita Ligure, Italy. Springer Verlag.

[Mac Lane, 1971] Mac Lane, S. (1971). Categories for the Working Mathematician,

volume 5 of Graduate Texts in Mathematics. Springer Verlag. [Manes, 1976] Manes, E. G. (1976). Algebraic Theories, volume 26 of Graduate Texts

in Mathematics. Springer Verlag. [Robinson, 1994] Robinson, E. (1994). Variations on algebra: monadicity and gener-

alisations of equational theories. Technical Report 6/94, Sussex Computer Science Technical Report.

[Rydeheard and Stell, 1987] Rydeheard, D. E. and Stell, J. G. (1987). Foundations of equational deduction: A categorical treatment of equational proofs and unification algorithms. In Category Theory and Computer Science, number 283 in Lecture Notes in Computer Science, pages 114– 139. Springer Verlag.

[Seely, 1987] Seely, R. A. G. (1987). Modelling computations: A 2-categorical framework. In Proceedings of the Second Annual Symposium on Logic in Computer Science, pages 65–71.

[Stell, 1994] Stell, J. G. (1994). Modelling term rewriting systems by Sesqui-categories. Technical Report TR94-02, Keele Unversity.