Substitution Defined

M[x := N] defined inductively. The three cases. Replace free occurrences only.

10 topics • ~1140 words

The compositor has a composing stick and a type piece. The stick has blank slugs tagged with a letter. "Setting type" means: find every blank with that tag and press in a copy of the type piece. One pass, all matching blanks filled at once. If a blank is inside a nested stick that has its own blank for the same letter, that blank is left alone -- it belongs to the inner stick.

Substitution is the engine of computation in lambda calculus. Every calculation, every program, every data structure -- all of it ultimately reduces to this one operation: replacing variables with terms. Get substitution right, and everything else follows.

What Is Substitution?

Substitution is written M[x := N] and means: take the term M, find every free occurrence of the variable x, and replace each one with the term N.

(x y)[x := a] = a y -- the free x is replaced by a
y[x := a] = y -- no x to replace, nothing changes
(x x)[x := a] = a a -- both free xs are replaced

Key rule: only free occurrences of x are replaced. Bound occurrences (those inside a λx) are not affected.

Variable Case: Match

The composing stick holds a single blank slug tagged x. The type piece is N. The blank IS the tag you are looking for -- press the piece in. The entire stick becomes N.

The simplest case of substitution: the term being substituted into is exactly the variable being replaced.

x[x := N] = N

The variable x matches the target, so it is replaced by N. This is the base case that does the actual work -- every other case of substitution either leaves things alone or descends deeper into the term, eventually reaching variables where this rule fires.

Examples:

x[x := a] = a
x[x := λy.y] = λy.y

Variable Case: Mismatch

When the term is a variable that does not match the variable being substituted, nothing happens. The variable is left as-is.

y[x := N] = y

We are looking for x, but we found y. Since y is not the target, it is untouched. Substitution only replaces the specific variable named in the operation.

Examples:

y[x := a] = y
z[x := λy.y] = z
a[b := c] = a

Perform a Substitution

The variable cases of substitution:

x[x := N] = N -- the variable matches, replace it
y[x := N] = y -- different variable, leave it alone

These are the two base cases. Every substitution eventually reduces to one of these: either the variable matches and is replaced, or it does not match and is left unchanged.

Substitution Enters the Body

A composing stick holds a nested stick inside it. The nested stick has its own blanks for y, but the outer stick is setting type for x. The compositor opens the nested stick and fills any x blanks inside -- the y blanks belong to the inner stick and are left alone.

When substitution encounters an abstraction whose parameter is a different variable, it descends into the body:

(λy.M)[x := N] = λy.(M[x := N])

The λy is preserved -- it binds y, not x. Substitution enters the body and continues replacing free xs inside.

Example: (λy.x)[x := a] = λy.a

The free x inside the body is replaced by a. The λy wrapper remains.

When the Argument Is Discarded

The compositor has a type piece ready, but the composing stick has no blanks tagged with that letter. Nothing to fill. The type piece goes back in the case, unused. The stick is unchanged.

Substitution M[x := N] replaces free occurrences of x in M. If x does not appear free in M, there is nothing to replace. The term N is simply discarded -- it has no effect.

y[x := a] = y -- no x to replace
(λy.y)[x := a] = λy.y -- no free x in the body
(λx.x)[x := a] = λx.x -- x is bound, not free

This is not an error. Discarding is a natural part of computation. A function that ignores its argument (like λx.y) simply produces the same result regardless of what x is.

Multiple Occurrences

The composing stick has three blanks all tagged x. The compositor does not fill them one at a time -- one pass, all matching blanks filled at once. Every x blank gets a copy of the type piece simultaneously.

When a variable appears multiple times in a term, substitution replaces all free occurrences simultaneously.

(x x)[x := y] = y y

Both occurrences of x are free, so both are replaced by y. This follows from the application rule: substitution distributes over application, entering both the function and the argument.

(M₁ M₂)[x := N] = (M₁[x := N]) (M₂[x := N])

Only Free Occurrences Are Replaced

A nested composing stick has its own blank tagged x. That blank belongs to the inner stick -- it is not available for the outer setting operation. The outer compositor skips it. Each stick controls its own blanks.

The critical rule: substitution only replaces free occurrences of the target variable. When the term is an abstraction that binds the same variable, substitution stops.

(λx.x)[x := a] = λx.x

The x inside λx.x is bound by λx. It is not a free occurrence, so substitution does not touch it. The entire term is returned unchanged.

Compare:

(λy.x)[x := a] = λy.a -- x is free, replaced
(λx.x)[x := a] = λx.x -- x is bound, untouched

Substitution Distributes Over Application

When the term being substituted into is an application M N, substitution enters both sides independently:

(M₁ M₂)[x := N] = (M₁[x := N]) (M₂[x := N])

The function part and the argument part are each substituted separately, and the results are applied to each other.

Examples:

(x y)[x := a] = a y -- x replaced, y unchanged
(x x)[x := a] = a a -- both sides replaced
(y z)[x := a] = y z -- neither side has x

Substitution Drill

The four rules of substitution:

x[x := N] = N -- variable matches, replace it
y[x := N] = y -- different variable, leave it
(λy.M)[x := N] = λy.(M[x := N]) -- enter body (when y ≠ x)
(M₁ M₂)[x := N] = (M₁[x := N]) (M₂[x := N]) -- enter both sides

When the abstraction binds x itself (λx.M), substitution stops -- all xs in the body are bound, not free.

Ready to test your understanding?

Bitwit uses spaced repetition to help you truly master concepts like this—not just read about them. Each card generates with different values, so you can't just memorize answers.

Practice Substitution Defined →