Rewriting the Conditions in Conditional Rewriting

Neil Ghani  Christoph Lüth  Stefan Kahrs
University of Leicester  Universität Bremen  University of Canterbury

     ng13@mcs.le.ac.uk    cxl@informatik.uni-bremen.de     S.Kahrs@ukc.ac.uk

August 30, 2000

Abstract

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. Recently we have developed a semantics for TRSs using monads which generalises the equivalence between algebraic theories and finitary monads on the category Set. This semantics underpins the recent categorical proofs of state-of-the-art results in modular rewriting.

We believe that our methods can be applied to modularity for conditional rewriting where several open problems exist. Any results we achieve here would be highly significant as, for the first time, substantial open problems in rewriting would have been solved using categorical techniques. This paper reports on the first step in this project, namely the construction of a semantics for CTRS using monads. ^{1}

1 Introduction

Term Rewriting Systems (TRSs) are widely used throughout computer science as they form an abstract model of computation while retaining a relatively simple and concrete syntax. TRSs originally arose in the study of the λ-calculus and combinatory logic and have, more recently, played a prominent role in the design and implementation of functional programming languages and in the theory of algebraic data types. In a different direction, TRSs are widely used in formal reasoning as TRSs which are strongly normalising and confluent provide decision procedures for equational theories.

A TRS consists of a set of rules for generating transformations, or rewrites, of the terms of a formal language and intuitively each rewrite is conceptually simple and easy to reason about while combinations of rewrites can model complex phenomena. The concreteness of TRSs has led to a tendency to concentrate on the technical details of specific problems to the detriment of a wider understanding of the subject and a proper interaction with other disciplines in computer science. Abstract models of TRSs have been developed to address this problem with the simplest being the Abstract Reduction Systems (ARSs) based upon relations. While useful for certain results, eg Newmann’s Lemma and the Commutation Lemma, ARSs do not posses enough structure to adequately model key concepts such as substitution, context, layer structure etc which arise in more complex problems such as modular rewriting. Hence ARSs are mainly used as an organisational tool with the difficult results proved directly at the syntactic level.

1Technical Report No. 2000/89, Department of Mathematics & Computer Science, University of Leicester, University Road, Leicester LE1 7RH, England. \begin{matrix}c \\ ◯ \end{matrix} University of Leicester, 2000.

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 [16, 17], Sesqui-categories [18] and confluent categories [3]. However, despite some one-off results [2, 16], these approaches have yet to make a lasting impact on term rewriting. Part of the problem seems to be that the semantics is actually constructed “set-theoretically” and hence reasoning about the semantics often involves set-theoretic reasoning. This often looks like translating the problem back into the syntax!

An alternative approach starts from the observation that term rewriting systems can be regarded as generalisations of algebraic theories. 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. Sice the categorical treatment of algebraic theories is based upon finitary monads on the category Set, it is natural to model a TRS by a monad over a more structured base category. Lüth and Ghani have used this monadic semantics to give categorical proofs of the modularity of confluence and strong normalization [9, 8].

Conditional term rewriting systems (CTRSs) are generalisations of TRSs which allow restrictions to be imposed on when a rewrite is permissible. An example of a conditional rewrite rule is the following

l ⇒^{∗} r ⊢ s ⇒ t

which allows s to rewrite to t providing we have already established that l rewrites to r. CTRSs arise naturally in the semantics of logic and functional programming languages and in structural operational semantics. We believe that our proofs of modularity for TRSs using monads can be generalised to CTRSs where several open problems exist. Any results we achieve would be highly significant as, for the first time, substantial open problems in rewriting would have been solved using categorical techniques. Towards our overall goal, this paper asks the question can conditional term rewriting systems be modelled by monads. The main contributions of this paper are:

• We answer the above question affirmatively. This is rather unexpected as, at first glance, CTRSs have the flavor of essentially algebraic theories which are strictly more general than theories modelled by monads. The key idea is to replace monads over Pre with monads over ordered Σ-algebras (where Σ is the signature of the CTRS). The conditionality in CTRSs is then replaced by the use of more complex arities for operations which are afforded by the use of this more complex base category.

• The usual semantics of a CTRS is the rewrite relation generated by the CTRS.

Unfortunately this semantics is not compositional as the following example shows. Let A, B, C, D be constants. Consider the following conditional rewrite rules

R_{1} :  ⊢ A⇒B
R_{2} : A⇒^{∗}B ⊢ C⇒D
R_{3} : A⇒^{∗}C ⊢ C⇒D

Then R_{2} and R_{3} have the same interpretations, ie the empty relation. But the CTRS R_{1} ∪ R_{2} has C⇒D, while the CTRS R_{1} ∪ R_{3} does not. Such a noncompositionality is clearly undesirable. Most strikingly, a non-compositional semantics makes a compositional investigation of properties very awkward.

• There are several different notions of CTRS in the literature, each corresponding to a different definition of what form a condition may have. The categorical methodology suggests a new notion of condition which subsumes most of those occurring in the literature. Our semantics therefore provides a unifying framework for studying CTRSs.

• Finally the theoretical basis of this research is the work of Kelly and Power in generalizing the equivalence between algebraic theories and finitary monads on the category of Set to more general categories. This theory was originally developed to study categories with extra structure. By providing a natural application within computer science, we hope to make their work more accessible to the computer science community.

The rest of the paper is divided as follows. In section 2 we standardise notion for the rest of the paper while in section 3 we briefly review the equivalence between algebraic theories and finitary monads on the category Set. Section 4 presents TRSs and gives a concrete semantics for TRSs using monads over the category Pre and this semantics is explained in section 5 in terms of the Kelly Power framework. Section 6 introduces CTRSs and section 7 discusses their semantics. We finish in section 8 with our conclusions and further work.

2 Notation and Preliminaries

The natural numbers are denoted ℕ. A pre-order is a pair ⟨X, ≤⟩ where X is a set and ≤⊆ X × X is a reflexive, transitive relation. We use the following conventions for variables: P, Q for pre-orders, X, Y, Z for sets, A, B for algebras, C, D for categories, and Σ for signatures. If P is a pre-order, its carrier set is denoted |P | and its order relation is denoted ⇒_{P} to emphasise the intuition that pre-orders model terms reducing to other terms. For the sake of legibility, and also to emphasise the logical nature of our inductive constructions over pre-orders, we write P ⊧ x⇒y if x, y ∈ P and x⇒_{P} y. We write 0, 1, 2, … for the finite discrete pre-orders, the elements of which we denote as x_{1}, x_{2}, . . .. When we need to draw pre-orders we will enclose the pre-order in brackets, either using letters or the symbol ∘ to represent elements of the carrier set and use arrows to denote when one element is related to another. Arrows which can be inferred from the reflexivity and transitivity of the order relation are omitted. The symbol ↓ denotes the preorder with two elements which are related in the order.

We assume the reader is familiar with the basic concepts of category theory and enriched category theory. The basic theory of monads over categories with more structure than Set has been developed by Kelly and Power [6] and forms the theoretical basis of this research. However, we dont consider familiarity with their work a pre-requisite for this paper. Rather, the concrete construction of representing monads for algebraic theories and for TRSs given in the next two sections should allow the reader to follow the rest of the paper.

3 Universal Algebra and Monads

Definition 1 (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_{C} ⇒ T, called the unit, and μ : T T ⇒ T, called the multiplication of the monad, satisfying the monad laws: μ.T η = 1_{C} = μ.η_{T}, and μ.T μ = μ.μ_{T}.

The monadic approach to term rewriting generalises the well known equivalence between (finitary) monads on the category Set and universal algebra. Thus, in order to motivate our constructions, we begin with a brief account of this equivalence. However, since this material is standard category theory, we omit most proofs and instead refer the reader to the standard references ([11], [15] and [10, Section VI]).

Every algebraic theory defines a monad on Set whose action maps a set to the free algebra over this set. The unit maps a variable to the associated term, while the multiplication describes the process of substitution. The monad laws ensure that substitution behaves correctly, i.e. substitution is associative and the variables are left and right units. Thus monads form an abstract calculus for equational reasoning where variables, substitution and term algebra (represented by the unit, multiplication and action of the monad) are the primitive concepts. We now make these ideas precise.

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

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

Var {x ∈ X \atop 'x ∈ T_{Σ}(X)}  Op\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 categorically inspired idea turns out to considerably simplify modularity proofs and hence is a nice example of a benefit to rewriting arising from its categorical semantics.

Lemma 1 The map X ↦ T_{Σ}(X) defines a monad T_{Σ} on Set.

The monads arising via the term algebra construction satisfy an important continuity condition, namely they are finitary. To understand this condition, the term algebra T_{Σ}(X) built over on an infinite set X of variables can be given as

T_{Σ}(X) = ⋃_{X_{0}⊂X is finite} T_{Σ}(X_{0})

This equation holds since all the operators in Σ have a finite arity and so a term built over X contains only a finite number of variables — such terms are therefore built over a finite subset of X. Categorically this is expressed by saying the functor T_{Σ} is finitary:

Definition 4 (Finitary Monads) A functor is finitary iff it preserves filtered colimits [10]. A monad is finitary iff its action is finitary.

Lemma 2 If Σ is a signature, then T_{Σ} is finitary [15, Lemma 1.7].

Monads also model algebraic theories:

Definition 5 (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)/ _{E}

and hence we again obtain a finitary monad over Set. The category of algebras of this monad is equivalent to the category of models of A, justifying the correctness of the monadic semantics: “universal algebra is the study of finitary monads over Set” [11].

One key property of this monadic semantics for algebraic theories is that it is compositional. For the disjoint union of algebraic theories, this means T_{A_{1}+A_{2}} ≅ T_{A_{1}} + T_{A_{2}}. This compositionality property is established by showing that every finitary monad arises from an algebraic theory called the internal language of the monad. Since the monadic semantics is left adjoint to the internal language construction, compositionality follows from the fact that left-adjoints preserve colimits.

In summary, monads provide a semantics for algebraic theories with the concepts of term-algebra, variable and substitution taken as primitive.

4 Categorical Rewriting

Rewriting systems consist of rules for transforming the terms of a formal language. Intuitively, each rule is “local”, conceptually simple and easy to reason about while sequences of rewrites can model complex effects. We now briefly review the theory of TRSs — our presentation differs slightly from traditional presentations [7] so as to allow a smoother development of the categorical semantics. The main differences are as follows:

• Traditionally one uses a set of variables but, as our semantics for TRSs is based upon monads over Pre, our variables must form a preorder. The carrier set of this preorder are the usual variables which are used to form terms while the order relation allows variables to rewrite to other variables.

• In addition, one usually fixes the variables at the outset. However, as the action of the representing monad of a TRS should map any pre-order (thought of as variables and variable rewrites) to a pre-order (thought of as terms and rewrites between them), we allow the pre-order of variables to vary.

• The last point also applies to rewrite rules, which are usually defined as l⇒r (with the set of variables fixed). Here, every rewrite rule has a context (which is of course not merely a set, but a pre-order of variables). The context is the arity of the rewrite rule and emphasizes our view of rewrite rules as operations, rather then directed equations.

• Traditionally, the semantics of a TRS is a relation, either the one-step rewrite relation or the many many-step rewrite relation. Rather than give the semantics of a TRS as a relation, our monadic semantics interprets a TRS as a special kind of function (ie a monad) which maps pre-orders (thought of as variables and variable rewrites) to pre-orders (thought of as terms and rewrites between them).

Each of these categorically inspired generalisations of rewriting has been applied to syntactic formulations of rewriting and, in particular, has lead to a significant simplification of modularity proofs. This is strong empirical evidence that our categorical models really do advance our understanding of rewriting.

Definition 6 (Rewrite Rules and Term Rewriting Systems) Let Σ be a signature. A Σ-rewrite rule is of the form X ⊢ l⇒r where X is a finite pre-order and l, r ∈ T_{Σ}(|X|). A TRS Θ = ⟨Σ, R⟩ consists of a signature Σ and a set R of Σ-rewrite rules.

Example 1 (Addition) The TRS for addition presented in the introduction formally consists of the signature Σ where

Σ(0) = {0}  Σ(1) = {S}  Σ(2) = {+}

and has as Σ-rewrite rules {r_{1}, r_{2}} where

\begin{aligned}r_{1} : & \{x\} & ⊢ & 0 + x & ⇒ & x \\ r_{2} : & \{x, y\} & ⊢ & Sx + y & ⇒ & S(x + y) \end{aligned}

Given a TRS one usually defines the one-step reduction relation and then the many step reduction relation which is the reflexive-transitive closure of the one-step reduction relation. As indicate above, our presentation of rewriting does not interpret a TRS as a relation, but as a function on relations. In addition, we take the many-step reduction relation as being of primary importance since it is usually this relation that one wants to reason about. Thus we define a term reduction algebra in Table 1 which takes a pre-order P of variables and rewrites between them and returns a pre-order T_{Θ}(P) of terms and rewrites between them. This term reduction algebra is the direct generalisation of the term algebra construction (Def. 3) which takes a set of variables X and returns a set of terms T_{Σ}(X). Just as the term algebra construction defines a monad over Set, so the term algebra construction defines a monad over Pre.

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

Let X be a pre-order. Then define the pre-order T_{Θ}(X) as follows

• T_{Θ}(X) has the carrier set T_{Σ}(|X|)

• T_{Θ}(X) has the least pre-order generated by the following rules:

[Var] {X ⊧ x ⇒ y \atop T_{Θ}(X) ⊧ 'x⇒'y}

[Cong] {T_{Θ}(X) ⊧ t_{1}⇒s_{1}, …, t_{n}⇒s_{n} \atop T_{Θ}(X) ⊧ f(t_{1}, …, t_{n})⇒f(s_{1}, …, s_{n})} f ∈ Σ_{n}

[Inst] {(Y ⊢ l⇒r) ∈ R,  σ : Y →T_{Θ}(X) \atop T_{Θ}(X) ⊧ lσ⇒rσ}

Lemma 3 The map X ↦ T_{Θ}(X) defines a finitary, Pre-enriched monad T_{Θ}.

Proof. The proofs follow those for algebraic theories, but we also have to show that η and μ preserve the order. To show T_{Θ} is Pre-enriched, we have to show it preserves the pointwise order on morphisms. See [9] for more details. □

Lemma 3 shows that we can model TRSs by monads over Pre. Although this semantics is powerful enough to prove state-of-the-art results in modular rewriting, it is unsatisfactory in a number of ways. Firstly, the semantics is a set-theoretic construction and proofs about the semantics will consequently use induction on the term structure; secondly, the semantics assumed various choices, eg the choice of base category, and if we change any of these, lemma 3 needs reproving. Thirdly, although we have given a mathematical account of the similarity of algebraic theories and TRSs at the semantics level, we have so far failed to justify our claim that they are similar at the syntactic level. Finally, given that many semantics exist for TRSs, is there any reason to believe the monadic semantics is preferable. In addition to the empirical evidence given by the results in modular rewriting we have achieved using monads, we would also prefer some more theoretical reasons to believe in the “canonicity” of the monadic semantics. These questions are answered by the theory of enriched monads to which we turn now.

5 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 [6] 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 algebra, and equations. In this section we briefly explain the Kelly-Power framework using algebraic theories and TRSs to motivate the general constructions. Then in section 7 we apply the Kelly-Power framework to derive a monadic semantics for CTRSs.

5.1 Generalised Signatures

Recall from definition 2 that a signature is a function Σ : ℕ→Set — that is for each arity n, there is a set of operations Σ(n). To define signatures for a category C it is natural to replace the idea of a set of operations by a C object of operations, i.e. change the codomain of Σ to C. As for the domain of Σ, the key point about the natural numbers is that they represent the isomorphism classes of finite sets presentable objects. Finite sets correspond to the finitely presentable objects Cfp (or fp-objects) of C. Hence, we replace ℕ by a set N ⊆ Cfp of fp-objects which represent isomorphism classes of fp-objects of C:

Definition 7 (Generalised Signatures) If C is a category, then a C-signature is a map Σ : N →C.

A pre-order is finitely presentable iff its carrier set is finite; the set N are essentially finite ordinals which may additionally have an order on the objects. Hence if we present a TRS as a generalised signature Σ, the signature will map a pre-order P ∈ N 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 offers a new perspective of treating rewrite rules as constructors in their own right as opposed to the more traditional view of rewrite rules as oriented equations.

Example 2 (Addition cont’d) The addition TRS has the following operations with associated arities

Operation 0 S + r_{1} r_{2}
Arity  0 1 2 1 2

The associated Pre-signature R : |Pre_{fp}|→Pre is

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

Since the arity of the rewrite rule r_{1} is the discrete 1-element pre-order, 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 summarise, when we 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}. Equality of e.g. s_{1} with the source of the actual rule 0 + x will be enforced by equations.

5.2 Generalised Term Algebras

The generalised term algebra construction should map an object of C, thought of as variables, to another object of C which we think of the terms built over the variables. Recall that the term algebra of an algebraic theory was defined inductively by the clauses Var and Op in Def. 3. We can replace t_{1}, … t_{m} ∈ T_{Σ}(X) in Op by a function θ : m→T_{Σ}(X) where m is the m element set or, equivalently, an element of [m, T_{Σ}(X)]. Further, as the term algebra is defined inductively, it is limit of the chain T_{0}(X) ↪ T_{1}(X) ↪ … where

T_{0}(X) = X  \begin{matrix}f ∈ Σ(m) & θ : [m, T_{n}(X)] \\ fθ ∈ T_{n+1}(X) \end{matrix}

Writing this more abstractly, and crucially isolating the rôle of Set:

T_{0}(X) = X  T_{n+1}(X) = X + ∑_{m∈Nat}[m, T_{n}(X)] × Σ(m)

This formulation of the term algebra construction makes explicit the structure of Set which is used and, consequently, suggests that we should define the generalised term algebra as follows

Definition 8 (Generalised Term Algebra:) Let Σ be a C-signature and X an object of X. Then define T_{Σ}(X) = colim T_{0}(X) ↪ T_{1}(X) ↪ …

T_{0}(X) = X
T_{n+1}(X) = X + ∑_{c∈C_{fp}} C(c, T_{n}(X)) ⊗ Σ(c)

In its most general form, the Kelly-Power framework considers a category C enriched over a category V. Then, the map X ↦ T_{Σ}(X) extends to a finitary, V-enriched monad on C. In this case, ⊗ is the co-power or tensor, that is we have C(U ⊗ A, B) ≅ [U, C(A, B)] natural in B in C. Thus the term algebra T_{Σ}(X) depends on not just the category C, but also the choice of enrichment. When modeling TRSs, we can consider Pre as enriched over Set or Pre as being enriched over Pre. To understand the consequences of the different choices of enrichments, consider a term constructor f of arity c and c-tuples of terms θ_{1}, θ_{2} : c→T_{n}(X):

• With enrichment over Set, [c, T_{n}(X)] is the set of monotone functions from the preorder c to the pre-order T_{n}(X). Thus, even if θ_{1}⇒θ_{2}, there is no forced relationship between the terms fθ_{1} and fθ_{2}. Consequently, reduction is not forced to be a congruence.

• With enrichment over Pre, [c, T_{n}(X)] is a pre-order of monotone functions. Consequently, if θ_{1} ≤ θ_{2}, then fθ_{1}⇒fθ_{2}. Therefore, enrichment over Pre forces reduction to be a congruence.

In most rewriting (including the version presented in this paper) reduction is considered to be a congruence and hence we always work with Pre-enriched structures. But it is re-assuring to know that if we wanted to study a non-congruent reduction relation, eg in the theory of eta-expansions [2, 4], we need only change the enrichment. Of course C and V must satisfy certain properties for Def. 8 to make sense. However, we delay a discussion of this until after we have introduced the generalisation of equations.

5.3 Generalised Equations and Generalised Algebraic Theories

Thus, every signature Σ : N → C gives us a monad. Conversely, every finitary monad gives a signature by precomposing the action with the inclusion N ↪ C. These two mappings form an adjunction

[N , C] [figure: T_{−}; ⊥] Mon_{Fin}(C)  (1)

between the category of signatures (functors from N to C) and finitary monads over C.

Definition 9 (Generalised Algebraic Theory) A generalised algebraic theory A = ⟨Σ, E⟩ is given by a generalised signature Σ, and equations which are given by a function E : N → C together with a family of pairs of maps

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

The idea is that E specifies the shape of the equations while the maps σ and τ specify the left-hand side and right hand side of the equations respectively. In the case of TRSs, we want to equate the formal sources and targets introduced by the generalised signature with the actual sources and targets of the rewrite rules. Intuitively this means writing

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

To translate these intuitive equations into the generalised equations of Def. 9 note that the carrier set of E(1) will contain one element for every equation of arity 1 between terms while the order relation of E(1) will specify equations of arity 1 between the rewrites. Similar comments hold for E(2). Since there are two equations of arity 1 between terms, and two equations of arity 2 between terms, we set E(1) = E(2) = 2. Consequently, the maps σ_{1} and τ_{1} consist of a pair of elements of T_{Σ}(1), and similarly for σ_{2} and τ_{2}:

\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}

Given an algebraic theory, the maps σ, τ : E(c) → T_{Σ}(c) in [N , C] have conjugates σ′, τ′ : T_{E}(c) → T_{Σ}(c) in Mon_{Fin}(C). The monad T_{A} representing is the coequaliser of σ′ and τ‘ in Mon_{Fin}(C). The main theorem of the Kelly and Power [6] is that every finitary monad can be represented as a coequaliser of two such morphisms, and thus every monad arises from a generalised algebraic theory.

Theorem 1 (Kelly-Power) Let C be a locally finitely presentable category enriched over the locally finitely presentable symmetric monoidal closed category V. Then

• Every C-algebraic theory A = ⟨Σ, E⟩ is represented by a finitary V-enriched monad T_{A}.

• Every finitary V-enriched monad on C arises from a C-algebraic theory.

We leave the reader to consult the literature [5] for the precise definition of a locally finitely presentable category in the enriched context. For our purposes, Pre is both lfp, and lfp as a closed category.

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 constructors (both terms and rewrites) may have non-discrete arities and we could write equations between any two terms, thus modeling equational rewriting.

6 Conditional Term Rewriting Systems (CTRSs)

Conditional rewriting allows conditions to be imposed on when a rewrite is permissible. There are various different types of CTRS depending on the exact nature of the conditions which may be imposed. We now briefly review the theory of CTRSs — more details may be found in [7]. Again our presentation differs slightly from traditional formulations in that we parameterise each conditional rewrite rule by a pre-order of variables.

Definition 10 (Conditional Term Rewrite Systems) Let Σ be a signature. A Σconditional rewrite rule is of the form

X, l_{1} ∼ r_{1}, …, l_{n} ∼ r_{n} ⊢ l⇒r

where X is a finite pre-order and l_{i}, l, r_{i}, r are all members of T_{Σ}(|X|). A Σ-CTRS consists of a set of Σ-conditional rewrite rules.

In the literature there are several standard interpretations of ∼, each of which leads to a different notion of CTRS.

• Join-CTRSs: The relation ∼ is called joinability and t ∼ u iff t and u have a common reduct. In this case we write t ⇓ u.

• Semi-equational CTRSs: The relation ∼ is interpreted as being equivalent in the associated equational theory. In such circumstances we write t ⇔^{∗} u

• Reduction CTRSs: The relation ∼ is interpreted as many-step reduction. In such circumstances we write t ⇒^{∗} u

Of course, there are many other possible interpretations of the relation ∼. Our semantics covers most interpretations of ∼ and hence provides a unifying framework for the study of many of the CTRSs which occur in the literature. In order to avoid committing ourselves to a particular notion of CTRS we will in future write Σ-conditional rewrite rules as

Y, C ⊢ l⇒r

where Y is a pre-order, l, r ∈ T_{Σ}(|Y |) and C is some relation on T_{Σ}(|Y |)

Defining the reduction relation of a CTRS is slightly more delicate than in the unconditional case, since it is not enough to close each rewrite rule is closed under substitutions and contexts. We further have to look at the rewrites already constructed, check whether the conditions of a rewrite rule are met, and if so add the conclusion of the rewrite rule to the rewrite relation. Thus, we take a rewrite relation, and add in more rewrites, if the conditions are satisfied; this gives the whole semantics a rather functional flavor.

Definition 11 (Reduction for CTRSs) Given a Σ-CTRS Θ, and a pre-order X, the conditional reduction algebra T_{Θ}(X) is defined in Table 2.

7 Can CTRSs be Modelled by Monads?

Since TRSs can be modelled by monads, a natural question is whether a CTRS can be modelled by a monad. To answer this question, recall that each rewrite rule of a TRS is treated as an operation of a generalised signature and that for the TRSs one usually considers, these arities are discrete. However the theory of enriched monads allows arities for rewrite rules to be non-discrete pre-orders and this leads to a limited form of CTRSs where each term in the conditions is a variable.

Example 3 Let Σ be the signature consisting of a nullary function symbol T and a binary function symbol eq. The Σ-conditional rewrite rule

x⇒z, y⇒z ⊢ eq(x, y)⇒T

Table 2: The Conditional Term Reduction Algebra for a Σ-CTRS Θ

Let X be a pre-order. Then define the pre-order T_{Θ}(X) as follows

• T_{Θ}(X) has the carrier set T_{Σ}(|X|)

• T_{Θ}(X) has the least pre-order generated by

[Var] {X ⊧ x ⇒ y \atop T_{Θ}(X) ⊧′ x⇒′y}

[Cong] \begin{matrix}T_{Θ}(X)(t_{1}⇒s_{1}), …, T_{Θ}(X)(t_{n}⇒s_{n}) \\ T_{Θ}(X) & ( & f(t_{1}, …, t_{n})⇒f(s_{1}, …, s_{n}) & ) \end{matrix} f ∈ Σ_{n}

[Inst] \begin{matrix}(Y, C ⊢ l⇒r) ∈ R,  σ : Y →T_{Θ}(X),  T_{Θ}(X)(C) \\ T_{Θ}(X) & ( & lσ⇒rσ & ) \end{matrix}

can be given as an operation with arity the pre-order (x⇒z ⇐ y). This is because a monotone map θ : (x⇒z ⇐ y)→T_{Θ}(X) will consist of three terms θ(x), θ(y) and θ(z) and monotonicity will force θ(x) and θ(y) both to rewrite to θ(z).

To model more general forms, where the conditions in the rewrite rules pertain not merely to variables but rather to arbitrary terms, one could imagine trying to use equations to model CTRSs with arbitrary conditions as a quotient of CTRSs whose conditions pertain solely to variables. However, this would betray a fundamental misunderstanding of the universality of universal algebra. The key point is that a conditional rewrite rule is an operation whose domain is restricted by the conditions, just like e.g. composition of morphisms in category is an operation which is defined only if the target of the first morphism equals the source of the second. Theories containing operations whose domains are (equationally) restricted are examples of essentially algebraic theories.

The construction of a monadic semantics for CTRSs will proceed in three essential steps. First, we give a straightforward semantics of CTRSs as functions over rewrite relations. Since rewrite relations are not suitable as a base category, we reformulate this semantics as a function over ordered algebras, which can then be made into a monad. Continuing the analogy above, categories can be presented by a monad, but over the category Grph of graphs, not over Set; and CTRSs can also be modelled by a monad, but over a base category which is rich enough to model the conditions uniformly.

7.1 CTRSs as Ordered Σ-Algebra Transformers

Although not defining a monad, we can view a CTRS Θ as a function [[Θ]] which maps a relation on terms to a relation on terms. In order to meaningful evaluate the conditions of the conditional rewrite rules, these relations need to closed under substitution and contexts. Such relations are called rewrite relations [1], and we write Rew(Σ, X) for all rewrite relations over T_{Σ}(X).

But even if we can define a function [[Θ]] : Rew(Σ, X)→Rew(Σ, X) for a CTRS Θ, this does not define a monad. Moreover, the rewrite relations do not form a good base category for our purposes: firstly they are very syntactic, since they are relations on terms; secondly, their categorical properties are not explored very well; and finally, we still need to deal with the conditional clause Inst in Table 2. In order to meet these problems, we replace rewrite relations with ordered Σ-algebras.

First we need to defined ordered Σ-algebras. There are three equivalent definitions — proofs of the equivalence can be found in e.g. [14].

Definition 12 (Ordered Σ-Algebras) Let Σ be a signature. An ordered Σ-algebra is one of:

• A pre-order P and, for every f ∈ Σ(n), a monotone map f_{A} : A^{n}→A. If A is an ordered Σ-algebra, then its carrier set is written |A| and is defined to be the carrier set of P.

• An algebra T_{Σ}A ⟶^{α} A of the Pre-enriched monad T_{Σ} : Pre→Pre, which is the representing monad of the TRS Σ = ⟨Σ, ∅⟩ whose signature is Σ and which contains no rewrite rules.

• A FP-functor from Th(Σ) to Pre, where Th(Σ) is the Pre-enriched Lawvere theory of Σ.

The category of ordered Σ-algebras is denoted Σ-OAlg. The free and forgetful functors between Σ-OAlg and Pre are denoted F_{Σ} and U_{Σ}

Pre [figure: F_{Σ}; ⊥; \underline{U_{Σ}}] Σ-OAlg  (2)

where F_{Σ} maps any preorder X to the free ordered Σ-algebra, and U_{Σ} maps any algebra to its carrier. Crucially, ordered Σ-algebras have enough structure to interpret the conditions arising in a CTRS. For this, if A is an ordered Σ-algebra T_{Σ}A ⟶^{α} A, and P a pre-order, then every map σ : P → A (thought of as a variable assignment) gives (under adjunction 2 rise to a homomorphic extension σ^{∗} : T_{Σ}(P), σ = α.T_{Σ}(σ). For l ∈ |T_{Σ}(P)| we denote the action of ϕ^{∗} on l as lϕ.

Definition 13 (Validation) An ordered Σ-algebra A validates a Σ-conditional rewrite rule (Y, C ⊢ l⇒r), if there exists σ : Y →A s.t. for each l⇒r ∈ C we have A ⊧ lσ⇒rσ; this is written as A ⊧_{σ} C.

We can now give a semantics to a CTRS as a map of ordered Σ-algebras in Table 3. Again, reflexivity of [[Θ]](A) follows from the rule [Var]. This semantics can now be turned into a monad, if we can remove the condition from rule Inst.

Table 3: A Semantics for CTRSs as ordered Σ-algebra-transformers

For a CTRS Θ = ⟨Σ, R⟩, [[Θ]] maps an ordered Σ-algebra A to the ordered Σ-algebra defined as follows:

• The carrier of [[Θ]](A) is the carrier of A.

• The order of [[Θ]](A) is defined inductively by

[Var] A is an ordered Σ-algebra A ⊆ [[Θ]](A)

[Inst] {X, C ⊢ l⇒r  σ : X→A  [[Θ]](A) ⊧_{σ} C \atop [[Θ]](A) ⊧ lσ⇒rσ}

[Cong] {[[Θ]](A) ⊧ l_{1}⇒r_{1}, …, [[Θ]](A) ⊧ l_{n}⇒r_{n} \atop [[Θ]](A) ⊧ f(l_{1}, …, l_{n})⇒f(r_{1}, … r_{n})} f ∈ Σ(n)

7.2 A Monadic Semantics for CTRSs

So far we have tried to give a semantics for CTRSs in terms of finitary monads over Pre and, when we found out this was not possible, we subsequently gave a semantics for CTRSs as ordered Σ-algebra-transformers. We now want to turn the ordered Σ-algebra-transformer into a monad over the category of ordered Σ-algebras. By changing to a more complex base category for the representing monad, the arities for operations now have a sufficiently rich structure to model CTRSs. However, instead of reasoning about pre-orders, we must now reason about ordered Σ-algebras.

A direct proof that a CTRS Θ can be modelled by a monad T_{Θ} : Σ-OAlg→Σ-OAlg would first extend the transformer [[Θ]] to an endofunctor [[Θ]] : Σ-OAlg → Σ-OAlg, construct the unit η_{A} : A → [[Θ]](A) (from the rule Var) and the multiplication μ_{A} : [[Θ]]^{2})A →→ [[Θ]](A), and then verify that these definitions satisfy the monad laws, and that [[Θ]] is finitary. This is a lot of work — not difficult but tedious.

Hence, a better alternative is to use the theory of enriched monads as described in Sect. 5. Therefore we will proceed as follows. First (7.2.1), we show that the category of ordered Σ-algebras satisfies the premises of the Kelly-Power framework as described in theorem 1. Then (7.2.2), we present each CTRS as an ordered Σ-algebra-theory. This amounts to defining each conditional rewrite rule as an operation whose arity is a finitely presentable ordered Σ-algebra. By theorem 1 this will define a Pre-enriched monad. Finally (7.2.3), we prove that the monadic semantics is actually correct, ie that it agrees with the ordered Σ-algebra-transformer semantics of section 7.1.

7.2.1 Preliminaries

Most of the results we require are (Pre-enriched versions of) well known results — we quote them here and provided references for proofs. Recall that we require properties of the category we are enriching over (here Pre) and properties of the base category of the monad (here Σ-OAlg). In addition, in order to associate arities to operations we need to know what the finitely presentable objects of Σ-OAlg are.

Lemma 4 The category Pre is a symmetric monoidal closed category and is lfp with respect to this closed structure.

Lemma 5 The category of Σ-OAlg is lfp. The set NΣ-OAlg representing isomorphism classes of fp-objects is represented as the coequaliser of [figure: F m; F n] where m, n are representing isomorphism classes of fp-objects in Pre.

Finally, tensors in Σ-OAlg are constructed with the following isomorphism:

P ⊗ F_{Σ}(P′) ≅ F_{Σ}(P × P′)  (3)

7.2.2 CTRSs as Generalised Theories

We now present a CTRS as a Σ-OAlg-theory. For the sake of clarity of our exposition, we focus for the time being on the CTRS containing the single conditional rewrite rule

R =^{def} (P, l⇒r ⊢ u⇒v)

At the end of this section we discuss the modifications required to treat more complex CTRSs. The most important question is refers to the arity of R which we shall henceforth denote ar(R). Intuitively, ar(R) should be the smallest ordered Σ-algebra such that the carrier of ar(R) is the carrier of F_{Σ}(P), and that ar(R) ⊧ l⇒r.

We now have construct such an ordered Σ-algebra, and moreover show it is finitely presentable.

Lemma 6 ar(R) is a finitely presentable ordered Σ-algebra presented as the coequalizer in Σ-OAlg of

F_{Σ}(2) [figure: σ; τ] F_{Σ}(P + ↓)  (4)

where σ =^{def} F_{Σ}(i) and i is the obvious composition of inclusions 2→ ↓ →P + ↓. To define τ, note that the pair of terms (l, r) define a map in Pre (l, r) : 2→T_{Σ}(P) = U_{Σ}F_{Σ}(P). Using the natural isomorphism of adjunction 2 this defines a map (l, r)^{∗} : F_{Σ}(2)→F_{Σ}(P). Finally define τ = F_{Σ}(ι) ∘ (l, r)^{∗} where ι : P →P + ↓ is the obvious inclusion.

Note that since ar(R) is presented by (4), by lemma 6 ar(R) is in NΣ-OAlg.

There are two points to remember when generalising the presentation of a TRS as a Pre-signature to the presentation of a CTRS as a Σ-OAlg-signature:

• Firstly, the use of Σ-OAlg as the base category of our monads means that the term constructors of the language have already been declared. This is in contrast to presentations of TRSs as Pre-signatures where the signature declares both the term and rewrite constructors.

• Secondly, given a TRS, each rewrite rule of arity P contributes the pre-order (⟶) to the operations of arity P. Unfortunately here we cannot simply write S(ar(R)) = (⟶) as the operations of a given arity must form an ordered Σ-algebra, and so have to use the free functor F_{Σ}.

Hence, the signature S : N_{Osalg}→Σ-OAlg for the CTRS Θ is given by

S(A) = F_{Σ}(↓) A = ar(R)
= F_{Σ}(0) otherwise

Again the need to have the operations of a given arity form a ordered Σ-algebra forces us to use the free functor F_{Σ}. The equations of the theory are used to ensure that no actually new term constructors are declared. These equations fall into two classes: firstly, those setting constructors introduced by F_{Σ} equal to their interpretation in their arity; secondly, those setting the source and target of rewrite rules must be set equal to u and v respectively.

Formally, the shape of the equations are defined by E : NΣ-OAlg→Σ-OAlg where

E(A) = F_{Σ}(2) A = ar(R)
= F_{Σ}(0) otherwise

which is the obvious generalisations of the equations used in the presentation of a TRS, incorporating the free functor F_{Σ}. Next, we define the maps σ_{A}, τ_{A} : E(A)⇒T_{S}(A) for A ∈ NΣ-OAlg by the following case distinction:

1. A = ar(R). Recall that our signature has declared term constructors s_{R} and t_{R} which we want to set to be the terms l and r. Since l, r are elements of the carrier set of T_{Σ}(P), they define a map (l, r) : 2→T_{Σ}(P) in Pre. This in turn defines a map (l, r)^{∗} : F_{Σ}(2)→F_{Σ}(P) which when postcomposed with the maps F_{Σ}(P)→ar(R)→T_{S}(ar(R)) defines σ. Since σ picks out the real source and target l and r of R, τ have to pick out the formal source and target constructors s_{R} and t_{R}. We construct a map F_{Σ}(2)→[ar(R), ar(R)]⊗ S(ar(R)) and then define τ to be the postcomposition of this map with the evident inclusion into T_{S}(ar(R)). Since S(ar(R)) = F_{Σ}(↓), by equation 3 this amounts to giving a map F_{Σ}(2)→F_{Σ}([ar(R), ar(R)]× ↓). This map is the image under F_{Σ} of

2 ≅ 1 × 2 ⟶ [ar(R), ar(R)]× ↓

2. A ≠ ar(R). Recall that the operations of a given arity have to form an ordered Σ-algebra and this forced us to declare the theory of Σ again. Now we get rid of them by setting these term constructors to be their interpretation the arity. We therefore define σ as above, but replacing (l, r) : 2→T_{Σ}(P) with ! : 0→T_{Σ}(P). As for τ, by similar reasoning to above, we need a map 0→[ar(R), A] × 0 which we obviously take as the identity (which is the unique map from the initial object)

7.2.3 Correctness

We have shown how to present a CTRS with a single rewrite rule as a generalised algebraic theory over Σ-OAlg. The representation was slightly complicated by the need to add in lots of term constructors and then throw them out again, but nevertheless the presentation is still fairly concise. By Theorem 1, this theory has a representing monad which defines the monadic semantics for CTRSs as promised.

However, we still have one thing to do. although we have a monad, is it correct? That is, is the action of the representing monad the same as ordered Σ-algebra-transformer semantics of section 7.1? We prove that this is the case in two stages.

Correctness of the Underlying Monad: Recall that the ordered Σ-algebra-transformer semantics maps an ordered Σ-algebra A to an ordered Σ-algebra [[Θ]](A) such that the carrier of A equals the carrier of [[Θ]](A). Therefore, correctness of the representing monad of a CTRS Θ requires the underlying monad |T_{Θ}| on the category of Σ-algebras is the identity. This underlying monad arises as a representing monad of a theory |Θ| which underlies the theory Θ. To show that this underlying theory is the identity we introduce the notion of a flat theory.

Definition 14 (Flat Theories) A theory A = ⟨Σ, E⟩ is flat iff E(c) = Σ(c) and

• There is a map σ_{0} : Σ(c)→c and σ arises by postcomposition with the unit of T_{A}.

That is σ is

E(c) = Σ(c) ⟶^{σ_{0}} c ⟶^{η_{c}} T_{A}(c)

• The map τ arises as the composition of the following maps

E(c) = Σ(c) ≅ 1 ⊗ Σ(c) ⟶^{1_{c}⊗1} [c, c] ⊗ Σ(c) ⟶ T_{A}(c)

Lemma 7 Given a flat theory A, its representing monad is the identity

Proof. We must construct a map T (c)→c which coequalises σ and τ. Such a map will of course be a cone over the ω-chain defining T (c) and is constructed inductively. The map ψ_{0} : T_{0}(c)→c is the identity on c. Given a map ψ_{n} : T_{n}(c)→c we now construct a map ψ_{n+1} : T_{n+1}(c)→c. The maps σ_{0} and ψ_{n} can be used to build a map

Σ[e, T_{n}(c)] ⊗ S(e)→Σ[e, c] ⊗ e

Next, the canonical map [e, c] ⊗ e→c can be used to build a map

Σ[e, c] ⊗ e→Σc→c

When taken with the identity on c, this gives our map T_{n+1}(c)→c. That this map coequalises σ and τ is a routine verification. □

Notice that the underlying theory of a CTRS Θ is flat and hence by Lemma 7 is represented by the identity monad.

Correctness of the Rewrites: Next we verify that the representing monad T_{Θ} adds in the correct number of rewrites. Since the idea of an equation between rewrites is vacuous we consider those rewrites derived by the term algebra construction. This adds a rewrite to the ordered Σ-algebra A for every map ar(R)→A. By definition of ar(R) such maps are maps F_{Σ}(X+ ↓)→A which coequalise the diagram defining ar(R). In turn this consists of a map X+ ↓ →U_{Σ}(A) whose conjugate satisfies the condition mentioned above. Finally such maps are given by a pair of maps

σ : X→U_{Σ}(X) σ′ :↓ U_{Σ}(X)

But if these maps are to satisfy coequalise the arrows defining ar(R), then σ′ is completely determined by σ and we must have σ^{∗}(l)⇒σ^{∗}(r) which is exactly when a rewrite is added by the ordered Σ-algebra-transformer semantics.

8 Conclusions and Further Work

This paper has carried on a line of successful research in categorical models of rewriting. We have presented a semantics for CTRSs using Pre-enriched monads over categories of ordered Σ-algebras, and can now use our previous results to study modularity of CTRSs from a categorical perspective. The semantics was obtained by systematically instantiating the general theory of Kelly and Power about enriched monads.

There are two natural continuations of this research

• Firstly, the semantics, obtained on a very general level, could be more tailored to the specific needs of CTRSs, along the lines of the term reduction algebra semantics for TRSs in Sect. 4.

• Secondly, we can now investigate modularity problems, using the tools developed in [9, 8]. This proceeds in the following three steps:

1. First, we needs to develop notions of the properties (e.g. confluence or strong normalisation) we want to investigate on the level of our monads.

2. Define a semantic notion of structuring operations — in particular, the coproduct of two monads modeling the disjoint union of CTRSs.

3. Show modularity semantically, e.g. that the coproduct of two confluent monads on Σ-OAlg is confluent.

Any modularity results that could be proven here would potentially be a significant improvement, since previous modularity results for CTRSs are rather scarce [12, 13]. Here, categorical rewriting has the potential to lead the way.

References

[1] Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.

[2] Neil Ghani. Adjoint Rewriting. PhD thesis, University of Edinburgh, 1995.

[3] C. B. Jay. Modelling reductions in confluent categories. In Proceedings of the Durham Symposium on Applications of Categories in Computer Science, 1990.

[4] C. Barry Jay and Neil Ghani. The virtues of η-expansion. Journal for Functional Programming, 5(2):135– 154, April 1995.

[5] G. M. Kelly. Structures defined by finite limits in the enriched context I. Cahiers de Topologie et Géométrie Différentielle, XXIII(1):3–40, 1982.

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

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

[8] C. Lüth and N. Ghani. Monads and modular term rewriting. In E. Moggi and G. Rosolini, editors, Category Theory and Computer Science, number 1290 in Lecture Notes in Computer Science, pages 69– 86, Santa Margherita Ligure, Italy, September 1997. Springer Verlag.

[9] Christoph Lüth. Categorical Term Rewriting: Monads and Modularity. PhD thesis, University of Edinburgh, 1998.

[10] S. Mac Lane. Categories for the Working Mathematician, volume 5 of Graduate Texts in Mathematics. Springer Verlag, 1971.

[11] Ernest G. Manes. Algebraic Theories, volume 26 of Graduate Texts in Mathematics. Springer Verlag, 1976.

[12] Aart Middeldorp. Modular properties of conditional term rewriting systems. Information and Computation, 104:110– 158, 1993.

[13] Aart Middeldorp. Completeness of combinations of conditional constructor systems. Journal for Symbolic Computation, 17:3– 21, 1994.

[14] A. J. Power.  Enriched Lawvere theories.  Available at

http://www.dcs.ed.ac.uk/ ajp, 1999.

[15] E. Robinson. Variations on algebra: monadicity and generalisations of equational theories. Technical Report 6/94, Sussex Computer Science Technical Report, 1994.

[16] D. E. Rydeheard and J. G. Stell. 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, 1987.

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

[18] John G. Stell. Modelling term rewriting systems by Sesqui-categories. Technical Report TR94-02, Keele Unversity, January 1994.