Newman's Lemma

Newman's Lemma (Theorem 3.9) is the single most useful theorem about ARSs:

If an ARS is weakly confluent and terminating, then it is confluent.

In symbols:

Why this is a big deal. Proving confluence directly requires checking the
diamond for ALL pairs $b, c$ reachable from any $a$ in ANY number of steps.
That's an infinite condition. Weak confluence only requires checking pairs that
are one step away from $a$. Combined with termination, you can use induction on
the length of reduction sequences to lift "local" to "global".

The proof sketch (induction on the number of steps from $a$ to $c$):

- Base: $a \to^* c$ in 0 steps means $c = a$. Trivial.
- Inductive step: assume it works for one fewer step. If $a \to^* c$ in
$k$ steps, factor the last step: $a \to^* c' \to c$. By IH, $b$ and $c'$
have a common reduct. Then $c'$ and $c$ (one step) join by weak confluence.
Transitivity of "having a common reduct" closes the diamond.

Practical impact. To prove your rewrite system gives unique answers:
1. Prove termination (often by a well-founded measure).
2. Prove weak confluence (only check one-step divergences).
3. Conclude confluence by Newman's Lemma.

This pattern appears in theorem provers, programming language semantics, and
the metatheory of $\lambda$-calculus.

Idea 3 (slides 367). When stating or proving anything, push it as low in the theory graph as possible — i.e., state it in the most general structure that still supports it.

Why? Because a theorem proved at a low node automatically propagates to all nodes above it (via the 'copy along any edge' principle from Idea 2). Stating a theorem too high is wasteful: you re-prove it for every specialisation.

Example. Associativity of $+$. It is true at any node that has a binary operation. So we should prove it once at the lowest such node — say at Semigroup (where the operation is associative) — and inherit it up to Monoid, Group, AbelianGroup, etc.

Anti-pattern. Proving associativity separately for every concrete group ($\mathbb{Z}$, $\mathbb{Q}$, $\mathbb{R}$, modular arithmetic, ...) instead of once at Semigroup. This is the 'exponential blowup' that 'object-oriented math' prevents.

The graph-theoretic concepts form their own theory graph, parallel to the algebra graph:

Magma
  |
 Univ (universe)
  |
 Magma ───────────── PSet (powerset)
  |                    |
 UAG (undirected,     Forest
  |   attributed     /     \
 UGraph             Tree    DAG
  |                 |       |
DiGraph            Graph ───── Graph (with cycles)

Where:
- Magma $\langle S, \circ \rangle$ — a set with a binary operation.
- PSet — a set with a unary predicate.
- Forest — a directed acyclic graph where each node has at most one parent.
- Tree — a forest with a distinguished root.
- DAG — directed acyclic graph (sharing allowed).
- UGraph / DiGraph / UAG — undirected / directed / attributed.

Inheritance along edges copies axioms (e.g. DAG → Tree adds the 'one parent' rule; DAG → Forest adds acyclicity; UGraph → DiGraph adds edge direction).

Definitions like root (the unique source in a tree), path (a sequence of adjacent edges), cycle (a path returning to start), and in-degree (number of incoming edges) all live at the appropriate node and propagate down the graph.

A DAG (directed acyclic graph) $G = \langle V, E \rangle$ has a finite number of vertices. We can do induction on $|V|$ (the size of the DAG).

Theorem. Every DAG has a vertex with in-degree 0 (a 'source').

Proof by induction on $|V|$.
- Base $|V| = 0$: Empty DAG has no vertices, so the statement is vacuously true (no vertex to violate the claim).
- Base $|V| = 1$: The single vertex has in-degree 0. ✓
- Step $|V| = k + 1$: Assume the claim holds for all DAGs with $\leq k$ vertices. Take a DAG $G$ with $k + 1$ vertices.
- Case 1: Some vertex $v$ has in-degree 0. Done.
- Case 2: Every vertex has in-degree $\geq 1$. Then we can 'peel off' a maximal vertex (one with no outgoing edges — every DAG has one, since otherwise we'd have an infinite descent). Removing $v$ gives a smaller DAG $G'$ with $k$ vertices. By IH, $G'$ has a source $u$ with in-degree 0 in $G'$. Either $u$ is a source in $G$ too (no edge was added incident to $u$), or $u = v$. But $u$ has in-degree 0 in $G'$ — meaning no other vertex points to it. Contradiction with Case 2 unless $u$ is also a source in $G$. So $u$ is a source in $G$. ✓

Reading. The trick: pick a sink (out-degree 0, no outgoing edges). Such a vertex exists in every non-empty DAG because otherwise an infinite walk would exist (which would force a cycle). Removing the sink gives a strictly smaller DAG, so the IH applies.

Topological sort corollary. Iteratively removing sources produces a linear ordering of the vertices — a topological sort. This is what tsort does in graph algorithms.