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.

- In the function
`λx.x`

, “x” is called a bound variable because it is both in the body of the function and a parameter. - In
`λx.y`

, “y” is called a free variable because it is never declared before hand.

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

When evaluating the
expression `(λx.x)a`

, we replace all occurences of “x” in the function’s body
with “a”.

`(λx.x)a`

evaluates to:`a`

`(λx.y)a`

evaluates to:`y`

You can even create higher-order functions:

`(λx.(λy.x))a`

evaluates to:`λy.a`

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

`(λx.λy.λz.xyz)`

is equivalent to`f(x, y, z) = x(y(z))`

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!**

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`

`a NOT b`

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

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

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

For any number n: `n = λf.f`

so:^{n}

`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)n`

**Challenge:** try defining your own multiplication function!

- A Tutorial Introduction to the Lambda Calculus
- Cornell CS 312 Recitation 26: The Lambda Calculus
- Wikipedia - Lambda Calculus

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 0 contributor(s).