As I have not *yet* studied advanced theoretical computer science courses in subjects like type theory, logic, abstract algebra, category theory, and so on.

I have recently been trying to learn the basics on my own.
Previous research attempts has time and time again led me back to the fundamentals of **rewriting systems**,^{1}
and I have decided to take a deeper dive into the basics to prepare myself for more advanced topics in the future.

## ❗

Disclaimer#I am not an expert in the field in any way, this article is merely a collection of my notes and thoughts on the subject, and exists to help me understand the topic of rewriting systems better. This work will in no way be exhaustive, but rather a short personal exploration and self-study.

I will be using various resources, including books, papers and online articles to help me understand the topic better, and I hope you find this article helpful in your own learning journey as well.
A great book I have found on the subject is * Term Rewriting and All That* by

*Franz Baader*and

*Tobias Nipkow*.

^{2}I will use the terms abstract rewriting systems, or abstract reduction systems

*(ARS)*and rewriting systems interchangeably,

^{3}

^{4}

^{2}as I am not focusing on any specific type of rewriting system (Frankly, I am not sure if there is a difference between the two).

## What are Rewriting Systems?#

A rewriting system is a **formal system** that consists of a set of rules that describe how to rewrite terms and are a fundamental concept in computer science, mathematics, and logic.^{5}^{1}^{3}
They are used to model a wide range of *computational processes* and *reasoning* in for example *lambda calculus*.^{6}
Rewriting systems are used in many areas of computer science, including programming languages, compilers, and automated theorem proving.

An abstract rewriting system *(ARS)* consists of a **set of elements \( A \)**, the set of **terms \(T\)**^{7} made up from elements, and **binary relations \(R\)**^{8} on **terms**^{7} (rewrite rules).
The set of symbolic terms can *sometimes* be a combination of elements (\(A \subseteq T\)), indeterminate variable symbols (\(V \subseteq T\)), operator symbols (\(O \subseteq T\)), etc.
This depends on the model domain of the system.
A relation between two terms is denoted by \( \rarr \) and is called the **reduction**, **rewrite relation** or **rule**.^{3}^{1}^{8}
Though the relation is not actually performing any *“reducing” action* or *computation*, it is merely a description of how one term can be *rewritten* into another term.
The system is thus defined by a **set of rules** that describe how terms can be rewritten (transformed), and these rules are applied to terms to produce new terms.
Formally, **\( (A, R) \) is an ARS** where **\( A \) is a set of elements** and **\( R \) is a set of rewrite relations** from one term to another \( R \subseteq A \times A \).
Again, where terms \( t \in T \) are made up of elements \( A \), like \( t ::= A \mid \ldots \), and potentially more constructs depending on domain (shown by \( \ldots \)).

Alternative notations for rewriting systems might use \( (A, \rarr) \) where \( \rarr \) denotes the rewrite relation set. Others might use multiple relation sets to define a system, denoted as \( (A, \rarr_1, \rarr_2, \ldots, \rarr_n) \), which together define the relation set \( R = \rarr_1 \cup \rarr_2 \cup \ldots \cup \rarr_n \) in \( (A, R) \).

### Example (A, B, C)#

Consider the following rewriting system with the set of *ground and linear*^{9} elements \( \lbrace a, b, c \rbrace \) and the rules:

$$ \begin{align*} a & \rarr b \\ b & \rarr c \\ \end{align*} $$

The system can be represented as a directed graph where the nodes are the elements and the edges are the rules. The graph is shown below:

In this system, the element and term \( a \) can be rewritten to \( b \) and \( b \) can be rewritten to \( c \). The term \( a \) can be rewritten to \( c \) by applying the rules \( a \rarr b \) and \( b \rarr c \) in sequence. This is an example of a simple rewriting system.

### Example (Logic)#

Let’s consider a more complex example, a rewriting system that models **logic**^{5} and basics of **boolean algebra**.^{10}
The set of **elements** is \( \lbrace \top, \bot \rbrace \) where \( \top \) represents *true* and \( \bot \) represents *false*.
A **Term** \( t \) can be made up of literal elements and *propositional variables*^{11} \( p, q, r, \ldots \in V \), formalized as \( t ::= \top \mid \bot \mid V \mid \lnot t \mid t \land t \mid t \lor t \).
The **rules**^{1} represent **logical axioms**,^{5} **logical equivalences**^{12} *and* **boolean algebra identities**,^{10} defined as:

$$ \begin{align*} \lnot \lnot p &\rarr p \\ p \land q &\rarr q \land p \\ p \lor q &\rarr q \lor p \\ \lnot (p \land q) &\rarr \lnot p \lor \lnot q \\ \lnot (p \lor q) &\rarr \lnot p \land \lnot q \\ p \land (q \land r) &\rarr (p \land q) \land r \\ p \lor (q \lor r) &\rarr (p \lor q) \lor r \\ (p \land q) \lor r &\rarr (p \lor r) \land (q \lor r) \\ \\ p \land \top &\rarr p \\ p \lor \bot &\rarr p \\ p \land \bot &\rarr \bot \\ p \lor \top &\rarr \top \\ p \land \neg p &\rarr \bot \\ p \lor \neg p &\rarr \top \\ \end{align*} $$

These rewrite relations often have a more complex term on the left-hand side and a simpler term on the right-hand side.
This is a common pattern and hints at the **normalization**^{13} properties of the system, discussed in the next section.
Using this system we can write any expression in its conjunctive normal form (CNF) or disjunctive normal form (DNF) by applying the rules in sequence.^{14}

Below is an example of how the rewrite system can be used to simplify a logical formula: \( \lnot((p \land q) \lor \lnot q)\) to \(\lnot(p \land q) \).

This system models logical reasoning and can be used to prove theorems and derive new logical formulas, and is an example of how rewriting systems can be used in practice.

## More Notation#

Before reading any academic papers using rewriting systems, we’ll need to understand some extended denotation used to describe the rules and properties of rewriting systems. Note, I’m trying to be as comprehensive as possible, but there are lots of different notations used in the literature. Also, I’m not an expert, so take this with a grain of salt.

### Direct Reduction#

Denotations include: \( R \), \( \xrightarrow{} \) and \( \rarr \).

A **regular relation** that represents **a single step** in a rewriting process where one term is **directly transformed** into another based on a *specific* rewrite rule.

### What are Closures?#

Before we go into detail on the different type of notations, let’s first understand what **closures** are __ in the context of rewriting systems__.
It’s easy to get confused with the term, as it may have a different meaning in other subjects.

## Mathematical definition#

A subset of a given set is closed under an operation of the larger set if performing that operation on members of the subset always produces a member of that subset. For example, the natural numbers are closed under addition, but not under subtraction: \(1 − 2\) is not a natural number, although both \(1\) and \(2\) are. Similarly, a subset is said to be closed under a collection of operations if it is closed under each of the operations individually. The closure of a subset is the result of a closure operator applied to the subset. The closure of a subset under some operations is the smallest superset that is closed under these operations. It is often called the span (for example linear span) or the generated set.

^{15}

I interpret this as a **closure** being a **set of elements** that when some **operation** is applied to them, the result **is always a member of the same set**.
Thus the operation is **closed** under the set of elements, meaning no elements are *lost or gained* after the operation, coming from any other set elsewhere, somehow.

The classical example here is of course the **natural numbers** being **closed under addition** but **not under subtraction**.
Because adding two natural numbers always results in another natural number, and subtracting two natural numbers may result in a negative number, which is not a natural number.

$$ \begin{align*} & \forall a, b \in \mathbb{N} \iff a + b \in \mathbb{N} \hspace{1cm} \text{OK} & \\ & \not \forall a, b \in \mathbb{N} \not \Rarr a - b \in \mathbb{N} \hspace{1cm} \text{Not OK} & \\ \end{align*} $$

So, what does this mean in the context of rewriting systems?
Simply put, a **closure**-relation is just like **a regular relation**, but **with additional properties**.^{15}
This is done by extending a basic relation \( R \) or \( \rarr \) to **expand the set of allowable transformations between terms**.
Closures are fundamental in understanding how terms can evolve in a system beyond simple direct transformations, incorporating **sequences**, **reversals**, and **self-referential** transformations, among others.

Above is a diagram showing the different types of closures of a relation.

### Transitive Closure#

Denotations include: \( \xrightarrow{+} \) and \( \rarr^+ \).

The first closure we’ll look at is the **transitive closure** of a relation.

## Mathematical definition#

A binary relation \(R\) on a set \(X\) is transitive if, for all elements \(a, b, c \in X\), whenever \(R\) relates \(a\) to \(b\) and \(b\) to \(c\), then \(R\) also relates \(a\) to \(c\).

The transitive closure of a relation extends the original relation \( \rarr \) so that it includes **direct** and **sequences of transformations** between terms.
For example, if term \( a \rarr b \) and term \( b \rarr c \),
then in the transitive closure, term \( a \) is considered to directly reach term \( c \), notated \( a \rarr^+ c \).
The example below generalize to any number of intermediate terms \( b_1, b_2, \ldots, b_N \).

Simply put, \( a \rarr^+ c \) means that *there is* some sequence of rewrites transforming the term \( a \) to \( c \) *(including one or more rewrites)*.
This is the **smallest** relation that contains the original relation \( \rarr \) *and* is the **transitive** property of terms.^{16}^{17}

### Reflexive Transitive Closure#

Denotations include: \( \xrightarrow{*} \) and \( \rarr^* \).

A **reflexive** relation \( R^* \) is a relation where every element in \(A\) is **related to itself**.
This *can* be formally defined as:^{18}

$$ \begin{align*} & \text{Relation } R \text{ is reflexive } \iff & \forall x \in A, & \ x R x \\ & & \text{or} \hspace{4mm} & \ x \rarr x \\ & & \text{or} \hspace{4mm} & \ (x, x) \in R \end{align*} $$

As every intersection of reflexive relations is reflexive, this defines a closure.
A **reflexive-transitive closure** is a closing relation that is both **reflexive** and **transitive**.^{19}^{16}^{17}
That is having the properties of both the **transitive** and **reflexive** closures, meaning that it includes **direct**, **sequence** and **self-referential** transformations between terms.

### Symmetric Closure#

Denotations include: \( \xleftrightarrow{} \) and \( \lrarr \).

This is a relation that is **symmetric** if, for all elements \(a, b \in X\), whenever \(R\) relates \(a\) to \(b\), then \(R\) also relates \(b\) to \(a\).
This is a closure that includes **bi-directional** transformations between terms.
Formally, a relation \( R \) *is symmetric if* \( a \rarr b \implies b \rarr a \), where \( \lrarr \ = (\rarr \cup \rarr^{-1}) \) and \( \rarr^{-1} \ = \lbrace (b, a) \mid (a, b) \in \rarr \rbrace \).^{3}^{8}

Formally a symmetric closure \( S \) of a relation \( R \) on the set of elements \( A \) is defined as:

$$ \begin{align*} S = R \cup R^{-1} \hspace{2mm} \text{where} \hspace{2mm} R^{-1} = \lbrace a, b \in A \mid (b, a) \in R \rbrace \end{align*} $$

### Reflexive Transitive Symmetric Closure#

Denotations include: \( \xleftrightarrow{*} \), \( \lrarr^* \) and \( \sim \).

This is a relation that is both **reflexive**, **transitive** and **symmetric**.
That is having the properties of the **transitive** and **reflexive** closures, and the **symmetric** property, meaning that it includes **direct**, **sequence**, **self-referential** and **bi-directional** transformations between terms.^{18}^{16}^{17}^{19}^{20}

Similarly, the **reflexive transitive symmetric closure** *or* **equivalence closure** of a relation is the smallest equivalence relation.^{15}^{21}

For all \( a, b, c \in A \):^{21}

**Reflexive**: \( a \rarr^* a \).**Transitive**: \( a \rarr^* b \land b \rarr^* c \implies a \rarr^* c \).**Symmetric**: \( a \rarr^* b \implies b \rarr^* a \).

### Joinability#

Denotation: \( \downarrow \).

A less formal term of normal forms are **joinable** terms, where two terms are joinable if they can be rewritten to the same term.
\( x \downarrow y \) denotes that there exists a term \( z \in A \) such that \( x \rarr^* z \land y \rarr^* z \), alternatively written as \( x \xrightarrow{*} z \xleftarrow{*} y \).

### Composition#

Denotation: \( \circ \).

Composition is a binary operation that combines two relations to form a new relation. For example, using the denotation of a reflexive transitive closure relations, \( \xrightarrow{*} \), the composition of two relations \( R^* \circ S^* \) is defined as \( \lbrace (a, c) \mid \exists b \in A, a \xrightarrow{*}_R b \land b \xrightarrow{*}_S c \rbrace \), and can be expressed by the operator \( \xrightarrow{*}_R \circ \xrightarrow{*}_S \).

## Properties#

Some properties of abstract term rewriting systems are **termination**,^{22}^{23} **confluence**,^{24} **normalization**,^{13} **completion**^{25}^{2} and **equivalence**.^{12}
A confluent and terminating ARS is called **convergent** or **canonical**.^{1}

### Termination#

Termination describes whether a rewriting system has a finite number of rewrites for any term in the system.
An ARS is said to be terminating if there is **no infinite chain** \( x_{0} \rightarrow x_{1} \rightarrow x_{2} \rightarrow \cdots \) of rewrites.^{26}

$$ \begin{align*} & \text{ARS is terminating} \iff \forall x_i \in A \\ % & \text{there is no infinite chain of rewrites } x_{0} \rightarrow x_{1} \rightarrow x_{2} \rightarrow \cdots \\ & \nexists x_{0}, x_{1}, x_{2}, \ldots \text{ such that } x_{0} \rightarrow x_{1} \rightarrow x_{2} \rightarrow \cdots \\ \end{align*} $$

### Confluence#

*“Confluence describes which terms in such a system can be rewritten in more than one way, to yield the same result”*.^{24}
A rewriting system is said to be **confluent** if,
for any terms \( t, s, u \) such that \( t \rarr^* s \land t \rarr^* u \),
there exists a term \( v \) such that \( s \rarr^* v \land u \rarr^* v \).^{24}
In a confluent system, the (TODO) relation is called the **confluence relation**.

Confluence is a property that implies that if a term can be rewritten in more than one way (leading to multiple possible outcomes), all these paths will eventually converge to a common rewrite outcome, regardless of the choices made during rewriting. Formally, denoting that any term \(a\) can reach any term \(b\) (and vice versa) through a sequence of forward and backward steps, is instrumental in analyzing confluence. If this closure holds between any two rewrite results of the same term, the system is confluent. The symmetric closure \( \xleftrightarrow{*} \) is used to define confluence.

An ARS possess the **Church-Rosser property** if and only if \( x \xleftrightarrow{*} y \) implies \( x \downarrow y \) for all terms \( x, y \) in the system.^{24}^{3}

$$ \begin{align*} & \text{Church-Rosser property} \iff \\ & \forall x, y \in A, x \xleftrightarrow{*} y \implies x \downarrow y \\ \end{align*} $$

### Convergence#

Convergence is a combination of confluence and termination. A rewriting system is convergent if it is both confluent and terminating. Convergence guarantees that every term can be rewritten to a unique normal form.

### Consistency#

In the context of logic and type systems, consistency refers to the property that there are no terms that can be both proved and disproved within the system. For rewriting systems, particularly those representing logical proofs, consistency means that there is no term that can be rewritten to both a theorem and its negation.

### Decidability#

A rewriting system has the property of decidability if there is an effective procedure (algorithm) to determine whether, for any two given terms, one term can be rewritten to the other. This property is important for automated reasoning systems where it’s necessary to know whether a certain state can be reached.

### Completion#

A rewriting system is complete if it is both confluent and strongly normalizing. Completeness is often desired in theorem proving and formal verification since it ensures that every valid proof can be found through a systematic search of the rewriting system.

### Equivalence#

The property of equivalence in rewriting systems refers to the scenario where different sequences of rewrites on a term or from a term lead to outcomes that can be considered equivalent under the rewriting rules. The reflexive transitive symmetric closure \( \xleftrightarrow{*} \) is the smallest equivalence relation containing the original rewrite relation \( \rarr \). This closure indicates that any two terms related by this closure can be transformed into each other through a series of rewriting steps, forward or backward, indicating that they are equivalent in the context of the rewriting system.

### Normal Forms#

A term in **normal form**^{13} (NF) is an irreducible, canonical representation of a term in a rewriting system.
That is, **no rewrite rules can be applied to the term to produce a new term**. Formally, if \( (A, \rarr) \) is an ARS, a **term \( t \)**, \( t \in A \) **is in normal form** if there is exists no other term \( s \in A \) such that \( t \rarr s \).

$$ \begin{align*} t \text{ is in normal form} &\iff \nexists s \in A \text{ such that } t \rarr s \\ \end{align*} $$

#### Strong Normalization#

A term is said to be **strongly normalizing (SN)** if *all possible rewrites* eventually reach a normal form and terminate in a finite number of steps.
An ARS is **strongly normalizing** if all terms in the system are strongly normalizing (terminating).^{13}^{26}

$$ \begin{align*} & t \text{ is strongly normalizing} \iff \bold{\forall} s \in A \\ & \text{ such that } t \rarr^* s \text{, } s \text{ is in normal form} \\ \end{align*} $$

Consider the following ARS:

$$ \begin{align*} a &\rarr c \\ b &\rarr c \\ c &\rarr d \\ c &\rarr e \\ d &\rarr f \\ e &\rarr f \\ d &\rarr g \\ f &\rarr h \\ \end{align*} $$

The **normal forms** of this system are \( h \) and \( g \).
Visualizing the relations above, we can see that any term can be rewritten to either \( h \) or \( g \) in a finite number of steps, making the system strongly normalizing.

#### Weak Normalization#

A term is said to be **weakly normalizing (WN)** if *any* rewrites reach a normal form and terminates in a finite number of steps.

$$ \begin{align*} & t \text{ is weakly normalizing} \iff \bold{\exists} s \in A \\ & \text{ such that } t \rarr^* s \text{ and } s \text{ is in normal form} \\ \end{align*} $$

To illustrate the distinction between strong and **weak normalization (WN)**, consider the following ARS:

$$ \begin{align*} A &\rarr B \\ A &\rarr (AA) \\ \end{align*} $$

The term \(A\) is **weakly normalizing** because it *can* be rewritten to \(B\), a normal form.
However, it’s **not strongly normalizing** since an infinite sequence of expansions can occur (see below).
This highlights that while * weak normalization ensures that a result can be found*,

*.*

**strong normalization**guarantees that the process of finding that result**is always finite**#### Conclusion Normalization#

Normal forms are important because they provide a unique term used to compare for equivalence^{12} and to prove properties of the system.
In some systems, not all terms have a normal form, and the system is said to be **non-terminating**^{22}^{23}^{26} and is the reason some rewriting systems are **non-deterministic** and **undecidable**.^{1}

## Conclusion#

Today we have explored the basics of rewriting systems, including the fundamental concepts, notation, and properties. We have seen how rewriting systems are used as a fundamental model for computational processes and reasoning in computer science, mathematics, and logic. They consist of a set of elements, terms, and rewrite rules that describe how terms can be transformed. Rewriting systems are used in many areas, including programming languages, compilers, and automated theorem proving.

I hope this article has helped you understand the basics of rewriting systems and that you have learned something new.

“Rewriting Systems”, https://en.wikipedia.org/wiki/Rewriting. ↩︎ ↩︎ ↩︎ ↩︎ ↩︎ ↩︎

“Term Rewriting and All That” by

*Franz Baader*and*Tobias Nipkow*. Find the book on Cambridge Core or Cambridge University Press. ↩︎ ↩︎ ↩︎“Abstract Rewriting System”, https://en.wikipedia.org/wiki/Abstract_rewriting_system. ↩︎ ↩︎ ↩︎ ↩︎ ↩︎

Enno Ohlebusch, “Abstract Reduction Systems,” in Advanced Topics in Term Rewriting, ed. Enno Ohlebusch (New York, NY: Springer, 2002), 7–35, https://doi.org/10.1007/978-1-4757-3661-8_2. ↩︎

“Logic”, https://en.wikipedia.org/wiki/Logic. ↩︎ ↩︎ ↩︎

“Lambda calculus”, https://en.wikipedia.org/wiki/Lambda_calculus. ↩︎

“Term (logic)”, https://en.wikipedia.org/wiki/Term_(logic). ↩︎ ↩︎

“Binary relation”, https://en.wikipedia.org/wiki/Binary_relation. ↩︎ ↩︎ ↩︎

“Ground and Linear Terms”, https://en.wikipedia.org/wiki/Term_(logic)#Ground_and_linear_terms. ↩︎

“Boolean algebra”, https://en.wikipedia.org/wiki/Boolean_algebra. ↩︎ ↩︎

“Propositional variable”, https://en.wikipedia.org/wiki/Propositional_variable. ↩︎

“Equivalence (logic), https://en.wikipedia.org/wiki/Logical_equivalence. ↩︎ ↩︎ ↩︎

“Normal form”, https://en.wikipedia.org/wiki/Normal_form_(abstract_rewriting). ↩︎ ↩︎ ↩︎ ↩︎

“Conjunctive normal form”, https://en.wikipedia.org/wiki/Conjunctive_normal_form. ↩︎

“Closure (mathematics)”, https://en.wikipedia.org/wiki/Closure_(mathematics). ↩︎ ↩︎ ↩︎

“Transitive relation”, https://en.wikipedia.org/wiki/Transitive_relation. ↩︎ ↩︎ ↩︎

“Transitive closure”, https://en.wikipedia.org/wiki/Transitive_closure. ↩︎ ↩︎ ↩︎

“Reflexive relation”, https://en.wikipedia.org/wiki/Reflexive_relation. ↩︎ ↩︎

“Reflective closure”, https://en.wikipedia.org/wiki/Reflexive_closure. ↩︎ ↩︎

“Symmetric closure”, https://en.wikipedia.org/wiki/Symmetric_closure. ↩︎

“Equivalence relation”, https://en.wikipedia.org/wiki/Equivalence_relation. ↩︎ ↩︎

Aart Middeldorp and Hans Zantema, “Simple Termination of Rewrite Systems,” Theoretical Computer Science 175, no. 1 (March 1997): 127–58, https://doi.org/10.1016/S0304-3975(96)00172-7. ↩︎ ↩︎

Nachum Dershowitz, “Termination of Rewriting,” Journal of Symbolic Computation 3, no. 1–2 (February 1987): 69–115, https://doi.org/10.1016/S0747-7171(87)80022-6. ↩︎ ↩︎

“Confluence”, https://en.wikipedia.org/wiki/Confluence_(abstract_rewriting). ↩︎ ↩︎ ↩︎ ↩︎

“Completion (logic)”, https://en.wikipedia.org/wiki/Completeness_(logic). ↩︎

“Termination”, https://en.wikipedia.org/wiki/Rewriting#Termination. ↩︎ ↩︎ ↩︎