Confluence, given a rewrite system in computer science, refers to the property that a term may be rewritten in several ways, according to , yet may be resolved to the same term after enough reduction steps. For example, in the lambda calculus confluence is shown via the Church-Rosser theorem. Rewriting in mathematics, computer science and logic covers a wide range of methods of transforming strings, written in some fixed alphabet, that are not deterministic but are governed by explicit rules. ... The word term refers to either a word unit or a time unit with specified boundaries or limits. ... The lambda calculus is a formal system designed to investigate function definition, function application, and recursion. ... The Church-Rosser theorem states that if there are two distinct reductions starting from some term in the lambda calculus, then there exists a term that is reachable via reduction from both sequences. ...

Confluent rewrite systems are very useful for analyzing provable equality in equational logic. This is because in a confluent system, an equation is provable precisely when both terms reduce to the same single term. This idea holds in many rewrite systems, including the typed and untyped lambda calculus.

If is a set of rewrite rules, we can show that if two terms M and N are reduced to the term P then the following equational axiom holds,

given the set of equational hypotheses , the rewrite relation defined as the reflexive, symmetrical and transitive closure of the single rewrite step and Γ a function mapping variables to types.

Local and global confluence

We can further characterize a rewrite system by the following properties:

• global confluence or just confluence holds if two terms M and N rewrite to P under the rewrite relation as opposed to,
• local confluence which is a strictly weaker system because we imply that the two terms M and N are provable equal, only if term M rewrites to P by an initial rewrite step over the relation . That is M rewrites to P only if implies . The same applies for the rewrite relation over term N. It is important to distinguish the two because a system can be locally confluent, yet not globally confluent, shown in the example below.

Example

Consider the following, taken from [1]. Given the rewrite system,

we can show that the system while locally confluent is not confluent in general. We show local confluence by noticing that the term a can rewrite to b and b can rewrite to a, a can then be rewritten to b. We don't have confluence because a can be rewritten to a₀, b rewritten to b₀. But since neither a₀ or b₀ can be reduced to the other, confluence fails.

Thus intuitively, local confluence only guarantees that within a single reduction step we can rewrite one term to the other. While strong confluence not only guarantees the above, but also that for n steps of reduction we have local confluence, therefore by induction, the whole system is globally confluent.

It is helpful to note that in a terminating rewrite system local confluence is the same as global confluence. Rewriting in mathematics, computer science and logic covers a wide range of methods of transforming strings, written in some fixed alphabet, that are not deterministic but are governed by explicit rules. ...

Critical pairs

An important notion is the critical pair. A critical pair is of terms representing an interaction between rewrite rules.

Left-linear rewrite system

To Do r2=6 x=2-1(8).

References

[1] Mitchell, John C., Foundations for Programming Languages, ISBN 0-262-13321-0, 1996, Massachusetts Institute of Technology.