Fundamental Theorems
1. Church-Rosser Theorem (Confluence)
If M reduces to both N1 and N2 (possibly via different reduction sequences), then there exists a term P such that both N1 and N2 reduce to P.
Significance: The order of reductions doesn't matter - if a normal form exists, any reduction strategy will find the same one.
2. Normalization Theorem (for Simply Typed Lambda Calculus)
Every well-typed term in the simply typed lambda calculus has a normal form (strongly normalizes).
Significance: Adding types ensures all computations terminate. The untyped calculus can express non-terminating computations like (λx.x x)(λx.x x).
3. Fixed-Point Theorem
Every lambda term F has a fixed point: there exists a term X such that F X = X. The Y combinator λf.(λx.f(x x))(λx.f(x x)) computes this fixed point.
Significance: This enables recursion without explicit self-reference, proving the lambda calculus is Turing-complete.
4. Church-Turing Thesis
Every effectively calculable function is lambda-definable. Lambda calculus, Turing machines, and recursive functions all define the same class of computable functions.
Significance: Lambda calculus captures the essence of computation itself.
5. Curry-Howard Isomorphism
Types correspond to propositions, terms correspond to proofs, and type inhabitation corresponds to provability. A → B as a type means "given a proof of A, construct a proof of B."
Significance: Programming and proving are the same activity seen from different perspectives.
6. Barendregt's Substitution Lemma
If x ≠ y and x is not free in L, then M[x:=N][y:=L] = M[y:=L][x:=N[y:=L]].
Significance: Substitutions can be reordered under certain conditions - essential for reasoning about reduction.
7. Standardization Theorem
If M reduces to N, then there exists a standard (leftmost-outermost) reduction sequence from M to N.
Significance: The leftmost-outermost strategy is normalizing - it finds a normal form if one exists.
8. Bohm's Theorem
Two distinct beta-normal forms can always be distinguished by some context. If M ≠ N (in normal form), there exists a context C[] such that C[M] = TRUE and C[N] = FALSE.
Significance: Different normal forms represent genuinely different computations - there's no "junk" equivalence.
9. Scott-Curry Theorem
No lambda term can decide equality: there's no term E such that E M N = TRUE iff M = N and E M N = FALSE otherwise.
Significance: Equality of lambda terms is undecidable - reflecting the halting problem.
10. Rice's Theorem (for Lambda Calculus)
Any non-trivial semantic property of lambda terms is undecidable. If P is any property that some lambda terms have and others don't, there's no algorithm to decide P.
Significance: We can't algorithmically determine anything interesting about what lambda terms compute.
11. Subject Reduction (Type Preservation)
If Γ ⊢ M : τ and M →β N, then Γ ⊢ N : τ. Types are preserved under reduction.
Significance: Well-typed programs don't "go wrong" - type safety is maintained through computation.
12. Girard's Paradox
A type system with Type : Type leads to inconsistency (non-termination). This is why dependent type theories use universe hierarchies.
Significance: Self-referential types must be carefully controlled to maintain consistency.
Key Literature
The Calculi of Lambda Conversion
Alonzo Church
1941 - Princeton University Press
The foundational monograph defining lambda calculus and its properties.
Lambda-Calculus and Combinators: An Introduction
J. Roger Hindley & Jonathan P. Seldin
2008 - Cambridge University Press
Modern comprehensive textbook covering both lambda calculus and combinatory logic.
The Lambda Calculus: Its Syntax and Semantics
Henk Barendregt
1984 - North-Holland
The definitive reference work on untyped lambda calculus, covering all major theorems.
Types and Programming Languages
Benjamin C. Pierce
2002 - MIT Press
Essential introduction to type systems, with lambda calculus as the core formalism.
Proofs and Types
Jean-Yves Girard, Yves Lafont, Paul Taylor
1989 - Cambridge University Press
Explores the Curry-Howard correspondence and System F in depth.
To Mock a Mockingbird
Raymond Smullyan
1985 - Knopf
Delightful puzzle book introducing combinatory logic and the Y combinator through bird-themed puzzles.