In computer science, confluence is a property of
rewriting
In mathematics, computer science, and logic, rewriting covers a wide range of methods of replacing subterms of a well-formed formula, formula with other terms. Such methods may be achieved by rewriting systems (also known as rewrite systems, rewr ...
systems, describing which terms in such a system can be rewritten in more than one way, to yield the same result. This article describes the properties in the most abstract setting of an
abstract rewriting system
In mathematical logic and theoretical computer science, an abstract rewriting system (also (abstract) reduction system or abstract rewrite system; abbreviated ARS) is a formalism that captures the quintessential notion and properties of rewriting s ...
.
Motivating examples
![Confluence example expression](https://upload.wikimedia.org/wikipedia/commons/9/99/Confluence_example_expression.svg)
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.
If every arithmetic expression evaluates to the same result regardless of reduction strategy, the arithmetic rewriting system is said to be ground-confluent. Arithmetic rewriting systems may be confluent or only ground-confluent depending on details of the rewriting system.
A second, more abstract example is obtained from the following proof of each
group
A group is a number of persons or things that are located, gathered, or classed together.
Groups of people
* Cultural group, a group whose members share the same cultural identity
* Ethnic group, a group whose members share the same ethnic iden ...
element equalling the
inverse
Inverse or invert may refer to:
Science and mathematics
* Inverse (logic), a type of conditional sentence which is an immediate inference made from another conditional sentence
* Additive inverse (negation), the inverse of a number that, when ad ...
of its inverse:
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. Some of the proofs require non-obvious, or even creative, steps, like applying axiom A2 in reverse, thereby rewriting "1" to "''a''
−1 ⋅ a" in the first step of R6's proof. 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.
If a
term rewriting system
In mathematics, computer science, and logic, rewriting covers a wide range of methods of replacing subterms of a formula with other terms. Such methods may be achieved by rewriting systems (also known as rewrite systems, rewrite engines, or red ...
is confluent and ''
terminating'', a straightforward method exists to prove equality between two expressions (also known as ''
terms'') ''s'' and ''t'':
Starting with ''s'', apply equalities
[then called ''rewrite rules'' to emphasize their left-to-right orientation] from left to right as long as possible, eventually obtaining a term ''s′''.
Obtain from ''t'' a term ''t′'' in a similar way.
If both terms ''s′'' and ''t′'' literally agree, then ''s'' and ''t'' are (not surprisingly) proven equal.
More importantly, if they disagree, then ''s'' and ''t'' cannot be equal.
That is, any two terms ''s'' and ''t'' that can be proven equal at all can be done so by that method.
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
Universal algebra (sometimes called general algebra) is the field of mathematics that studies algebraic structures themselves, not examples ("models") of algebraic structures.
For instance, rather than take particular groups as the object of study, ...
,
[The ]Knuth–Bendix completion algorithm The Knuth–Bendix completion algorithm (named after Donald Knuth and Peter Bendix) is a semi-decision algorithm for transforming a set of equations (over terms) into a confluent term rewriting system. When the algorithm succeeds, it effectively ...
can be used to compute such a system from a given set of equations. Such a system e.g. for groups is shown here
Here is an adverb that means "in, on, or at this place". It may also refer to:
Software
* Here Technologies, a mapping company
* Here WeGo (formerly Here Maps), a mobile app and map website by Here
Television
* Here TV (formerly "here!"), a TV ...
, with its propositions consistently numbered. Using it, a proof of e.g. R6 consists in applying R11 and R12 in any order to the term (''a''−1)−1⋅1 to obtain the term ''a''; no other rules are applicable.
not a tinge of creativity is required to perform proofs of term equality; that task hence becomes amenable to computer programs. Modern approaches handle more general ''abstract rewriting systems'' rather than ''term'' rewriting systems; the latter are a special case of the former.
General case and theory
A rewriting system can be expressed as a
directed graph
In mathematics, and more specifically in graph theory, a directed graph (or digraph) is a graph that is made up of a set of vertices connected by directed edges, often called arcs.
Definition
In formal terms, a directed graph is an ordered pa ...
in which nodes represent expressions and edges represent rewrites. 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''). This is represented using arrow notation; ''a'' → ''b'' indicates that ''a'' reduces to ''b''. Intuitively, this means that the corresponding graph has a directed edge from ''a'' to ''b''.
If there is a path between two graph nodes ''c'' and ''d'', then it forms a ''reduction sequence''. 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 →. Using the example from the previous paragraph, we have (11+9)×(2+4) → 20×(2+4) and 20×(2+4) → 20×6, so (11+9)×(2+4) 20×6.
With this established, confluence can be defined as follows. ''a'' ∈ ''S'' is deemed confluent if for all pairs ''b'', ''c'' ∈ ''S'' such that ''a'' ''b'' and ''a'' ''c'', there exists a ''d'' ∈ ''S'' with ''b'' ''d'' and ''c'' ''d'' (denoted
). If every ''a'' ∈ ''S'' is confluent, we say that → is confluent. This property is also sometimes called the ''diamond property'', after the shape of the diagram shown on the right. Some authors reserve the term ''diamond property'' for a variant of the diagram with single reductions everywhere; that is, whenever ''a'' → ''b'' and ''a'' → ''c'', there must exist a ''d'' such that ''b'' → ''d'' and ''c'' → ''d''. The single-reduction variant is strictly stronger than the multi-reduction one.
Ground confluence
A term rewriting system is ground confluent if every
ground term
In mathematical logic, a ground term of a formal system is a term that does not contain any variables. Similarly, a ground formula is a formula that does not contain any variables.
In first-order logic with identity, the sentence Q(a) \lor P(b) ...
is confluent, that is, every term without variables.
Local confluence
![Non-cyclic locally, but not globally confluent rewrite system](https://upload.wikimedia.org/wikipedia/commons/6/65/Non-cyclic_locally%2C_but_not_globally_confluent_rewrite_system.gif)
An element ''a'' ∈ ''S'' is said to be locally (or weakly) confluent if for all ''b'', ''c'' ∈ ''S'' with ''a'' → ''b'' and ''a'' → ''c'' there exists ''d'' ∈ ''S'' with ''b'' ''d'' and ''c'' ''d''. If every ''a'' ∈ ''S'' is locally confluent, then → is called locally (or weakly) confluent, or having the ''weak Church–Rosser property''. This is different from confluence in that ''b'' and ''c'' must be reduced from ''a'' in one step. In analogy with this, confluence is sometimes referred to as ''global confluence''.
The relation , introduced as a notation for reduction sequences, may be viewed as a rewriting system in its own right, whose relation is the
reflexive-transitive closure of ''→''. Since a sequence of reduction sequences is again a reduction sequence (or, equivalently, since forming the reflexive-transitive closure is
idempotent
Idempotence (, ) is the property of certain operation (mathematics), operations in mathematics and computer science whereby they can be applied multiple times without changing the result beyond the initial application. The concept of idempotence ...
), = . It follows that → is confluent if and only if is locally confluent.
A rewriting system may be locally confluent without being (globally) confluent. Examples are shown in picture 3 and 4. However,
Newman's lemma In mathematics, in the theory of rewriting systems, Newman's lemma, also commonly called the diamond lemma, states that a terminating (or strongly normalizing) abstract rewriting system (ARS), that is, one in which there are no infinite reduction ...
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.
Church–Rosser property
A rewriting system is said to possess the Church–Rosser property if and only if
implies
for all objects ''x'', ''y''.
Alonzo Church
Alonzo Church (June 14, 1903 – August 11, 1995) was an American mathematician, computer scientist, logician, philosopher, professor and editor who made major contributions to mathematical logic and the foundations of theoretical computer scienc ...
and
J. Barkley Rosser
John Barkley Rosser Sr. (December 6, 1907 – September 5, 1989) was an American logician, a student of Alonzo Church, and known for his part in the Church–Rosser theorem, in lambda calculus. He also developed what is now called the "Rosser siev ...
proved in 1936 that
lambda calculus
Lambda calculus (also written as ''λ''-calculus) is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution. It is a universal model of computation ...
has this property; hence the name of the property. (The fact that lambda calculus has this property is also known as the
Church–Rosser theorem
In lambda calculus, the Church–Rosser theorem states that, when applying reduction rules to terms, the ordering in which the reductions are chosen does not make a difference to the eventual result.
More precisely, if there are two distinct red ...
.) In a rewriting system with the Church–Rosser property the word problem may be reduced to the search for a common successor. In a Church–Rosser system, an object has ''at most one''
normal form; that is the normal form of an object is unique if it exists, but it may well not exist. In lambda calculus for instance, the expression (λx.xx)(λx.xx) does not have a normal form because there exists an infinite sequence of
β-reduction
Lambda calculus (also written as ''λ''-calculus) is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution. It is a universal model of computation th ...
s (λx.xx)(λx.xx) → (λx.xx)(λx.xx) → ...
A rewriting system possesses the Church–Rosser property
if and only if
In logic and related fields such as mathematics and philosophy, "if and only if" (shortened as "iff") is a biconditional logical connective between statements, where either both statements are true or both are false.
The connective is bicondi ...
it is confluent. 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.
[Marc Bezem, ]Jan Willem Klop
Jan Willem Klop (born 1945) is a professor of applied logic at Vrije Universiteit in Amsterdam. He holds a Ph.D. in mathematical logic from Utrecht University. Klop is known for his work on the Algebra of Communicating Processes, co-author of ''T ...
, Roel de Vrijer ("Terese"), ''Term rewriting systems'', Cambridge University Press, 2003, , Here: p.11
Semi-confluence
The definition of local confluence differs from that of global confluence in that only elements reached from a given element in a single rewriting step are considered. By considering one element reached in a single step and another element reached by an arbitrary sequence, we arrive at the intermediate concept of semi-confluence: ''a'' ∈ ''S'' is said to be semi-confluent if for all ''b'', ''c'' ∈ ''S'' with ''a'' → ''b'' and ''a'' ''c'' there exists ''d'' ∈ ''S'' with ''b'' ''d'' and ''c'' ''d''; if every ''a'' ∈ ''S'' is semi-confluent, we say that → is semi-confluent.
A semi-confluent element need not be confluent, but a semi-confluent rewriting system is necessarily confluent, and a confluent system is trivially semi-confluent.
Strong confluence
Strong confluence is another variation on local confluence that allows us to conclude that a rewriting system is globally confluent. An element ''a'' ∈ ''S'' is said to be strongly confluent if for all ''b'', ''c'' ∈ ''S'' with ''a'' → ''b'' and ''a'' → ''c'' there exists ''d'' ∈ ''S'' with ''b'' ''d'' and either ''c'' → ''d'' or ''c'' = ''d''; if every ''a'' ∈ ''S'' is strongly confluent, we say that → is strongly confluent.
A confluent element need not be strongly confluent, but a strongly confluent rewriting system is necessarily confluent.
Examples of confluent systems
* Reduction of
polynomial
In mathematics, a polynomial is an expression consisting of indeterminates (also called variables) and coefficients, that involves only the operations of addition, subtraction, multiplication, and positive-integer powers of variables. An exa ...
s modulo an
ideal
Ideal may refer to:
Philosophy
* Ideal (ethics), values that one actively pursues as goals
* Platonic ideal, a philosophical idea of trueness of form, associated with Plato
Mathematics
* Ideal (ring theory), special subsets of a ring considere ...
is a confluent rewrite system provided one works with a
Gröbner basis
In mathematics, and more specifically in computer algebra, computational algebraic geometry, and computational commutative algebra, a Gröbner basis is a particular kind of generating set of an ideal in a polynomial ring over a field . A Gröbn ...
.
*
Matsumoto's theorem follows from confluence of the braid relations.
* β-reduction of λ-terms is confluent by the
Church–Rosser theorem
In lambda calculus, the Church–Rosser theorem states that, when applying reduction rules to terms, the ordering in which the reductions are chosen does not make a difference to the eventual result.
More precisely, if there are two distinct red ...
.
See also
*
Convergence (logic) In mathematics, computer science and logic, convergence is the idea that different sequences of transformations come to a conclusion in a finite amount of time (the transformations are terminating), and that the conclusion reached is independent of ...
*
Critical pair (logic)
A critical pair arises in a term rewriting system when two rewrite rules overlap to yield two different terms. In more detail, (''t''1, ''t''2) is a critical pair if there is a term ''t'' for which two different applications of a rewrite rule (ei ...
*
Normal form (abstract rewriting)
In abstract rewriting, an object is in normal form if it cannot be rewritten any further, i.e. it is irreducible. Depending on the rewriting system, an object may rewrite to several normal forms or none at all. Many properties of rewriting systems ...
Notes
References
* ''Term Rewriting Systems'', Terese, Cambridge Tracts in Theoretical Computer Science, 2003.
*
Term Rewriting and All That',
Franz Baader
Franz Baader (15 June 1959, Spalt) is a German computer scientist at Dresden University of Technology.
He received his PhD in Computer Science in 1989 from the University of Erlangen-Nuremberg, Germany, where he was a teaching and research assist ...
and
Tobias Nipkow
Tobias Nipkow (born 1958) is a German computer scientist.
Career
Nipkow received his Diplom (MSc) in computer science from the Department of Computer Science of the Technische Hochschule Darmstadt in 1982, and his Ph.D. from the University of ...
, Cambridge University Press, 1998
External links
*
{{DEFAULTSORT:Confluence (Abstract Rewriting)
Rewriting systems