Everything is a function
Lambda calculus is a tiny formal language with exactly three kinds of expression: a variable, a function definition and a function application. A function definition is written with the Greek letter lambda, like this: the function that takes x and returns x is written λx.x. Applying a function to an argument is written by putting them next to each other.
That is the whole language. There are no numbers, no booleans, no loops and no data structures built in. Everything else is encoded using functions. It was introduced in the 1930s by Alonzo Church as part of research into the foundations of mathematics, and it is one of the classic answers to what it means for something to be computable.
The only rule: substitution
Computation has one step, usually called beta reduction. To apply λx.body to an argument, replace every occurrence of x in the body with the argument. For example, (λx.x) y reduces to y, because the body is just x and x is replaced by y.
A slightly bigger one: (λx.λy.x) a b. The outer function takes x and returns another function that takes y. Applying to a gives λy.a, and applying that to b gives a, since y does not occur. This particular function, which keeps its first argument and discards its second, is a close relative of the K combinator.
Numbers from nothing
How do you count with only functions? One answer is Church numerals. The number n is represented as a function that takes a function f and a value x and applies f to x exactly n times.
- Zero is λf.λx.x (apply f no times).
- One is λf.λx.f x.
- Two is λf.λx.f (f x).
Arithmetic follows. A successor function takes a numeral n and returns one with an extra application of f, written λn.λf.λx.f (n f x). Check it on zero: applying successor to zero gives λf.λx.f (zero f x), and zero f x reduces to x, so the result is λf.λx.f x, which is one. Addition, multiplication and exponentiation can be defined in similar fashion.
Booleans work the same way: true can be a function that returns its first argument and false one that returns its second, which turns “if” into plain application. Pairs, lists and other structures are encoded with similar tricks.
Loops without loops
Repetition needs a trick, because a function cannot refer to itself by name. A fixed-point combinator, of which the best known is usually called the Y combinator, builds recursion out of ordinary application. The details are a famous brain-teaser: Y applied to a function f behaves like f applied to the result of Y f, which lets f call itself indirectly. This is the foundation for recursion in a language with no names for functions.
It also connects lambda calculus to the halting problem. Some lambda expressions reduce forever, so deciding whether an arbitrary expression reaches a final form is undecidable, just as for other universal systems.
How esoteric languages use it
Lambda calculus shows up in odd languages in several ways.
- Directly. Some hobby languages are essentially lambda calculus with different notation, sometimes using binary encodings so that a program is a string of bits. The aim is usually to have a minimal, precise definition of “the smallest universal language” or to experiment with very short programs.
- Through combinators. Languages such as Unlambda use the variable-free cousin of lambda calculus, and the translation between the two is a standard technique.
- As a source of ideas. First-class functions, closures and laziness in many mainstream languages descend from this tradition, though the connection can be loose.
The recurring appeal is minimalism: a complete programming language whose entire definition fits on a few lines.
Strengths and awkwardness
Lambda calculus is excellent for reasoning. Its single rule makes it easy to define precisely, and a lot of theoretical work about programs is done in lambda-calculus-like settings. But it is awkward to write by hand for practical tasks. Numbers are slow to compute with, there is no built-in input or output, and a tiny mistake in a substitution can produce a very different result. For esoteric purposes, those are features as much as flaws.
There are also subtleties. Which reduction to apply first matters in practice. Some strategies get stuck in infinite loops on expressions that other strategies would finish, which is part of why lazy and eager evaluation are discussed so much in language design.
Place in the bigger picture
Lambda calculus is one of several equivalent models of computation, alongside Turing machines and rewriting systems. The Church-Turing thesis is the informal claim that these models capture everything we would reasonably call computable. In practice, it is a bridge between the stepwise world of machines and the expression-based world of functions, and esoteric languages are a playful way to cross it. If you try one exercise, try reducing “successor of one” to two by hand. It takes only a few lines and makes the encoding feel real.