Newman's lemma

Remarks

Confluence always implies local confluence, so the content is the converse. Since the system is terminating, the converse of $\to^+$ (one or more steps) is a well-founded relation. One proves by well-founded induction on $a$ that any two reducts $a \to^* b$ and $a \to^* c$ are joinable. If $a \to b_1 \to^* b$ and $a \to c_1 \to^* c$, local confluence joins $b_1$ and $c_1$ at some $d$, and the induction hypothesis at $b_1$ and then at $c_1$ joins everything. Termination is necessary: the system with $b \to a$, $b \to c$, $c \to b$, $c \to d$ is locally confluent but not confluent, because $b$ has the two normal forms $a$ and $d$. In practice the lemma reduces confluence to checking finitely many local situations, such as the critical pairs of a term rewriting system.

Going deeper

For a student

Newman's lemma is the basic tool for proving that a rewriting system has unique normal forms. For term rewriting systems, local confluence reduces further to the joinability of critical pairs, which is the basis of Knuth–Bendix completion. For lambda calculus the lemma does not apply, since beta reduction is not terminating, and confluence is proved instead by parallel reduction.