LetItCrash

Algebra you forgot, and why it's the on-ramp to lambda calculus

LLM-authored, human-reviewed

Proofs & logic

If you clicked through to lambda calculus and your eyes slid off the notation, the problem probably isn’t lambda calculus. It’s the algebra underneath it—the algebra you learned once and let go rusty. Lambda calculus is a formal system built from three ideas - variables, functions, and substitution. When those ideas are sharp, lambda calculus looks like unfamiliar notation for something you already understand. When they’re dull, it looks like alien symbols.

This is the refresher. It covers the school algebra you need to have internalized before the lambda calculus section, and connects each idea to the programming concept wearing the same clothes. It stops where lambda calculus begins: free and bound variables, then substitution. From there, continue with the lambda calculus intro and the /lambda exercises. If you already read f(x) = x² + 1 without flinching and know what “substitute 3 for x” means, skim this. If that sentence made you hesitate, read on. The article uses math symbols (∈, ∪, →, ∘), and the mathematical shorthand article decodes them.

Sets: the universe things live in

Ronald Kneusel opens his Math for Programming with a claim that sounds grand until you read it literally: “Programming is fundamentally about manipulating sets of symbols. Therefore, an understanding of the what and how of sets is as essential to programming as numbers are to arithmetic.” A set is a collection of things—usually numbers, but the things can be anything, including other sets. We write sets with curly brackets:

S = {1, 2, 5}

This defines a set S with three elements. The number of elements is the cardinality, written |S|, so |S| = 3. A set can be infinite. The natural numbers N = {1, 2, 3, ...} go on forever, so |N| = ∞. The empty set, ∅ or {}, has no elements.

Two pieces of notation matter. Membership—“x is an element of S”—is written x ∈ S; “y is not” is y ∉ S. Set-builder notation defines a set with a rule instead of a list: A = {x | x ∈ N, x < 20, x even} means “A is the set of all x in N such that x is less than 20 and x is even.” If you’ve used a list comprehension, you’ve used set-builder notation. Kneusel says the similarity is intentional. Elixir’s for x <- 1..20, rem(x, 2) == 0, do: x and JavaScript’s array.filter(x => x < 20 && x % 2 === 0) are both set-builder notation in code.

The four set operations are the ones you’d expect:

Union:        A ∪ B = {everything in A or B or both}
Intersection: A ∩ B = {everything in both A and B}
Difference:   A − B = {everything in A but not in B}
Subset:       B ⊂ A means every element of B is also in A

Why does this matter for lambda calculus? Every function in mathematics, including lambda calculus, is a mapping between sets: from a domain set to a codomain set. Kneusel puts it this way: “We can abstract the concept of a function in the typical algebra sense to something closer to its role in a programming language: a process that maps inputs to outputs, as opposed to a simple mathematical expression.” That is the on-ramp. A function isn’t really an expression like x² + 1; it is a mapping that takes each input from one set and assigns it an output in another. The expression is a compact description of that mapping.

Functions: the thing everything else is made of

Here is the formal definition. Read it slowly; lambda calculus rests on it. Kneusel states it precisely:

A function (or mapping), f, between two sets, S (the domain) and T (the image, codomain, or range), written as f : S → T, is a set of pairs, (s, t), s ∈ S, t ∈ T, such that every element of S pairs with one, and only one, element of T. We may also write this pairing as f(s) = t.

“One, and only one” gives you two requirements. Every element of S must be paired; the function is defined on the whole domain. Each element of S must pair with exactly one element of T; a function cannot return two different answers for the same input. Programming languages enforce that second rule: a function f(x) returns one value, not several. That rule makes functions predictable enough to reason about.

In programming terms, the domain S is the set of valid inputs—the types your function accepts. The codomain T is the set of possible outputs—the return type. The function is the rule that chooses an output for each input. f : int → int in math is function f(x: number): number in TypeScript. Same idea, different clothes.

You won’t be quizzed on injective vs surjective in the lambda calculus exercises, so the catalog of function properties is beside the point. Keep the core idea: a function is a constrained mapping—total (defined on the whole domain) and single-valued (one output per input). When you write λx. M, you’re defining a function whose domain is “all terms” and whose output is “M with x substituted,” with the same totality and single-valuedness as any algebra function. The functions exercises and the article on function evaluation make this mapping view automatic.

Variables: names that stand for values

This is the concept to sharpen first. It is where math and programming diverge in a way that matters, and it leads directly to lambda calculus’s hardest idea.

In algebra, a variable is a name that stands for a value. The expression x² + 1 is not really about x; it is a template. When you “substitute 3 for x,” replace the name x everywhere with the value 3 and get 3² + 1 = 10. The variable is a placeholder. Substitution fills it, and a function call does the same thing: f(3) means “take the template, substitute 3 for x, simplify.”

The important difference is what a variable is not. In most programming languages, a variable is also a storage location: you can reassign it, mutate it, and read it later. In algebra, it is a pure name. The same name in two places means the same value, and there is no state to change. x + x means “the value, plus itself,” not “read x, then read x again and it might have changed.” Elixir’s immutability gives you exactly this: x = x + 1 rebinds the name to a new value instead of incrementing a box. In Elixir, = isn’t even assignment—it is pattern matching. See Reading Elixir as a JS developer.

Lambda calculus uses this model throughout: pure names, no storage, and substitution as the only operation. Hold onto this: a variable is a placeholder, substitution fills it in, and the same name means the same value everywhere it appears in scope. That is the variable model lambda calculus assumes. The substitution article and the /substitutions exercises drill it to fluency.

Function composition: functions all the way down

If a function is a mapping, feed its output into another function’s input. That is composition, written (g ∘ f)(x) = g(f(x)) and read “g of f of x.” The order matters: in g(f(x)), f runs first, then g runs on f‘s result. With f(x) = x − 3 and g(x) = x², the composition (g ∘ f)(x) is (x − 3)², which expands to x² − 6x + 9. In code, you write g(f(x)) or Elixir’s x |> f() |> g(). The pipe operator makes composition read left-to-right, in data-flow order.

Composition matters because lambda calculus has only functions. Numbers, booleans, pairs, lists—everything is encoded as functions, and operations on them are compositions of functions. When the lambda calculus exercises ask you to reduce (λf. λg. λx. f (g x)) A B c—“compose A and B, then apply the result to c”—you are evaluating a composition. It is the same g(f(x)) move, with lambda abstractions instead of named f and g. The composition article and the /functions exercises take this further, including the two facts lambda later uses: associativity and the identity function id(x) = x, which is λx. x in lambda calculus.

Induction and recursion: the same idea, twice

The last two algebra prerequisites are one idea from two angles: induction (a proof technique) and recursion (its computational twin). You won’t do inductive proofs in the lambda calculus exercises, but induction has the same shape as every recursive function you’ve written: a base case plus a recursive step. That shape lets you argue that a function “always terminates” or “is defined for all inputs.”

Induction, in Kneusel’s compressed form, is a two-step recipe for proving a statement P(n) is true for every natural number:

  1. Demonstrate that P(1) is true.
  2. Demonstrate for every m ≥ 1 that if P(m) is true, then P(m + 1) is also true.

The first step is the base case: show it works at the bottom. The second is the inductive step: show that if it works for some m, it works for m + 1. Together, the steps cover every natural number. P(1) is true by step 1, so P(2) is true by step 2, then P(3) is true by step 2 again, and so on to infinity. It feels like cheating because you proved P(m+1) by assuming P(m). But the assumption says only, “if it’s already true one rung down,” and the base case gives you the bottom rung.

Recursion is induction run backwards. Induction proves “P holds for all n” with a base case and an inductive step. Recursion defines a function “for all inputs” with a base case and a recursive case. Kneusel again, in the chapter that follows induction:

Recursion involves two conditions:

  • A base case where the problem is now simple enough to solve without further division.
  • A recursive case where the problem is written as a combination of simpler versions of itself.

The structural parallel is exact. Induction’s base case is recursion’s base case: the smallest input, handled directly. Induction’s inductive step is recursion’s recursive case: the assumption “P(m) holds” becomes the recursive call “solve the smaller version.” Every recursive function you trust to terminate is, secretly, an inductive argument that it does. The base case makes it stop; the recursive case moves it toward that case.

Why does this matter before lambda calculus? The lambda calculus exercises include terms that don’t terminate, most famously Ω (omega), defined as (λx. x x)(λx. x x), which reduces to itself forever. Recognize the pattern: “this has no base case, so it will never bottom out.” It is the same diagnosis as “this recursive function has no base case, so it will stack-overflow.” The vocabulary of base case and termination turns Ω into a familiar bug instead of a mystery. The section even has a non-termination exercise asking exactly: does this term have a normal form, or does it reduce forever?

Substitution: the one operation that runs the show

Everything above was warm-up. Lambda calculus is built on this operation, and this is where the refresher hands off to the exercises.

Substitution means replacing a variable with a value (or another expression) throughout a formula. “Evaluate x² + 1 at x = 3“ means “substitute 3 for x,” giving 3² + 1 = 10. A function call is substitution: the function is a template, and the call fills the hole. The substitution article and the /substitutions exercises drill this move until it is automatic.

Lambda calculus takes that operation—substitute the argument for the bound variable throughout the function body—and makes it the only operation in the formal system. There are no numbers, no arithmetic, and no built-in data structures. There are only:

  • Variables - x, y, z (the placeholders you already understand)
  • Abstractions - λx. M, read “the function of x that returns M” (a function definition; the site’s bridge is λx. M is x => M, mapping straight onto a JavaScript arrow function)
  • Applications - M N, read “apply M to N” (a function call)

And the single rule that makes it run, beta-reduction: (λx. M) N becomes M with N substituted for every free occurrence of x. That’s it. The whole calculus is substitution, repeated until nothing more can be substituted. If you can substitute fluently in algebra—“evaluate x² + 1 at x = 3“—you can beta-reduce. The notation is unfamiliar; the operation is not.

Where this hands off

This refresher stops here. The next concept—free versus bound variables, and the subtlety of capture-avoiding substitution—is where lambda calculus stops being “algebra in funny notation” and becomes its own subject. The lambda calculus section calls it “the one genuinely new idea on this rung”: when you substitute a term containing a free variable y into a function whose bound variable is also named y, naive substitution lets the argument’s free y get captured by the binder and silently changes the expression’s meaning. The fix is to rename the bound variable first, a process called alpha-conversion. That idea is genuinely new, and the section teaches it after the basics.

You don’t need to learn that here. Arrive at the exercises with these ideas sharp: what a set and membership are, so “domain” and “codomain” mean something; what a function is as a mapping, so λx. M reads as “a function”; what a variable is as a pure name, so substitution feels natural; what composition is, so f (g x) reads as nested function calls; what base case and termination mean, so a non-terminating reduction looks like a familiar failure mode; and the substitution move itself, so beta-reduction feels like an old friend in new notation. Sharpen those, and the lambda calculus exercises’ first stage—five exercises of plain beta-reduction—will feel like applying algebra you already know. That is exactly what it is.

When you’re ready, read Why lambda calculus is on this site for the framing and motivation, then do the /lambda exercises. Both assume the fluency this refresher rebuilds.

Where to go next

Related exercises

← Back to articles

Exercises