Confluence (computer science)

from Wikipedia, the free encyclopedia
Confluence in a term rewriting system

Confluence is a term from theoretical computer science and describes the property of a transition system to assign at most one normal form to each element . This means that if an element or a term can be replaced in different ways, it will always be transferred to the same term after further replacements. Confluence is therefore analogous to several streams that merge into one stream. In the lambda calculus this is shown by the Church-Rosser theorem .

Formally this means:

A transition system is called confluent if and only if applies to all : if and , then there is a with and .

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

Confluence is undecidable on the set of all term rewriting systems. For terminating term rewriting systems, however, the confluence is decidable. Because according to the Diamond Lemma the confluence for a terminating term rewriting system is equivalent to the local confluence . And the local confluence is decidable according to the critical pair lemma , since a term rewriting system is locally confluent if and only if all its critical pairs can be brought together .

Web links