Back to Lambda Calculus Evaluator

Lecture: Lambda Calculus Theory

Introduction

Lambda calculus is a formal system in mathematical logic for expressing computation based on function abstraction and application. It was introduced by Alonzo Church in the 1930s as part of his research into the foundations of mathematics.

Despite its simplicity, lambda calculus is Turing complete, meaning it can express any computation that a Turing machine can perform. It forms the theoretical foundation for functional programming languages and has significant applications in type theory and proof theory.

Basic Concepts

Syntax

The syntax of lambda calculus consists of three constructs:

  1. Variables: Single letters (e.g., x, y, z)
  2. Abstraction: Function definitions, written as λx.M, where x is a variable and M is a lambda term
  3. Application: Function application, written as (M N), where M and N are lambda terms

Examples of Lambda Terms

  • Variable: x
  • Abstraction: λx.x (the identity function)
  • Application: (λx.x y) (applying the identity function to y)

Precedence Rules

  • Application associates to the left: M N P = ((M N) P)
  • Abstraction extends as far right as possible: λx.M N = λx.(M N)

Beta Reduction

Beta reduction is the process of evaluating lambda expressions by substituting arguments for parameters. It is written as:

(λx.M) N → M[x := N]

where M[x := N] means "the term M with all free occurrences of x replaced by N."

Example:

(λx.x x) (λy.y) → (λy.y) (λy.y) → λy.y

Beta reduction can be performed in different orders, which leads to different reduction strategies:

  1. Normal order: Leftmost, outermost reductions first
  2. Applicative order: Evaluate arguments before applying functions

Church Encodings

Lambda calculus can encode data and operators using only functions. Here are some common encodings:

Booleans

  • TRUE = λx.λy.x
  • FALSE = λx.λy.y
  • AND = λp.λq.p q p
  • OR = λp.λq.p p q
  • NOT = λp.p FALSE TRUE

Natural Numbers (Church Numerals)

  • 0 = λf.λx.x
  • 1 = λf.λx.f x
  • 2 = λf.λx.f (f x)
  • 3 = λf.λx.f (f (f x))

Arithmetic

  • SUCC = λn.λf.λx.f (n f x)
  • ADD = λm.λn.λf.λx.m f (n f x)
  • MULT = λm.λn.λf.m (n f)

Y Combinator

The Y combinator is a fixed-point combinator that enables recursion in lambda calculus:

Y = λf.(λx.f (x x)) (λx.f (x x))

For any lambda term F, the term Y F is a fixed point of F, meaning:

Y F = F (Y F)

This allows the definition of recursive functions in a system with no built-in recursion.

Applications

Lambda calculus has profound implications in:

  • Programming language design: Functional programming languages (Lisp, Haskell, ML) are based on lambda calculus
  • Type theory: Simply typed lambda calculus and polymorphic lambda calculi form the basis of type systems
  • Proof theory: The Curry-Howard isomorphism relates lambda calculus to intuitionistic logic
  • Computability theory: Providing an alternative formulation of computation equivalent to Turing machines

Evaluation Strategies

Normal Order Evaluation

Normal order evaluation (also called "lazy evaluation") follows the leftmost, outermost reduction strategy:

  1. Always reduce the leftmost, outermost redex first
  2. Evaluate function bodies before evaluating arguments
  3. May evaluate terms that aren't needed in the final result
  4. Always reaches a normal form if one exists

Applicative Order Evaluation

Applicative order evaluation (also called "eager evaluation") follows the leftmost, innermost reduction strategy:

  1. Always reduce the leftmost, innermost redex first
  2. Evaluate arguments before applying functions
  3. More efficient when all terms must be evaluated
  4. May not terminate even if a normal form exists

Alpha Conversion and Variable Capture

Alpha conversion is the process of renaming bound variables to avoid name conflicts. For example:

λx.x is equivalent to λy.y

This becomes important when performing substitutions to avoid variable capture. Variable capture occurs when a free variable in the argument becomes bound after substitution.

For example, in (λx.λy.x y) y, if we naively substitute y for x, we get λy.y y, which changes the meaning. To avoid this, we perform alpha conversion first: (λx.λz.x z) y, which then reduces to λz.y z.

Interactive Examples

Try these expressions in our Lambda Calculus Evaluator:

  • Identity function: λx.x
  • Apply identity to a value: (λx.x) y
  • Boolean TRUE: λx.λy.x
  • Church numeral 2: λf.λx.f (f x)
  • Addition of 1 and 2: (λm.λn.λf.λx.m f (n f x)) (λf.λx.f x) (λf.λx.f (f x))