Free and Bound Variables

Bound vs free occurrences. Which variables belong to which lambda.

10 topics • ~1211 words

A composing stick has tagged blank slugs — positions marked with a name, waiting for a type piece. The tag x means "this blank will be filled when someone provides type for x." Every blank tagged x in this stick is bound — the stick controls what goes there.

But if the text mentions a tag that has no matching blank in this stick, that tag is free. It refers to something outside — type piece from a different stick, a different job entirely. The current stick cannot fill it.

Before we can define substitution correctly, we need to know which variables "belong" to which λ. Getting this wrong is the most common source of errors in lambda calculus.

What Makes a Variable Bound?

A variable occurrence is bound if there is a λ in the expression that binds it. It is free if no λ claims it.

In λx.x y:

x is bound — λx captures it
y is free — no enclosing λy binds it

The same variable name can be free in one place and bound in another: (λx.x) x — the first x is bound (inside λx), the second x is free (outside).

What Makes a Variable Free?

A free tag in a composing stick is a reference the stick cannot resolve. The stick has no blank for that name — the type piece must come from elsewhere. The stick does not treat this as an error. It simply cannot fill what it does not control.

A variable occurrence is free if no enclosing λ binds it. It references something outside the current term.

In λx.x y:

y is free — no λy appears anywhere enclosing it
x is bound — λx encloses it

Free does not mean "undefined" or "error." A free variable is simply a reference to something the current term does not control. The term y by itself is perfectly valid — y is free, and that is fine.

Free or Bound?

To determine whether a variable occurrence is free or bound, look for an enclosing λ with the same name:

Bound: a λ with that name wraps around the occurrence
Free: no such λ exists

In λx.x y: x is bound (enclosed by λx), y is free (no λy). In (λx.x) y: x is bound, y is free. In λy.x: x is free (no λx), y is not even an occurrence in the body — it only appears as the parameter name.

Same Name, Different Status

Two composing sticks sit on the bench. The first has a tagged blank for x — every x inside that stick is bound to it. The second stick has no blank for x at all. If x appears in the second stick, it is free — a reference to type piece from somewhere else. Same letter, different sticks, different status.

The same variable name can appear both free and bound in a single expression. What matters is which occurrence you are looking at and whether a λ with that name encloses that particular occurrence.

In (λx.x) x:

The first x (inside λx) is bound
The second x (outside λx) is free

The name x does not have a single status. Each occurrence is evaluated independently based on its position.

Why Free Variables Matter

When we apply (λx.M) N, we substitute N for x in M. But crucially, substitution only replaces free occurrences of x in M. Any x that is bound by an inner λx is left untouched.

Example: (λx.x (λx.x)) a

The outer x in the body is free with respect to the inner λx
The inner x is bound by its own λx
Result: a (λx.x) — only the free x was replaced

This is why the free/bound distinction exists: it tells substitution which occurrences to replace and which to protect.

Counting Free Occurrences

To count free variable occurrences, examine each variable in the term individually. For each one, check whether an enclosing λ with the same name exists. If not, that occurrence is free.

Remember: count occurrences, not distinct names.

In x y x:

Three variable occurrences, all free (no λ anywhere)
Free occurrences: 3

In λx.x y:

x is bound (enclosed by λx), y is free
Free occurrences: 1

No Matching Binder Means Free

A common mistake: seeing a λ in the expression and assuming all variables must be bound. But a λ only binds variables with the same name. Other variables are unaffected.

In λx.y:

y is free — the only λ here is λx, which binds x, not y

In λx.λy.z:

z is free — neither λx nor λy binds z

The presence of lambdas in a term does not make all variables bound. Each variable needs its own λ to be bound.

The Binder Must Enclose

Each composing stick has a boundary. Tagged blanks inside the stick are under its control. But a tag sitting on the bench next to the stick — even if it has the same letter — is not part of that stick. The stick only controls what is physically inside it.

A λx only binds occurrences of x that are inside its body — the part after the dot. An x that appears outside the scope of that λ is not bound by it, even if the names match.

In (λx.x) x:

The x inside λx.x is bound (it is in the body)
The x after the closing parenthesis is free (it is outside)

In x (λx.x):

The first x is free (the λx has not started yet)
The second x is bound (inside the λx body)

Position matters. The λ must wrap around the occurrence.

Terms with No Lambdas

A term with no λ at all has no binders. Since every variable needs an enclosing λ with its name to be bound, and there are none, every variable in such a term is free.

x y z — three variable occurrences, all free.

f x — two variable occurrences, both free.

These are valid lambda terms. Applications and variables are two of the three term forms — no λ is required. The variables simply refer to things defined elsewhere.

Listing Free Variables

The free variables of a term are the set of variable names that have at least one free occurrence. We write FV(M) for this set.

Examples:

FV(x y) = {x, y} — no lambdas, both are free
FV(λx.x y) = {y} — x is bound, y is free
FV(λx.λy.x y) = {} — both variables are bound
FV(λx.y z) = {y, z} — only x has a binder

A term with no free variables is called closed (or a combinator).

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 Free and Bound Variables →