Math 2.0

Mathematical logic and foundations Theorem

Strong normalization of simply typed lambda calculus

Builds on Simply typed lambda calculusBeta reductionNormalization propertyChurch–Rosser theoremCurry–Howard correspondence

Statement

Let tt be a term of the simply typed lambda calculus with Γ⊢t:τ\Gamma \vdash t : \tau for some context Γ\Gamma and type τ\tau. Then tt is strongly normalizing for beta reduction: there is no infinite sequence t=t0→βt1→βt2→β⋯t = t_0 \to_\beta t_1 \to_\beta t_2 \to_\beta \cdots.

Remarks

The standard proof is Tait's method of reducibility. For each type τ\tau, one defines a set of reducible terms by induction on τ\tau. At a base type they are the strongly normalizing terms, and at σ→τ\sigma \to \tau they are the terms that send reducible arguments to reducible results. One shows that reducible terms are strongly normalizing, and then that every typed term is reducible, by induction on its typing derivation. A direct induction on terms fails, because substitution can copy subterms and create new redexes; the reducibility sets give a stronger induction hypothesis.

The untyped term Ω=(λx. x x)(λx. x x)\Omega = (\lambda x.\, x\, x)(\lambda x.\, x\, x) reduces to itself forever, and the theorem explains why no type can be given to it. Strong normalization together with the Church–Rosser theorem gives each typed term a unique normal form, so equality of typed terms is decidable by comparing normal forms. It also shows that some type has no closed term, which gives the consistency of the matching logic.

Going deeper

For a student

The theorem is the normalization property in its strongest form for the simply typed calculus. Through the Curry–Howard correspondence it says that every proof in the implication fragment of intuitionistic natural deduction has a normal form. This is a form of cut elimination. The price is expressiveness: the typed calculus is not Turing complete, since every typed program halts. The same reducibility method, with Girard's reducibility candidates, proves strong normalization for System F.

Reading path

To understand this page from the ground up, read these 28 pages in order. The foundations come first.

Show the path as a graph
Beta normal form, concept, no evidence levelBeta normal formconceptBeta reduction, concept, no evidence levelBeta reductionconceptElement, definition, no evidence levelElementdefinitionIntuitionistic logic, concept, no evidence levelIntuitionistic logicconceptLambda calculus, concept, no evidence levelLambda calculusconceptNormalization property, concept, no evidence levelNormalization propertyconceptProposition, concept, no evidence levelPropositionconceptSet, concept, no evidence levelSetconceptChurch–Rosser theorem, statement, no evidence levelChurch–Rosser theoremstatementSet, definition, no evidence levelSetdefinitionConjunction, definition, no evidence levelConjunctiondefinitionDisjunction, definition, no evidence levelDisjunctiondefinitionImplication, definition, no evidence levelImplicationdefinitionNegation, definition, no evidence levelNegationdefinitionBiconditional, definition, no evidence levelBiconditionaldefinitionTruth table, concept, no evidence levelTruth tableconceptModus ponens, concept, no evidence levelModus ponensconceptMathematical proof, concept, no evidence levelMathematical proofconceptPropositional logic, concept, no evidence levelPropositional logicconceptTautology, definition, no evidence levelTautologydefinitionLogical equivalence, definition, no evidence levelLogical equivalencedefinitionDouble negation law, statement, no evidence levelDouble negation lawstatementProof by contradiction, concept, no evidence levelProof by contradictionconceptRussell's paradox, statement, no evidence levelRussell's paradoxstatementType theory, concept, no evidence levelType theoryconceptCurry–Howard correspondence, concept, no evidence levelCurry–Howard correspo…conceptSimply typed lambda calculus, concept, no evidence levelSimply typed lambda c…conceptStrong normalization of simply typed lambda calculus, statement, no evidence levelStrong normalization …statement
Each page uses the pages above it. The colour of the bar on a box shows how strong the evidence is, and the box also gives it as text. The list has the same pages.
  • no evidence level
  1. Beta normal form concept
  2. Beta reduction concept
  3. Element definition
  4. Intuitionistic logic concept
  5. Lambda calculus concept
  6. Normalization property concept
  7. Proposition concept
  8. Set concept
  9. Church–Rosser theorem statement
  10. Set definition
  11. Conjunction definition
  12. Disjunction definition
  13. Implication definition
  14. Negation definition
  15. Biconditional definition
  16. Truth table concept
  17. Modus ponens concept
  18. Mathematical proof concept
  19. Propositional logic concept
  20. Tautology definition
  21. Logical equivalence definition
  22. Double negation law statement
  23. Proof by contradiction concept
  24. Russell's paradox statement
  25. Type theory concept
  26. Curry–Howard correspondence concept
  27. Simply typed lambda calculus concept
  28. Strong normalization of simply typed lambda calculus statement

Where this leads

1 page builds on this one.

Further reading

  1. Web https://en.wikipedia.org/wiki/Normal_form_(abstract_rewriting)
  2. Web https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus
About this page
TagV2Z855MFPC
URIm2://V2Z855MFPC
Kindstatement, theorem
WritingW0 stub
MSC03B40, 03F05, 68N18
StatusThis copy of the site has no build data. Run m2 status V2Z855MFPC.
AboutSimply typed lambda calculus
UsesSimply typed lambda calculus, Beta reduction, Normalization property, Church–Rosser theorem, Curry–Howard correspondence
Changed3 November 2026

Markdown · JSON · Edit on GitHub

What this page needs for W1

  • an inventory row: the row of the inventory that the node accounts for (0 of 1)
  • a source with a locator (0 of 1)

The writing levels say how complete the text of a page is. They do not measure its truth.

What links here

Used by