Alpha Equivalence

Renaming bound variables preserves meaning. Lambda x.x = lambda y.y.

10 topics • ~1028 words

A composing stick has blanks tagged x. You relabel every tag to w and relabel the binder to match. The printed output is identical -- the tag is internal bookkeeping, not part of the final print. The reader never sees which letter you used on the blanks.

Lambda calculus has infinitely many ways to write the same function. λx.x, λy.y, λz.z -- all describe the identity. We need a formal way to say "these are the same term." That is alpha equivalence.

What Is Alpha Equivalence?

Two lambda terms are alpha-equivalent (written =α) if one can be obtained from the other by consistently renaming bound variables.

λx.x =α λy.y =α λz.z

All three are the identity function. The name of the bound variable does not affect what the term does -- only the binding structure matters. Think of the variable name as a label connecting a λ to the positions it controls.

Renaming Bound Variables

An $\alpha$-rename changes a bound variable name. To rename x to z in λx.x:

  1. Change the binder: λx becomes λz
  2. Change every occurrence that λx binds: x becomes z
  3. Result: λz.z

Both the binder and its bound occurrences must change together. Changing only one would break the connection between the λ and the positions it controls.

Are These Alpha-Equivalent?

Two terms are alpha-equivalent when they have the same binding structure -- the same pattern of which λ controls which positions. The variable names are interchangeable labels.

λx.x =α λy.y -- same structure (binder controls one position)

λx.x y ≠α λx.x z -- different free variables (y vs z)

Only bound variable names can differ between alpha-equivalent terms. Free variables must match exactly.

Free Variables Cannot Be Renamed

If a composing stick references a tag from outside -- a tag with no matching blank in this stick -- that tag names a specific type piece from elsewhere. Changing that name would request a different piece entirely. Only internal tags (bound variables) are the compositor's to relabel.

$\alpha$-renaming applies only to bound variables. Free variables cannot be renamed because they refer to something outside the term.

λx.x y -- x is bound, y is free.

  • Rename x to z: λz.z y -- valid $\alpha$-rename, same term
  • Rename y to z: λx.x z -- not an $\alpha$-rename, different term

Changing a free variable changes what the term depends on. y and z are different external references.

The Capture Trap

Suppose a composing stick has blanks tagged x and the text also references an external tag y. If you relabel the x blanks to y, the stick now treats every y as its own blank -- including the one that was an external reference. The outside reference has been captured by the stick's own binder.

You cannot alpha-rename a bound variable to a name that already appears free in the body. This would capture the free variable.

Consider λx.x y:

  • x is bound, y is free
  • Rename x to z: λz.z y -- safe, y is still free
  • Rename x to y: λy.y y -- wrong! The free y is now bound by λy. The term's meaning has changed.

λx.x y applies its argument to y. But λy.y y applies its argument to itself. These are completely different functions.

Why Alpha Equivalence Matters

$\alpha$-equivalence is practically useful because it lets us choose convenient names for bound variables.

Suppose we want to apply λx.λy.x to y. Naive substitution would give λy.y -- but that captures the free y! Because of $\alpha$-equivalence, we can first rename the inner bound variable: λx.λy.x =α λx.λw.x. Now substitution gives λw.y, which is correct.

Without $\alpha$-equivalence, substitution would be broken. With it, we can always rename to avoid collisions.

Structure, Not Names

Two composing sticks that use different tag letters but have blanks in exactly the same positions, bound by exactly the same binders, will produce identical printed output. The tag letter is invisible to the reader -- what matters is which binder controls which position.

What matters for alpha equivalence is the binding structure -- which λ controls which variable positions.

λx.λy.x and λa.λb.a are alpha-equivalent:

  • Both have an outer binder controlling the body variable
  • Both have an inner binder that binds nothing in the body
  • The names x/a and y/b are different, but the structure is the same

λx.λy.x and λa.λb.b are not alpha-equivalent:

  • In the first, the outer binder controls the body variable
  • In the second, the inner binder controls the body variable
  • Different structure, different meaning

Renaming One Binder at a Time

In a term with multiple λs, each binder is independent. You can $\alpha$-rename one without touching the others.

Consider λx.λy.x y:

  • Rename x to z: λz.λy.z y -- only x and its binder change
  • Rename y to w: λx.λw.x w -- only y and its binder change

Each λ controls its own set of occurrences. Renaming one binder affects only the variables it binds, leaving everything else untouched.

Alpha Equivalence Check

To check alpha equivalence, compare the binding structure: which binder (by position, not name) controls which body variable (by position, not name).

λx.λy.y and λa.λb.b:

  • In both, the inner binder controls the body variable
  • Alpha-equivalent: same structure, different labels

λx.λy.y and λa.λb.a:

  • First: inner binder controls the body variable
  • Second: outer binder controls the body variable
  • Not alpha-equivalent: different structure

Perform an Alpha-Rename

To alpha-rename a bound variable, change the binder and every occurrence it binds to the new name. The result is alpha-equivalent to the original.

Example: rename x to w in λx.x y

  • Change λx to λw
  • Change the bound x to w
  • Result: λw.w y

The free variable y is untouched -- it is not controlled by λx.

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 Alpha Equivalence →