Normalization

Origin. Gentzen (1935) cut elimination. Prawitz (1965) for natural deduction. Proofs simplify to canonical form. Foundation for proof theory and type theory.

Models. Detours: intro followed by elim. Normalization: remove detours. Strong normalization: all reduction sequences terminate. Canonical proofs reveal structure.

Formalism.

Detour (natural deduction): ⋮ ─── ∧I A ∧ B ─── ∧E₁ A

Reduces to: ⋮ A

β-reduction (implication): [A] ⋮ B ─── →I A → B A ─────── →E B

Reduces to proof of B with A substituted.

Normal form: No detours. Subformula property: only subformulas of conclusion appear.

Strong normalization: All reduction sequences terminate. Well-typed λ-terms: SN. Proof: logical relations, reducibility candidates.

Weak normalization: Some reduction sequence terminates. Weaker property.

Church-Rosser: If M →* N₁ and M →* N₂, then ∃P. N₁ →* P and N₂ →* P. Unique normal form (if exists).

Cut elimination: Sequent calculus analog. Remove cut rule from proofs. Gentzen's Hauptsatz.

Symbols.

Symbol	Unicode	Name	Meaning
→	U+2192	Reduces	One step
→*	—	Reduces	Many steps
SN	—	Strongly norm	All paths finite
WN	—	Weakly norm	Some path finite
↓	—	Normal form	Irreducible

Metatheory. Consistency via normalization. Curry-Howard: normalization = evaluation. Proof identity. Complexity bounds.

Applies to. Proof assistants. Type theory. λ-calculus. Program termination. Constructive logic.

Limitations. Proving SN hard. Non-termination in some systems. Confluence needed. Extensions may break SN.