19 Rewriting theory

We briefly recall the basics of rewrite theory necessary to our exposition, following mostly Baader and Nipkow [ 3 ] , and generally omitting proofs when they can be found there.

We first work in the abstract taking an arbitrary set $A$ , with a given equivalence relation over it which we denote $\approx$ . We consider a relation $R$ over $A$ .

Definition 19.1

We write $a \to b$ if $a R b$ holds in $A$ , and say that $a$ rewrites to (or reduces to) $b$ . We further define

$\to^{+}$ as the transitive closure of $R$ .
$\to^{*}$ as the reflexive transitive closure of $R$ .
$\leftrightarrow^{*}$ as the reflexive transitive and symmetric closure of $R$ .

We sometimes write $b \leftarrow a$ , (resp. $b^{*} \leftarrow a$ etc) to mean $a \to b$ (resp. $a \to^{*} b$ etc), and chain notations, e.g. $b_{1} \leftarrow a \to b_{2}$ .

Note that $\leftrightarrow^{*}$ is an equivalence relation and the hope is for it to be equal to $\approx$ , in order to deduce properties of the latter.

One should first note that if even $R$ is contained in $\approx$ , then so are $\to^{+}, \to^{*}$ and $\leftrightarrow^{*}$ (as it is an equivalence relation), so we will focus on that case. Generally $a \to^{*} b$ can be seen as a way to compute the $\approx$ relation, as it is directed, in a way to constrain our search space.

However, in general, we cannot deduce the converse, so it may be the case that $a \approx b$ but neither $a \to^{*} b$ nor $b \to^{*} a$ nor even is there a single $c$ such that $a \to^{*} c^{*} \leftarrow b$ , as the number of “left-right alternations” may be arbitrarily large.

The following properties are going to be very useful to deduce exactly such a converse.

Definition 19.2

We say that $R$ is Church-Rosser if whenever $a \leftrightarrow^{*} b$ , there exists some $c$ such that

a \to^{*} c^{*} \leftarrow b

We say that $R$ is confluent if whenever $b_{1}^{*} \leftarrow a \to^{*} b_{2}$ there exists some $c$ such that $b_{1} \to^{*} c^{*} \leftarrow b_{2}$ .

We say that $R$ is locally confluent if whenever $b_{1} \leftarrow a \to b_{2}$ there exists some $c$ such that $b_{1} \to^{*} c^{*} \leftarrow b_{2}$ .

We say that (an arbitrary) $a$ is in normal form (or $a$ is a normal form) if there is no $a^{'} \neq a$ such that $a \to a^{'}$ , and that $R$ is weakly normalizing if for every $a$ , there is some $a^{'}$ such that $a \to^{*} a^{'}$ and $a^{'}$ is in normal form.

We say that $R$ is strongly normalizing if there are no infinite rewrite sequences $a_{1} \to a_{2} \to \dots$ . In particular, a strongly normalizing $R$ is also weakly normalizing.

It turns out that if $R$ is strongly normalizing and Church-Rosser, and effective (we can “compute” with it) then the problem of equivalence is decidable! This is because of the following lemma.

Lemma 19.3

If $R$ is Church-Rosser, then any normal form is unique.

This means that, in this situation, $a$ and $b$ reduce to an identical normal form $c$ if and only if $a \leftrightarrow^{*} b$ ! This means that we have the following algorithm to decide $a \leftrightarrow^{*} b$ (and therefore $a \approx b$ if these relations coincide):

Repeatedly apply $R$ to $a$ and $b$ until normal forms $a^{'}$ and $b^{'}$ are found for them (this is possible because $R$ is strongly normalizing).
Compare $a^{'}$ and $b^{'}$ for exact equality (sometimes called “syntactic equality”).
If $a^{'} = b^{'}$ , we can conclude $a \leftrightarrow^{*} b$ .
If $a^{'} \neq b^{'}$ can can conclude that they are not equivalent due to the lemma.

Note that weak normalization does not change much here except at step 1, where we need to pick reductions which eventually bring the elements to normal forms.

The strategy is therefore, for a given $\approx$ to find an $R$ which is (strongly) normalizing and Church-Rosser, and such that $\leftrightarrow^{*} = \approx$ . This is roughly the goal of the entire field of completion. We call such an $R$ complete for $\approx$ .

The task is helped by the following facts, which we state here also without proof.

Theorem 19.4

$R$ is Church-Rosser iff it is confluent.
(Newman’s lemma) if $R$ is strongly normalizing, then $R$ is confluent iff it is locally confluent.

This can be leveraged by looking at the particulars of the equivalence relation of interest, namely quantified equations over syntactic trees as in Chapter 10, and a theory $Γ$ , which we will usually take to be finite (usually it will have a single equation!).

We will therefore consider relations over the set of elements of the free magma $M_{X}$ , and the aim is to find a rewrite system $R$ is complete for $≃$ .

Certainly $≃$ is closed over substitutions, and be a congruence: if $a ≃ a^{'}$ and $b ≃ b^{'}$ under $Γ$ , then $a ⋄ b ≃ a^{'} ⋄ b^{'}$ under $Γ$ as well.

We therefore consider $R$ to be both closed under substitutions and a congruence. A convenient way to represent this is via a rewrite system: simply a set of pairs of words $(l, r) \in M_{X}$ (we typically write $l \to r$ ) which represents the smallest congruence, closed by substitutions that contains those pairs.

Naturally, a set of laws $w ≃ w^{'}$ can be seen, given a choice of orientation (left-to-right or right-to-left) for each law as such a rewrite system. In this case, it is very clear that the reflexive transitive closure $\leftrightarrow^{*}$ recovers the original equational theory $Γ ⊨ \cdot ≃ \cdot$ . However, it’s clear that sometimes these systems will either be not strongly normalizing, or confluent, or both.

For example, it’s clear that commutativity (the rule $x \cdot y ≃ y \cdot x$ cannot possibly be oriented. Here is a non-confluent example:

x \cdot (y \cdot z) \to y

We have $a \cdot (b \cdot (c \cdot d)) \to^{*} b$ , but also $a \cdot (b \cdot (c \cdot d)) \to^{*} a \cdot c$ for any $a, b, c, d$ (which are both in normal form).

Knuth and Bendix [ 8 ] described a technique by which a theory or set of equations $Γ$ could be turned into a complete system. The crucial idea is the observation that the non-local-confluence of a rewrite system can be reduced to a finite (if the system is finite) set of “worst offenders” for confluence. If these pairs can be joined (reduced to the same term) then the system is confluent. It is possible to compute such pairs.

The high-level idea is therefore to identify such pairs, and add them as an unoriented equation, to be oriented if possible, and repeating until no un-joinable pairs exist. If this procedure succeeds and terminates, the system is successfully completed, and as a result the theory $Γ$ is decidable, via the completed system as described above.

We use the intuitive notions of “position in a word” and “word at a position $p$ ”. We denote by $w [w^{'}]_{p}$ the word $w$ with $w^{'}$ inserted at position $p$ .

Definition 19.5

Given a rewrite system $R$ and two rules $ρ_{1} : l_{1} \to r_{1}$ and $ρ_{2} : l_{2} \to r_{2}$ in $R$ , we say that $(t, u)$ is a critical pair for $ρ_{1}$ and $ρ_{2}$ if there is some non-variable position $p$ in $l_{1}$ such that $l_{2}$ unifies with the term at that position. We denote by $σ$ the most general unifier thus obtained and have $t = r_{1} σ$ and $u = l_{1} σ [r_{2} σ]_{p}$

Note that, in the above setting, $t \leftarrow l_{1} σ \to u$ , giving us a candidate for non-local-confluence. The next lemma states that these candidates are the most general ones.

Theorem 19.6

Given a rewrite system $R$ , if for every critical pair $(t, u)$ of $R$ , there is a term $v$ such that $t \to^{*} v^{*} \leftarrow u$ , then $R$ is locally confluent.

Note that building critical pairs of a finite system is computable. Therefore the only step of the completion process which require genuine creativity is the choice of the orientation of the equations, along with the proof that that orientation is strongly normalizing.

As a capper to this section we can note that even in the event that such an orientation is not found, one can still partially apply the completion procedure, using any well-founded order on terms that is stable by substitution and congruence, to obtain a semi-decision procedure for equality. This process is sometimes called unfailing completion and is at the core of the superposition calculus used in Vampire.