NF-Confluence

Normalization of programs is confluent: any two reduction paths yield the same normal form. Proved via termination + local confluence + Newman’s Lemma.

NF-Confluence

Summary

Normalization of programs is confluent: any two reduction paths yield the same normal form. Proved via termination + local confluence + Newman’s Lemma.

Statement

%
\label{lem:nf-confluence}
If $P$ reduces to normal form $N_1$ by one reduction sequence
and to $N_2$ by another, then $N_1 = N_2$.

Proof / Justification

[Proof sketch]
The reduction rules are:
\begin{enumerate}
    \item $\sigma_{s,s} \to \varepsilon$ (cancel identity swaps).
    \item $\sigma_{t,s} \circ \sigma_{s,t} \to \varepsilon$
          (cancel inverse swaps).
    \item $\sigma_{s,t} \circ \sigma_{r,s} \to \sigma_{r,t}$
          (compose transitive swaps).
    \item $\sigma_{s,t} \circ \rho \to \rho \circ \sigma_{s,t}$
          (commute swaps past $\rho$).
\end{enumerate}
These rules are terminating (each application reduces
the total instruction count or moves swaps leftward)
and locally confluent (any two overlapping reductions
can be completed to a common result).
By Newman's Lemma (termination $+$ local confluence $\implies$
global confluence), the normal form is unique.

Source Context

• Registry source: book-01.jsonl line 48
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part03/ch13-program-monoid.tex lines 101-106

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.Denotation.ProgramMonoid
• Name: Tau.Denotation.nf_confluence

Dependencies

• Canonical: I.D14, I.T01

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.