Newman Confluence

Abstract

Terminating locally confluent rewrite systems have globally joinable reductions.

Theorem 1.1 (Every pair of reductions is joinable).

$$\mathrm{WellFounded}(\mathrm{swap}(r))\wedge (\forall h,a,b,r(h,a)\wedge r(h,b)\Rightarrow \exists c,\mathrm{ReflTransGen}(r)(a,c)\wedge \mathrm{ReflTransGen}(r)(b,c))\Rightarrow \forall h,\forall a,b,\mathrm{ReflTransGen}(r)(h,a)\wedge \mathrm{ReflTransGen}(r)(h,b)\Rightarrow \exists c,\mathrm{ReflTransGen}(r)(a,c)\wedge \mathrm{ReflTransGen}(r)(b,c).$$

Proof. Machine-checked in Lean as D5/S0/Rewriting/NewmanConfluence.newman_confluent (✓ std3). ∎

Citation. M. H. A. Newman (1942). On Theories with a Combinatorial Definition of “Equivalence”. DOI: 10.2307/1968867.

Commentary.

For every terminating and locally confluent rewrite relation, any two reflexive-transitive reductions from a common source reach a common successor.

This corollary reuses the frozen unique-normal-form theorem in D5/S0/Rewriting/Newman; the pinned Mathlib version supplies Relation.ReflTransGen.trans but no matching Newman interface.

References

• Truth anchor: D5/S0/Rewriting/NewmanConfluence.newman_confluent
• Dependency: D5/S0/Rewriting/Newman