Lambda calculus is the smallest programming language ever invented. It has no numbers, no strings, no booleans, no data structures, no control flow, no types. It has three ways to build an expression and one rule for computing with them. Yet it is Turing complete - capable, in principle, of expressing any computation a real computer can perform. Every functional programming language, Elixir included, is built on the ideas it crystallized.
This article teaches the formal system: where it came from, its three constructs, its one computation rule, and how it encodes something as ordinary as the number 3 using only functions. It also covers what happens when a computation never stops. For the motivation behind putting this on a practical-Elixir site, read Why lambda calculus is on this site first. If the algebra underneath feels shaky, the algebra refresher rebuilds it. This is the middle: the formal system, in full.
Where it came from
Lambda calculus was introduced by the logician Alonzo Church in the 1930s as a formal system for reasoning about functions and computation. As one textbook puts it, “the origins of the functional programming paradigm can be traced back to the 1930s when Alonzo Church introduced Lambda calculus. Lambda calculus presents a theoretical framework for describing functions and their evaluation, and is a mathematical abstraction rather than a programming language. However, Lambda calculus is the foundation of most functional programming languages.”
Church built it to answer questions in mathematical logic: what does it mean for a function to be computable? What is the smallest thing that still counts as computation? The answer was strikingly small. The Stanford Encyclopedia of Philosophy describes it this way: “The λ-calculus is, at heart, a simple notation for functions and application. The main ideas are applying a function to an argument and forming functions by abstraction. The syntax of basic λ-calculus is quite sparse, making it an elegant, focused notation for representing functions.”
The most important result about it, proven over the following decades, is that it is exactly as expressive as a Turing machine. The SEP states the theorem plainly: the lambda calculus “is exactly as expressive as other models of computing, such as Turing machines and register machines.” Church and Turing, working independently in the same decade on different formalizations of “computable,” converged on the same notion of what computation is. We now call it the Church-Turing thesis. Learn lambda calculus and you are learning computation in its most reduced form.
There is a historical irony behind a term you’ll meet shortly. The technique of expressing multi-argument functions as nested single-argument functions is called currying, after Haskell Curry. One popular textbook incorrectly attributes the invention of lambda calculus to Curry; it was Church. Curry’s actual contribution was combinatory logic and the rediscovery of the nested-functions technique, which Moses Schönfinkel had described first in 1924. (The SEP, with dry humor, notes that “perhaps it would be more historically accurate to call the operation fregeing, but there are often miscarriages of justice in the appellation of mathematical ideas.”) Keep this straight: Church invented lambda calculus; currying is named after Curry; Schönfinkel got there first. The next article in this series covers currying in JavaScript vs. Elixir in depth.
The three constructs
The entire grammar of lambda calculus is three rules. The SEP states them as an inductive definition:
The class of λ-terms is defined inductively as follows:
- Every variable is a λ-term.
- If M and N are λ-terms, then so is (M N).
- If M is a λ-term and x is a variable, then (λx M) is a λ-term.
Terms formed according to rule (2) are called application terms. Terms formed according to rule (3) are called abstraction terms.
That’s the whole language. Three constructs:
Variables. A name - x, y, z. Variables are the raw material;
everything else is built from them. If you did the algebra refresher,
you already know what a variable is here: a pure placeholder for a value, not a
storage location.
Abstraction - λx. M, read “the function of x that returns M.” This is a
function definition. The λx binds the variable x as the function’s
parameter; M is the body. The site’s bridge from programming is exact:
λx. M is x => M. So λx. x + 1 is the JavaScript arrow function
x => x + 1 and the Elixir fn x -> x + 1 end. Same idea, different clothes.
(Though - and this matters - pure lambda calculus has no + and no 1. We’ll
get to how those are built.)
Application - M N, read “apply M to N.” This is a function call. If M
is a function and N is its argument, M N means “run M on N.” Application is
left-associative, so M N P means (M N) P: apply M to N first, then apply the
result to P. Parentheses override grouping, as usual.
That’s it. Variables, abstraction, application. There is no fourth construct. There are no numbers (you build them), no conditionals (you build them), no lists (you build them), no recursion (you build it). Those three constructs, plus the one computation rule below, are enough to express any computation. The rest of the article shows how.
One notational point matters here: lambda calculus writes multi-argument
functions as nested single-argument functions. There is no λx y. M. To add
two numbers, write λx. λy. x + y: a function that takes x and returns a
function that takes y and returns the sum. As the SEP puts it, “one can
represent such multiple-arity operations using the apparatus of the
λ-calculus by viewing the operation as taking one input at a time.” This is
currying, the topic of its own article. For now, remember that every function
in lambda calculus takes exactly one argument. Multi-argument behavior comes
from functions returning functions.
The one computation rule: beta-reduction
If the three constructs define the grammar, beta-reduction is the only rule that makes anything happen. The SEP calls it “the central principle of the λ-calculus… the heart of the λ-calculus.” Stated formally:
(β) (λx. M) N ▹ M[x := N]
Read it this way: an application of an abstraction (λx. M) to an argument N
reduces to M[x := N]. That means “M with N substituted for every free
occurrence of x.” A function applied to an argument becomes its body with the
argument substituted for the parameter.
This is the same move as evaluating x² + 1 at x = 3 from algebra: substitute
3 for x everywhere in the body. It is also what calling a function does:
when you call f(3) where f(x) = x² + 1, the language substitutes 3 for x
in the body. Beta-reduction is that move in its purest form. The algebra refresher
covers substitution in detail; here substitution becomes the engine of an entire
formal system.
Let’s reduce a term. Start with the identity function applied to an argument:
(λx. x) y ▹ y
The abstraction λx. x is the identity function: “return whatever you’re
given.” Applied to y, it substitutes y for x in the body x, producing
y. This is the first exercise on the /lambda section and the
simplest possible beta-reduction: one step, done.
A two-argument chain is really two nested one-argument functions:
(λx. λy. x) a b ▹ (λy. a) b ▹ a
First apply λx. λy. x to a. Substitute a for x in the body λy. x to
get λy. a, a function that ignores its argument and returns a. Then apply
that function to b. Substituting b for y changes nothing because y does
not appear in a. The result is a. This function is the Church-encoded
boolean true, which we’ll meet shortly: “return the first of two arguments.”
A composition - applying a function that takes two functions and threads them:
(λf. λg. λx. f (g x)) A B c
▹ (λg. λx. A (g x)) B c
▹ (λx. A (B x)) c
▹ A (B c)
At each step, beta-reduce the leftmost abstraction applied to its first
argument. This is function composition (f ∘ g)(x) = f(g(x)) from algebra,
written as a chain of single-argument applications. If you can substitute
fluently - and the algebra refresher
ends by sharpening that skill - you can beta-reduce. The notation is unfamiliar;
the operation is not.
Normal forms, and when reduction stops
A term is in beta-normal form when it contains no beta-redex: no
subexpression of the form (λx. M) N remains to reduce. The SEP says: “A term
is said to be in β-normal form if it has no β-redexes.” (“Redex” is short for
“reducible expression.”) To evaluate a lambda term, keep beta-reducing until
you reach a normal form. Then there is nothing left to compute.
A natural worry follows: what if a different reduction order gives a different answer? The Church-Rosser theorem says it will not. The SEP states it: “if P reduces to Q and P reduces to R, then there exists a term S such that both Q and R reduce to S.” In plain terms, if a term has a normal form, every terminating reduction sequence reaches the same one, up to renaming bound variables, regardless of which redex you choose first. That is why the /lambda section can grade your reduction against a canonical trace: every correct reduction sequence ends in the same place.
One wrinkle matters: not every reduction strategy terminates, even when a normal form exists. The strategy the site uses is normal order - always reduce the leftmost-outermost redex first - because the SEP’s analysis shows that “the leftmost strategy… is normalizing,” meaning it finds a normal form whenever one exists. Other strategies, such as reducing arguments before the function (called applicative order), can get stuck reducing a divergent argument that the function would have thrown away. Normal order is lazy enough to avoid that trap.
When reduction doesn’t stop
Some terms have no normal form. They reduce forever. The canonical example is Ω (omega), defined as the self-application combinator applied to itself:
Ω = (λx. x x) (λx. x x)
Reduce it. Substitute (λx. x x) for x in the body x x:
(λx. x x) (λx. x x) ▹ (λx. x x) (λx. x x) ▹ ...The result is itself. The SEP says: “Ω reduces in one step to Ω. Every term of every β-reduction sequence commencing with Ω is equal to Ω.” Ω is a computation that runs forever and makes no progress: an infinite loop with no exit, built from the three constructs and the one rule. The /lambda section puts this in front of you: a structural exercise asks whether Ω has a normal form, and the answer is no.
Why does this matter? Lambda calculus has non-termination as a first-class phenomenon despite its minimalism. Some computations finish; some don’t; and (as Church and Turing independently proved) no algorithm can tell you in advance which is which. This is the halting problem inside a formal system with three grammar rules. The section also has you look at the Y combinator, a famous fixed-point combinator does something subtly different - it doesn’t repeat, it grows, spawning a new layer every step - but it, too, never reaches a normal form. Non-termination is not a bug in lambda calculus. It is an unavoidable property of any system powerful enough to be Turing complete.
Data as functions: Church encodings
So far we have functions and substitution. But computation is supposed to deal with things - numbers, booleans, lists. Where are they? The answer is the central idea of the calculus: there are no things. There are only functions. Data is encoded as functions. As one textbook puts it, in lambda calculus “the whole world are Lambda Expressions.”
Church booleans
Start with booleans. A boolean chooses between two options. Encode it as a function that takes two arguments and returns one of them:
TRUE = λx. λy. x -- "return the first argument"
FALSE = λx. λy. y -- "return the second argument"
TRUE throws away its second argument and returns the first; FALSE throws
away its first and returns the second. You saw TRUE already in the
(λx. λy. x) a b ▹ a example. Define the boolean operator AND as a function that
takes two Church booleans and returns a Church boolean:
AND = λp. λq. p q p
Walk through it. AND takes p and q (both Church booleans) and applies p
to q p. If p is TRUE, TRUE q TRUE returns its first argument q, so
AND TRUE q = q, exactly as AND should. If p is FALSE, FALSE q FALSE
returns its second argument FALSE, so AND FALSE q = FALSE, also correct.
Now reduce AND TRUE FALSE:
(λp. λq. p q p) (λx. λy. x) (λx. λy. y)
▹ (λq. (λx. λy. x) q (λx. λy. x)) (λx. λy. y)
▹ (λx. λy. x) (λx. λy. y) (λx. λy. x)
▹ (λy. (λx. λy. y)) (λx. λy. x)
▹ λx. λy. y
= FALSE
AND TRUE FALSE reduces to FALSE by beta-reduction, with no booleans in the
calculus itself. The booleans emerged from function behavior. This is the
/lambda section’s first Church-encoding exercise. Reduce it by hand
and the core idea becomes clear: there was never a boolean primitive. There
were only functions; “true” and “false” are names for two functions that choose.
Church numerals
Numbers use the same trick. The textbook treatment is direct: “This is a way to represent Numbers using Lambda Notation:
0 = λf. λx. x
1 = λf. λx. f x
2 = λf. λx. f (f x)
3 = λf. λx. f (f (f x))Basically, the number is represented by how many times a function f is applied to x. In the zero case, it’s applied 0 times. In the one case, it’s applied 1 time and so on.”
A Church numeral takes a function f and a value x, then applies f to x
that many times. 0 applies it zero times and returns x; 3 applies it three
times and returns f (f (f x)). The number is the count of applications.
There is no integer anywhere, only a function whose behavior is counting.
Now arithmetic. The successor function takes a numeral n and returns the
numeral one larger:
SUCC = λn. λf. λx. f (n f x)
Given a numeral n, which applies f to x some number of times, SUCC n
wraps those applications in one more f. Reduce SUCC TWO and confirm it
gives THREE:
(λn. λf. λx. f (n f x)) (λf. λx. f (f x))
▹ λf. λx. f ((λf. λx. f (f x)) f x)
▹ λf. λx. f (f (f x))
= THREE
SUCC TWO reduces to THREE. Addition follows from the function structure.
From here, multiplication (MULT), pairs (PAIR, FST, SND), and the rest
of the data encodings work the same way: define each operation as a function
whose reduction behavior implements it. The /lambda section walks
you through SUCC, PLUS, MULT, and pairs as reduction exercises. Reduce each one
by hand until the answer emerges.
Why this is the deep idea
Look at what happened. We started with three grammar rules and one computation rule. We built booleans, natural numbers, and arithmetic. No primitive “number” or “boolean” entered the language. They were encoded as patterns of functions, and their operations were beta-reduction. This is what “the whole world are Lambda Expressions” means. Data does not sit beside computation in lambda calculus; data is a particular shape of computation.
Every functional programming language inherited this idea, even when it stopped
being literal about it. When Elixir treats a function as a first-class value you
can pass to Enum.map/2, or JavaScript lets you store an arrow function in a
variable and hand it to Array.prototype.reduce, you are using the
lambda-calculus idea of “function as a thing”: a value in its own right, not just
a named instruction. The calculus is the stripped-down source of that idea. You
don’t write Church numerals in production. But understanding that data can be
functions - that the boundary between “value” and “computation” is a design
choice, not a law of nature - is exactly what functional programming asks you to
internalize.
Free and bound variables, and the one trap
One subtle idea remains. It is where “looks obviously right” and “is actually right” diverge. The existing article flags it as “the one genuinely new idea on this rung,” so I’ll sketch it here and let the section teach it properly.
When a variable appears inside a λx. M, that lambda binds it; it is the
parameter. When it appears outside any lambda that binds it, it is free - it
refers to something defined elsewhere. In λx. x y, the x is bound by the
λx, and the y is free. Beta-reduction replaces only free occurrences of the
variable: (λx. x y) z becomes z y, substituting z for the free x while
leaving the free y untouched.
The trap is capture. Suppose you substitute a term containing a free y
into a body where y is bound. Naive substitution lets the free y get
“captured” by the binder and silently changes the term’s meaning. The classic
case is (λx. λy. x) y. It should not reduce to λy. y: the substituted y
is free in the original term, while λy. y makes it bound. The free y was
captured. The fix is alpha-conversion. Rename the bound variable first:
(λx. λy. x) y reduces to λy₁. y, where the renamed variable avoids the
collision. The SEP states the rule with this proviso: beta-reduction holds
“provided no variable that occurs free in N becomes bound after its substitution
into M.”
This is where lambda calculus stops being “algebra in funny notation” and becomes its own subject. The grammar and beta rule feel familiar from the first exercise; capture-avoidance requires you to slow down. The good news is that it is the only such place. Once it clicks, the rest of the section applies skills you already have.
The connection to programming, in one paragraph
Every functional programming language is a lambda calculus with extras. The
three constructs - variables, function abstraction, function application - are
exactly what you do with functions in Elixir or JavaScript: name inputs (fn x ->),
define a function body, and call a function (f.(x)). Beta-reduction is what
happens at every function call: substitute the argument for the parameter in
the body, then evaluate. Elixir’s anonymous functions are sometimes literally
called “lambdas” (as in Elixir in Action: “because the function isn’t bound to a
global name, it’s also called an anonymous function or lambda”) because they are
lambda calculus’s abstractions with practical conveniences. The pipe operator,
currying, higher-order functions, closures - every one elaborates an idea that
already exists in pure form in the three-construct formal system you just
learned. Seeing lambda calculus directly is not learning unrelated material. It
is seeing the floor everything else was standing on.
Where to go next
This article taught the formal system. The natural next steps:
- Why lambda calculus is on this site for the motivation and what the exercises actually feel like.
- The algebra refresher if any of the substitution, function, or composition material felt rusty.
-
The /lambda section itself - 17 exercises that walk you through
beta-reduction basics, capture-avoidance, Church encodings, non-termination,
and fixed-point combinators, all graded by execution of a pure-Elixir
beta-reducer (never an LLM). Start with
(λx. x) yand reduce. -
The halting problem: why code can only be run, never read
- where the non-termination section of this article ends up: no algorithm can tell you in advance which terms reduce forever.
-
Bits have no meaning: the stored-program bargain
- the other side of the same coin: lambda calculus is where “a program is data” was first made precise, before it became hardware.
Lambda calculus is small, but it turned out to express everything. Three constructs, one rule, and computation follows from them. The exercises make that concrete: you’ll build booleans, numbers, and arithmetic from function application, then watch data emerge from the functions’ structure. Nothing else works quite like it.