skip to content

Reducing (λx. λy. x) y, why does naive substitution produce the identity function instead of the correct term?

level: middleimportance: should knowfreq 34%

answer

  1. names are not all equal
  2. which binder owns this occurrence
  3. the argument brought a free name with it
  4. rename the binder, not the free name
  5. choose a name occurring nowhere in either term

basics

~20 s

The argument is the free variable y, and substituting it blindly drops it under an inner binder that already uses that name, so it is captured. Renaming the bound name first gives λz. y, a constant function.

solid answer

~50 s

Inside `λx. λy. x`, the `x` in the body is bound by the outer binder, and the inner `λy` binds nothing that actually occurs. The argument is the **free** variable `y`. Substituting it for `x` without care places it directly under `λy`, where it stops meaning the caller's `y` and starts meaning the inner parameter — the term collapses to `λy. y`, the identity. Substitution is only defined when no free variable of the argument gets captured, so you first apply **alpha conversion**: rename the inner binder to something fresh, turning the term into `λx. λz. x`, and then reduce, giving `λz. y` — a function that ignores its argument and returns the outer `y`. Bound names are arbitrary labels and may be renamed; free names are not, because they refer to something outside the term.

code

pseudocode · 9 lines
pseudocode
term:     (λx. λy. x) y        -- the argument is the FREE variable y

naive:    substitute y for x inside (λy. x)
          ==> λy. y            -- wrong: the argument fell under λy

correct:  alpha-rename the inner binder first
          (λx. λy. x)  =  (λx. λz. x)
          substitute y for x inside (λz. x)
          ==> λz. y            -- ignores its argument, returns the free y

go deeper

for a junior

Recall the difference between a free and a bound occurrence, and that a bound name is owned by the nearest enclosing binder that declares it. Be able to point at each occurrence in a three-symbol term and say which it is.

for a middle

Explain capture with a worked term: show the argument's free name landing under a binder that reuses it, and show the rename that prevents it. Say why the binder is the thing you are allowed to move.

for a senior

Demonstrate the production version: inlining a call whose argument mentions a name the body declares locally. Say what the resulting code does, why nothing flags it, and what a rewriting tool must do before substituting.

for a principal

The judgment call is where a team spends its guarantee — on a naming discipline people follow, or on tooling that generates names nobody can collide with. The second costs readability and buys correctness that does not depend on attention.

## Which binder owns an occurrence An occurrence of a variable in a term is **bound** if some enclosing abstraction declares that name, and **free** otherwise. The distinction is positional, not lexical: the same name can be free in one part of a term and bound in another, and a name that is bound is owned by the *nearest* enclosing binder of that name. - In `λx. x`, the `x` in the body is bound. - In `λx. y`, the `y` is free — the term says nothing about what `y` is, and its meaning depends on whatever surrounds the term. - In `λx. λx. x`, the body's `x` is bound by the **inner** binder; the outer one binds nothing. The practical consequence is that bound names are private labels with no meaning outside the abstraction that declares them, while free names are references to the outside world. That asymmetry decides everything below. ## The capture, worked Take `(λx. λy. x) y`. The function is the constant-function term; the argument is the bare variable `y`, free. | | What happens | Resulting term | Meaning | |---|---|---|---| | Naive | Put `y` wherever `x` occurs in `λy. x` | `λy. y` | a function returning its own argument | | Correct | Rename the inner binder, then substitute | `λz. y` | a function ignoring its argument, returning the outer `y` | The two results are not variations on a theme; they are different functions. Naively, the argument travelled into a region where the name `y` was already spoken for, and on arrival it was silently reinterpreted as the inner parameter. That is **variable capture**. The rule that forbids it is not a convention or a style preference: substitution `B[x := A]` is *defined* only when no free variable of `A` becomes bound in `B`. ## Alpha conversion: what may be renamed **Alpha conversion** renames a bound variable together with every occurrence that its binder binds. `λy. x` and `λz. x` are the same function written two ways; the calculus treats alpha-equivalent terms as one term, and no reduction can tell them apart. What may *not* be renamed is a free variable. Changing `y` to `w` in the argument would change which outside thing the term refers to — it would be answering a different question. The asymmetry is the whole technique: the collision is resolved by moving the name that has no meaning of its own, never the one that does. ## A procedure that always works 1. Identify the redex `(λx. B) A` you are about to fire. 2. Collect the **free** variables of the argument `A`. 3. Walk the body `B` and look at every binder you would have to pass through to reach a free occurrence of `x`. If any of those binders names a variable from step 2, you have a collision. 4. Rename that binder — and every occurrence it binds — to a name that occurs nowhere in either term: not free in `A`, and neither free nor bound in `B`. 5. Now substitute. The step is defined, and repeat for any nested redex. Implementations avoid doing this repeatedly by choosing a representation in which a variable is written as the distance out to its own binder rather than as a name. With no names, there is nothing to clash, and the whole hazard disappears — at the cost of terms that are much harder for a person to read. ## The same hazard outside the calculus Anywhere one piece of syntax is substituted into another, capture is waiting. Inlining a call by hand during review is the everyday case: you paste the argument expression into the body, and if the argument mentions a name that the body already declares locally, the pasted expression now reads the local one. The result compiles, runs, and is wrong — which is precisely the failure mode the naive reduction above demonstrates in four symbols. Tools that generate or rewrite code face the same obligation and solve it the same way: they invent names that cannot collide before they substitute. This is also why "what does this lambda capture" is a different question from "what does this substitution capture". Capturing an enclosing variable deliberately is what makes a function value useful. Capture in the sense above is an accident of naming that changes a term's meaning, and the fix is always to rename the binder that got in the way.

  • Two terms differ only in the names of their bound variables. Are they the same term?
    Yes — they are alpha-equivalent, and the calculus treats them as one term. Renaming a binder together with every occurrence it binds changes nothing observable, and that freedom is exactly what you spend to avoid capture. Renaming a free variable is a different act entirely: a free name refers to something outside the term, so changing it changes what the term means.
  • How would you choose the fresh name mechanically rather than by eye?
    Pick a name that occurs nowhere in either term: not free in the argument, and neither free nor bound in the body. A generator that keeps a counter and never reuses a number is enough. The alternative is to drop names altogether and write each variable as the distance out to its binder, which removes the question because there is nothing left to clash.

It is the hazard of forwarding a letter into a house where someone already answers to the name on the envelope: the letter arrives and the wrong person opens it. The fix is for the house to rename its own occupant, never to rewrite the address the sender wrote.

saying these in an interview costs you the question

  • Thinks any variable can be renamed, free ones included
  • Treats substitution as textual replacement with no regard for binders
  • Says a name collision is harmless because bound names are arbitrary
  • Renames the free variable in the argument to dodge the clash
  • Believes capture only happens under dynamically scoped name lookup
  • Cannot say which of λy. y and λz. y is the correct result