Confluence and Termination

When you rewrite things, you can take different paths. Confluence asks: do
those paths always come back together?

Formally, an ARS $\langle A, \to \rangle$ is confluent iff for all
$a, b, c \in A$:

This is the "diamond" drawn vertically: anything reachable in two ways from $a$
can be brought together to a common $d$.

Three closely related notions (weaker to stronger):

1. Diamond property (one-step): $b \leftarrow a \to c$ implies
$\exists d.\ b \to d \land c \to d$. Strictly one-step reductions
can be joined in one step.
2. Weak confluence: $b \leftarrow a \to c$ implies
$\exists d.\ b \to^* d \land c \to^* d$. One-step reductions join in
any number of steps.
3. Confluence: $b \leftarrow^* a \to^* c$ implies
$\exists d.\ b \to^* d \land c \to^* d$. Multi-step reductions join in
any number of steps.

Confluence is stronger than weak confluence which is stronger than the diamond.

Termination is a separate property: an ARS is terminating iff there is
no infinite chain $a_0 \to a_1 \to a_2 \to \cdots$. Equivalently, every
reduction sequence eventually hits a normal form.

Why termination matters. Without termination, "the answer" might not exist.
With termination, every reduction sequence eventually reaches a normal form.
If also confluent, ALL sequences reach THE SAME normal form — the answer is
unique regardless of strategy.