Confluence (term rewriting)

Confluence (term rewriting)

Confluence is a property of term rewriting systems, describing that terms in this system can be rewritten in more than one way, to yield the same result.

Motivating example

Consider the rules of regular arithmetic. We can think of these rules as forming a rewriting system. Suppose we are given the expression: (11 + 9) imes (2 + 4)We can rewrite this expression in two ways -- either simplifying the first bracket, or the second. Simplifying the first bracket, we have: 20 imes (2 + 4) = 20 imes 6 = 120Simplifying the second, gives: (11 + 9) imes 6 = 20 imes 6 = 120We get the same result from rewriting the term in two different ways. This suggests that the rewriting system formed from regular arithmetic is a confluent rewriting system.

General case and theory

We can think of a rewriting system abstractly as being a set "S", together with a relation "R" which is a subset of "S"×"S". Instead of denoting relations as pairs ("s", "t"), with "s","t" ∈ "S", we write "s" →"i" "t", where "i" is from some index set "I". If "u" ∈ "S", and "u" →"j" "v" for some "j" ∈ "I", then we say "v" is a "reduct" of "u" (alternatively "v" is an "expansion" of "u", or "u" is "reduced to" "v"). We can also think of a chain of reductions of some element: if "w" ∈ "S", then we may have : w ightarrow_{i_1} w_1 ightarrow_{i_2} w_2 ightarrow_{i_3} cdots where "i""k" ∈ "I". We call this chain a "reduction sequence", or just a "reduction of" "w". If the reduction sequence terminates, say in "w""n", we write : w ightarrow^*_I w_n,reflecting that relations in "I" were chosen. If "I" is clear from context then we can omit this subscript.

With this established, confluence can be defined as follows. Let "a", "b", "c" ∈ "S", with "a" →* "b" and "a" →* "c". If "a" is confluent, there exists a "d" ∈ "S" with "b" →* "d" and "c" →* "d". If every "a" ∈ "S" is confluent, we say that → is confluent, or has the "Church-Rosser property". This property is also sometimes called the "diamond property", after the shape of the diagram shown on the right. Caution: other presentations 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.

Local confluence

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, we say that → is locally (or weakly) confluent, or has 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".

We may view →*, which we introduced as a notation for reduction sequences, as a rewriting system in its own right, whose relation is the transitive closure of "R". Since a sequence of reduction sequences is again a reduction sequence (or, equivalently, since forming the transitive closure is idempotent), →** = →*. It follows that → is confluent if and only if →* is locally confluent.

A rewriting system may be locally confluent without being globally confluent. 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.

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.

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 strongly confluent element need not be confluent, but a strongly confluent rewriting system is necessarily confluent.

See also

* critical pair
* Church–Rosser theorem

References

* "Term Rewriting Systems", Terese, Cambridge Tracts in Theoretical Computer Science, 2003
* "Term Rewriting and All That", Franz Baader and Tobias Nipkow, Cambridge University Press, 1998

External links

*


Wikimedia Foundation. 2010.

Игры ⚽ Нужен реферат?

Look at other dictionaries:

  • Confluence (abstract rewriting) — In computer science, confluence is a property of rewriting systems, describing that terms in this 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… …   Wikipedia

  • Confluence (disambiguation) — Confluence, in geography, describes the meeting of two or more bodies of water. Confluence may also refer to: Confluence (abstract rewriting), a property of term rewriting systems Confluence (meteorology), the streamline air flow convergence of a …   Wikipedia

  • Rewriting — In mathematics, computer science and logic, rewriting covers a wide range of potentially non deterministic methods of replacing subterms of a formula with other terms. What is considered are rewrite systems (also rewriting systems, or term… …   Wikipedia

  • Abstract rewriting system — In mathematical logic and theoretical computer science, an abstract rewriting system (also (abstract) reduction system or abstract rewrite system; abbreviation ARS) is a formalism that captures the quintessential notion and properties of… …   Wikipedia

  • Binary relation — Relation (mathematics) redirects here. For a more general notion of relation, see Finitary relation. For a more combinatorial viewpoint, see Theory of relations. In mathematics, a binary relation on a set A is a collection of ordered pairs of… …   Wikipedia

  • Maude system — The Maude system is an implementation of rewriting logic developed at SRI International. It is similar in its general approach to Joseph Goguen s OBJ3 implementation of equational logic, but based on rewriting logic rather than order sorted… …   Wikipedia

  • Knuth-Bendix completion algorithm — The Knuth Bendix completion algorithm is an algorithm for transforming a set of equations (over terms) into a confluent term rewriting system. When the algorithm succeeds, it has effectively solved the word problem for the specified algebra. An… …   Wikipedia

  • Critical pair (logic) — In mathematical logic, a critical pair arises in term rewriting systems where rewrite rules overlap to yield two different terms. For example, in the term rewriting system with rules , the only critical pair is then (g(x,z), f(x,z)). When one… …   Wikipedia

  • Reecriture (informatique) — Réécriture (informatique) Pour les articles homonymes, voir Réécriture. La réécriture (ou récriture) est un modèle de calcul utilisé en informatique, en algèbre, en logique mathématique et en linguistique. Il s’agit de transformer des objets… …   Wikipédia en Français

  • Réécriture (arithmétique) — Réécriture (informatique) Pour les articles homonymes, voir Réécriture. La réécriture (ou récriture) est un modèle de calcul utilisé en informatique, en algèbre, en logique mathématique et en linguistique. Il s’agit de transformer des objets… …   Wikipédia en Français

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”