Family 245Mathematical logicNo LeanNot yet digested
Weak normalization implies strong normalization in pure type systems
Proves that weak normalization implies strong normalization for every pure type system: if every legal expression in every valid context has a β-normal form, every β-reduction sequence terminates. This resolves the β-Barendregt–Geuvers–Klop conjecture, including nonfunctional rules and open contexts.
Manuscripts in this family · 1
Weak and strong normalization in pure type systems
Sep 25, 2026·paper.pdf
We prove that every weakly β-normalizing pure type system is strongly β-normalizing. Both properties quantify over all legal expressions in all valid contexts, and reduction acts inside type annotations. No functionality hypothesis is required. This resolves the β-Barendregt–Geuvers–Klop conjecture.