# Today I Learned

Some of the things I've learned every day since Oct 10, 2016

## 67: Confluence (Rewriting Systems)

A term $a$ within a rewriting system (such as one in the lambda calculus) is confluent if, for any pair of terms $b, c$ such that $a \rightarrow b$ and $a \rightarrow c$ (where $x \rightarrow y$ means $y$ is a reduct of $x$ under 0 or more reductions), there exists a term $d$ such that $b \rightarrow d$ and $c \rightarrow d$. If every term in a system is confluent, the system itself is said to be confluent.

Systems which are both confluent and terminating are especially nice, because any sequence of reductions can be applied to a given term with the resulting irreducible reduct being the same.