Confluence (abstract rewriting)

Confluence is a term used in theoretical computer science and refers to the property of a transition system to assign each element at most one normal form. That is, if an element or a term may be substituted in various ways, it is more substitutions always leads to the same term. Confluence is thus analogous to a plurality of streams that flow together to a current. In the lambda calculus, this is shown by the Church - Rosser theorem.

Formally, this means:

A transition system is said to be confluent if for all: if and, then there is a with and.

Confluent term rewriting systems are very useful when one wants to prove that terms are equivalent, for example, in a system of equations. An equation is provably correct if and only if the terms can be formed on both sides of the equality symbol to the same term.

Confluence is undecidable on the set of term rewriting systems. For terminating term rewriting systems, confluence is decidable but. Because after the Diamond Lemma is the confluence of a terminating term rewriting system equivalent to local confluence. And the local confluence is decidable for the critical pair lemma, since a term rewriting system is locally confluent iff all its critical pairs are merged.