Quartz 4

Lambda Calculus

5 min read

Lambda calculus is a formal system in mathematical logic and computer science for expressing computation based on function abstraction and application. Developed by Alonzo Church in the 1930s, it forms the theoretical foundation of functional programming languages, including Haskell.

Core Concepts

The lambda calculus consists of three basic components:

  1. Variables: Symbols that represent parameters or values (e.g., x, y, z)
  2. Function abstraction: Creating a function that maps an input to an output
  3. Function application: Applying a function to an argument

Syntax

The syntax of the lambda calculus can be defined as:

<expr> ::= <variable>             -- Variable
         | λ<variable>.<expr>     -- Abstraction (creating a function)
         | <expr> <expr>          -- Application (applying a function)

Examples

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

Rewrite Rules

α-conversion (Alpha Conversion)

Alpha conversion allows renaming bound variables as long as no free variables are captured:

λx.M ≡ λy.M[y/x]

where M[y/x] means “substitute y for x in M”, and y is not already a free variable in M.

Example:

λx.x ≡ λy.y

β-reduction (Beta Reduction)

Beta reduction represents function application - substituting the argument for the parameter in the function body:

(λx.M) N → M[N/x]

Example:

(λx.x+1) 5 → 5+1 → 6

η-conversion (Eta Conversion)

Eta conversion captures the idea that two functions are equivalent if they give the same result for all inputs:

λx.(f x) ≡ f

where x does not appear free in f.

Church Encodings

Since lambda calculus has only functions, we need to encode data using functions.

Booleans

true = λx.λy.x
false = λx.λy.y

These encode the behavior of true and false in an if-then-else construct:

  • true returns the first argument
  • false returns the second argument

Natural Numbers (Church Numerals)

Church numerals represent natural numbers by applying a function n times:

0 = λf.λx.x
1 = λf.λx.f x
2 = λf.λx.f (f x)
3 = λf.λx.f (f (f x))
...
n = λf.λx.f^n x  (f applied n times to x)

Arithmetic Operations

succ = λn.λf.λx.f (n f x)      -- Successor function
add = λm.λn.λf.λx.m f (n f x)  -- Addition
mult = λm.λn.λf.m (n f)        -- Multiplication

Fixed Point Combinators

Fixed point combinators allow us to define recursive functions in the lambda calculus, where recursion isn’t directly supported.

The Y combinator is a classic fixed point combinator:

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

Given a function f, Y f is a fixed point of f, meaning that:

Y f = f (Y f)

This allows us to create recursive functions.

Connection to Haskell

Haskell’s syntax is directly inspired by lambda calculus. For example:

Lambda calculus:

λx.λy.x + y

Haskell:

\x -> \y -> x + y
-- Or equivalently
\x y -> x + y

Many Haskell concepts can be traced back to lambda calculus:

  • Anonymous functions (lambdas)
  • Higher-order functions
  • Currying
  • Lazy evaluation (similar to normal-order evaluation in lambda calculus)

Evaluation Strategies

Normal Order Evaluation

In normal order evaluation (which Haskell uses a variant of), function arguments are substituted without being evaluated, and then the resulting expression is evaluated.

Example:

(λx.x+x) (1+2)
→ (1+2)+(1+2)
→ 3+3
→ 6

Applicative Order Evaluation

In applicative order evaluation, function arguments are evaluated before being substituted.

Example:

(λx.x+x) (1+2)
→ (λx.x+x) 3
→ 3+3
→ 6

Church-Rosser Theorem

The Church-Rosser theorem states that if an expression can be reduced in two different ways, then there exists a common form that both reduction paths eventually reach.

This ensures that the lambda calculus is confluent, meaning the order of reductions doesn’t affect the final result (if it exists).

Computability and the Lambda Calculus

The lambda calculus is Turing complete, meaning it can express any computable function. This was one of the key insights that led to the development of modern computers.

Examples in Haskell

Encoding Church Numerals in Haskell

-- Church numeral type
type Church a = (a -> a) -> a -> a
 
-- Converting from Integer to Church
toChurch :: Integer -> Church a
toChurch 0 = \f x -> x
toChurch n = \f x -> f (toChurch (n-1) f x)
 
-- Converting from Church to Integer
fromChurch :: Church Integer -> Integer
fromChurch n = n (+1) 0
 
-- Church arithmetic
churchSucc :: Church a -> Church a
churchSucc n = \f x -> f (n f x)
 
churchAdd :: Church a -> Church a -> Church a
churchAdd m n = \f x -> m f (n f x)
 
churchMult :: Church a -> Church a -> Church a
churchMult m n = \f -> m (n f)

Y Combinator in Haskell

-- Y combinator (with a type annotation to make it work in Haskell)
y :: (a -> a) -> a
y f = (\x -> f (x x)) (\x -> f (x x))
 
-- Using Y to define factorial
factorial = y $ \f n -> if n <= 0 then 1 else n * f (n-1)

Note: This won’t actually work in Haskell due to the type system, but it illustrates the concept.

Key Points to Remember

  1. Lambda calculus consists of variables, abstractions (functions), and applications
  2. Alpha conversion renames bound variables
  3. Beta reduction substitutes arguments into function bodies
  4. Church encodings represent data as functions
  5. Fixed point combinators enable recursion
  6. The lambda calculus is Turing complete
  7. Haskell’s syntax and semantics are directly inspired by lambda calculus

Graph View

Backlinks