Learn X in Y minutes

Where X=Lambda Calculus

Lambda Calculus

Lambda calculus (λ-calculus), originally created by Alonzo Church, is the world's smallest programming language. Despite not having numbers, strings, booleans, or any non-function datatype, lambda calculus can be used to represent any Turing Machine!

Lambda calculus is composed of 3 elements: variables, functions, and applications.

Name Syntax Example Explanation
Variable <name> x a variable named "x"
Function λ<parameters>.<body> λx.x a function with parameter "x" and body "x"
Application <function><variable or function> (λx.x)a calling the function "λx.x" with argument "a"

The most basic function is the identity function: λx.x which is equivalent to f(x) = x. The first "x" is the function's argument, and the second is the body of the function.

Free vs. Bound Variables:

Evaluation:

Evaluation is done via β-Reduction, which is essentially lexically-scoped substitution.

When evaluating the expression (λx.x)a, we replace all occurrences of "x" in the function's body with "a".

You can even create higher-order functions:

Although lambda calculus traditionally supports only single parameter functions, we can create multi-parameter functions using a technique called currying.

Sometimes λxy.<body> is used interchangeably with: λx.λy.<body>

It's important to recognize that traditional lambda calculus doesn't have numbers, characters, or any non-function datatype!

Boolean Logic:

There is no "True" or "False" in lambda calculus. There isn't even a 1 or 0.

Instead:

T is represented by: λx.λy.x

F is represented by: λx.λy.y

First, we can define an "if" function λbtf that returns t if b is True and f if b is False

IF is equivalent to: λb.λt.λf.b t f

Using IF, we can define the basic boolean logic operators:

a AND b is equivalent to: λab.IF a b F

a OR b is equivalent to: λab.IF a T b

NOT a is equivalent to: λa.IF a F T

Note: IF a b c is essentially saying: IF((a b) c)

Numbers:

Although there are no numbers in lambda calculus, we can encode numbers using Church numerals.

For any number n: n = λf.fn so:

0 = λf.λx.x

1 = λf.λx.f x

2 = λf.λx.f(f x)

3 = λf.λx.f(f(f x))

To increment a Church numeral, we use the successor function S(n) = n + 1 which is:

S = λn.λf.λx.f((n f) x)

Using successor, we can define add:

ADD = λab.(a S)b

Challenge: try defining your own multiplication function!

Get even smaller: SKI, SK and Iota

SKI Combinator Calculus

Let S, K, I be the following functions:

I x = x

K x y = x

S x y z = x z (y z)

We can convert an expression in the lambda calculus to an expression in the SKI combinator calculus:

  1. λx.x = I
  2. λx.c = Kc provided that x does not occur free in c
  3. λx.(y z) = S (λx.y) (λx.z)

Take the church number 2 for example:

2 = λf.λx.f(f x)

For the inner part λx.f(f x):

  λx.f(f x)
= S (λx.f) (λx.(f x))          (case 3)
= S (K f)  (S (λx.f) (λx.x))   (case 2, 3)
= S (K f)  (S (K f) I)         (case 2, 1)

So:

  2
= λf.λx.f(f x)
= λf.(S (K f) (S (K f) I))
= λf.((S (K f)) (S (K f) I))
= S (λf.(S (K f))) (λf.(S (K f) I)) (case 3)

For the first argument λf.(S (K f)):

  λf.(S (K f))
= S (λf.S) (λf.(K f))       (case 3)
= S (K S) (S (λf.K) (λf.f)) (case 2, 3)
= S (K S) (S (K K) I)       (case 2, 3)

For the second argument λf.(S (K f) I):

  λf.(S (K f) I)
= λf.((S (K f)) I)
= S (λf.(S (K f))) (λf.I)             (case 3)
= S (S (λf.S) (λf.(K f))) (K I)       (case 2, 3)
= S (S (K S) (S (λf.K) (λf.f))) (K I) (case 1, 3)
= S (S (K S) (S (K K) I)) (K I)       (case 1, 2)

Merging them up:

  2
= S (λf.(S (K f))) (λf.(S (K f) I))
= S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (K I))

Expanding this, we would end up with the same expression for the church number 2 again.

SK Combinator Calculus

The SKI combinator calculus can still be reduced further. We can remove the I combinator by noting that I = SKK. We can substitute all I's with SKK.

Iota Combinator

The SK combinator calculus is still not minimal. Defining:

ι = λf.((f S) K)

We have:

I = ιι
K = ι(ιI) = ι(ι(ιι))
S = ι(K) = ι(ι(ι(ιι)))

For more advanced reading:

  1. A Tutorial Introduction to the Lambda Calculus
  2. Cornell CS 312 Recitation 26: The Lambda Calculus
  3. Wikipedia - Lambda Calculus
  4. Wikipedia - SKI combinator calculus
  5. Wikipedia - Iota and Jot

Got a suggestion? A correction, perhaps? Open an Issue on the GitHub Repo, or make a pull request yourself!

Originally contributed by Max Sun, and updated by 8 contributors.