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.

## 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 in computer science, refers to the property, that a term may be rewritten in several ways, according to , 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 is a set of rewrite rules, we can show that if two terms *M* and *N* are reduced to the term *P* then the following equational axiom holds,

given the set of equational hypotheses , the rewrite relation defined as the reflexive, symmetrical and transitive closure of the single rewrite step and Γ 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 *M* and *N* rewrite to *P* under the rewrite relation as opposed to,
*local confluence* which is a strictly weaker system because we **imply** that the two terms *M* and *N* are provable equal, only if term *M* rewrites to P by an initial rewrite step over the relation . That is *M* rewrites to *P* only if implies . The same applies for the rewrite relation over term *N*. 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,

we can show that the system while locally confluent is not confluent in general. We show local confluence by noticing that the term *a* can rewrite to *b* and *b* can rewrite to *a*, *a* can then be rewritten to *b*. We don't have confluence because *a* can be rewritten to *a*_{0}, *b* rewritten to *b*_{0}. But since neither *a*_{0} or *b*_{0} 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.