Confluence (abstract rewriting)

The usual rules of elementary arithmetic form an abstract rewriting system.

For example, the expression (11 + 9) × (2 + 4) can be evaluated starting either at the left or at the right parentheses; however, in both cases the same result is eventually obtained.

[1] A second, more abstract example is obtained from the following proof of each group element equalling the inverse of its inverse:[2] This proof starts from the given group axioms A1–A3, and establishes five propositions R4, R6, R10, R11, and R12, each of them using some earlier ones, and R12 being the main theorem.

One of the historical motivations to develop the theory of term rewriting was to avoid the need for such steps, which are difficult to find by an inexperienced human, let alone by a computer program [citation needed].

The success of that method does not depend on a certain sophisticated order in which to apply rewrite rules, as confluence ensures that any sequence of rule applications will eventually lead to the same result (while the termination property ensures that any sequence will eventually reach an end at all).

Therefore, if a confluent and terminating term rewriting system can be provided for some equational theory,[note 2] not a tinge of creativity is required to perform proofs of term equality; that task hence becomes amenable to computer programs.

So, for example, if the expression a can be rewritten into b, then we say that b is a reduct of a (alternatively, a reduces to b, or a is an expansion of b).

So, for instance, if c → c′ → c′′ → ... → d′ → d, then we can write c ∗→ d, indicating the existence of a reduction sequence from c to d. Formally, ∗→ is the reflexive-transitive closure of →.

However, Newman's lemma states that if a locally confluent rewriting system has no infinite reduction sequences (in which case it is said to be terminating or strongly normalizing), then it is globally confluent.

In a rewriting system with the Church–Rosser property the word problem may be reduced to the search for a common successor.

In lambda calculus for instance, the expression (λx.xx)(λx.xx) does not have a normal form because there exists an infinite sequence of β-reductions (λx.xx)(λx.xx) → (λx.xx)(λx.xx) → ...[8] A rewriting system possesses the Church–Rosser property if and only if it is confluent.

[9] Because of this equivalence, a fair bit of variation in definitions is encountered in the literature.

For instance, in "Terese" the Church–Rosser property and confluence are defined to be synonymous and identical to the definition of confluence presented here; Church–Rosser as defined here remains unnamed, but is given as an equivalent property; this departure from other texts is deliberate.

The name confluence is inspired from geography, where it means the meeting of two bodies of water.
In this diagram, a reduces to both b or c in zero or more rewrite steps (denoted by the asterisk). In order for the rewrite relation to be confluent, both reducts must in turn reduce to some common d .
Figure 1: Cyclic, locally-confluent, but not globally confluent rewrite system [ 4 ]
Figure 2: Infinite non-cyclic, locally-confluent, but not globally confluent rewrite system [ 4 ]