Confluence
|
|
A confluence is the merger or meeting of two or more objects (or subjects) that seem to inseparably bind their respective forces or attributes into a point of junction.
| Contents |
Geography
The word is typically used in geography to describe the point where two rivers meet and become one, usually when a tributary joins a more major river.
Etymology
The word is comprised of the prefix con (from the Latin "com"), meaning "with" or "together", and joined with the suffix fluence from the Latin "fluere" meaning "to flow". The resulting meaning literally translates as "to flow together". It is interesting to note that the joining of both prefix and suffix to make the word confluence is a confluence in and of itself; both word parts join to form something that flows in the phenomenal river of language.
HDL
Confluence is a modern functional hardware description language (HDL, but not to be confused with high density lipoproteins (HDL)).
Computer science
Confluence, given a rewrite system <math>\mathcal{R}<math> in computer science, refers to the property, that a term may be rewritten in several ways, according to <math>\mathcal{R}<math>, 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.
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 <math>\mathcal{R}<math> is a set of rewrite rules, we can show that if two terms <math>M<math> and <math>N <math> are reduced to the term <math>P<math> then the following equational axiom holds,
- <math>
\mathcal{E}_{\mathcal{R}}\vdash M=N[\Gamma]\ \iff\ M\hookrightarrow_{\mathcal{R}}P\hookleftarrow_{\mathcal{R}}N, <math>
given the set of equational hypotheses <math>\mathcal{E}<math>, the rewrite relation <math>\hookrightarrow<math> defined as the reflexive, symmetrical and transitive closure of the single rewrite step <math>\rightarrow<math> and <math>\Gamma<math> 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 <math>M<math> and <math>N<math> rewrite to <math>P<math> under the rewrite relation <math>\hookrightarrow_{\mathcal{R}}<math> as opposed to,
- local confluence which is a strictly weaker system because we imply that the two terms <math>M<math> and <math>N<math> are provable equal, only if term <math>M<math> rewrites to P by an initial rewrite step over the relation <math>\rightarrow_{\mathcal{R}}<math>. That is M rewrites to P only if <math>L\leftarrow M\rightarrow O<math> implies <math>L\hookrightarrow_{\mathcal{R}}P\hookleftarrow_{\mathcal{R}}O<math>. The same applies for the rewrite relation over term <math>N<math>. 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,
<math>a\rightarrow b, b\rightarrow a,<math> <math>a\rightarrow a_0, b\rightarrow b_0<math>
we can show that the system while locally confluent is not confluent in general. We show local confluence by noticing that the term <math>a<math> can rewrite to <math>b<math> and <math>b<math> can rewrite to <math>a<math>, <math>a<math> can then be rewritten to <math>b<math>. We don't have confluence because <math>a<math> can be rewritten to <math>a_0<math>, <math>b<math> rewritten to <math>b_0<math>. But since neither <math>a_0<math> or <math>b_0<math> 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.
Critical pairs
An important notion is the critical pair. A critical pair is of terms representing an interaction between rewrite rules. To Do
Left-Linear Rewrite System
To Do r2=6 x=2-1(8).
See also
References
[1] Mitchel J. C., Foundations for Programming Languages, ISBN 0-262-13321-0, 1996, Massachusetts Institute of Technology.