12.2 Lambda calculus and proof normalization

Lambda calculus is a formal system for expressing computation through function abstraction and application. It provides a simple yet powerful foundation for studying computability, programming languages, and proof theory, connecting abstract mathematics with practical computer science.

In this section, we explore lambda calculus basics, its properties, and its relationship to proofs. We'll see how lambda terms encode data and computation, and how concepts like normalization and the Curry-Howard correspondence link lambda calculus to logic and programming.

Lambda Calculus Basics

Syntax and Evaluation Rules

Top images from around the web for Syntax and Evaluation Rules

• 

  Haskell for Lambda Calculus, Type Inferencing - Stack Overflow View original

  Is this image relevant?

• 

  Figure 1: Lambda expression syntax View original

  Is this image relevant?

• 

  Conversion of lambda calculus terms into graphs | chorasimilarity View original

  Is this image relevant?

• 

  Haskell for Lambda Calculus, Type Inferencing - Stack Overflow View original

  Is this image relevant?

• 

  Figure 1: Lambda expression syntax View original

  Is this image relevant?

1 of 3

Top images from around the web for Syntax and Evaluation Rules

• 

  Haskell for Lambda Calculus, Type Inferencing - Stack Overflow View original

  Is this image relevant?

• 

  Figure 1: Lambda expression syntax View original

  Is this image relevant?

• 

  Conversion of lambda calculus terms into graphs | chorasimilarity View original

  Is this image relevant?

• 

  Haskell for Lambda Calculus, Type Inferencing - Stack Overflow View original

  Is this image relevant?

• 

  Figure 1: Lambda expression syntax View original

  Is this image relevant?

1 of 3

• Lambda terms consist of variables, abstractions (anonymous functions), and applications
  • Variables are single letters used to represent values (x, y, z)
  • Abstractions are functions defined using the λ symbol followed by a variable and a body (λx.M where M is another lambda term)
  • Applications represent the application of a function to an argument (M N where M and N are lambda terms)
• Beta reduction is the process of evaluating an application by substituting the argument for the bound variable in the function body
  • Example: (λx.x) y $\beta$-reduces to y by replacing all occurrences of x with y in the function body
• Alpha conversion allows renaming bound variables in a lambda term without changing its meaning
  • Example: λx.x and λy.y are equivalent terms related by $\alpha$-conversion
• Normal form is a lambda term that cannot be further reduced using $\beta$-reduction
  • Terms in normal form represent fully evaluated expressions

Encoding Data and Computation

• Church encodings allow representing data types like booleans, numbers, and pairs using lambda terms
  • Church booleans: true = λx.λy.x, false = λx.λy.y
  • Church numerals: 0 = λf.λx.x, 1 = λf.λx.f x, 2 = λf.λx.f (f x), ...
• Lambda calculus is Turing complete can express any computable function
  • Recursive functions can be defined using fixed-point combinators (Y combinator)
  • Example: factorial = λf.λn.if (isZero n) 1 (multiply n (f (pred n)))

Properties of Lambda Calculus

Confluence and Uniqueness of Normal Forms

• Church-Rosser theorem states that if a term can be reduced to two different terms, there exists a common term to which both can be reduced
  • Implies confluence: reduction order does not affect final result
  • Example: (λx.x x) (λy.y) $\beta$-reduces to (λy.y) (λy.y) regardless of evaluation order
• Uniqueness of normal forms is a consequence of the Church-Rosser theorem
  • If a term has a normal form, it is unique up to $\alpha$-conversion

Termination and Decidability

• Strong normalization property holds for some variants of lambda calculus (simply typed lambda calculus)
  • Guarantees that every reduction sequence terminates in a normal form
  • Implies decidability of normalization and type checking
• Untyped lambda calculus is not strongly normalizing some terms have infinite reduction sequences
  • Example: (λx.x x) (λx.x x) $\beta$-reduces to itself indefinitely
  • Undecidable to determine if an arbitrary term has a normal form

Lambda Calculus and Proofs

Correspondence with Natural Deduction

• Cut elimination in natural deduction corresponds to $\beta$-reduction in lambda calculus
  • Cut rule allows using a lemma (intermediate proof) in a larger proof
  • Elimination of cuts yields a direct proof analogous to a normal form
• Typed lambda calculus assigns types to lambda terms, restricting well-formed expressions
  • Simple types: $\tau ::= \alpha \mid \tau \to \tau$ (base types and function types)
  • Well-typed terms cannot "go wrong" during evaluation (type soundness)
• Curry-Howard correspondence relates proofs in intuitionistic logic to typed lambda terms
  • Propositions correspond to types, proofs correspond to terms
  • Example: $A \to B$ corresponds to the type of functions from $A$ to $B$
  • Proof normalization (cut elimination) corresponds to $\beta$-reduction

Applications in Programming Languages

• Functional programming languages (Haskell, ML) are based on typed lambda calculus
  • Higher-order functions, type inference, pattern matching, lazy evaluation
• Dependently typed languages (Coq, Agda) extend the Curry-Howard correspondence
  • Types can depend on values, allowing expressing precise specifications
  • Proofs of program properties can be expressed and checked within the language
• Proof assistants (Isabelle, Lean) use lambda calculus as a foundation for formal reasoning
  • Proofs are represented as lambda terms, can be checked and manipulated programmatically
  • Enable formalization of mathematics and verification of software/hardware