Shadowing

Inner bindings hide outer. Careful with equipment-free constraints.

7 topics • ~770 words

A composing stick tagged x contains a nested stick also tagged x. Inside the nested stick, every blank marked x belongs to the inner stick -- the outer stick's x blanks are hidden there. The inner tag takes priority. The outer stick's x still works outside the nested stick, but within it, the inner stick is in control.

You already know that the scope of λx is its body. But what happens when two lambdas use the same parameter name, one inside the other? This is shadowing -- a precise, well-defined rule that tells you which binder wins.

What Is Shadowing?

Shadowing occurs when an inner λ uses the same parameter name as an outer λ. The inner binding hides the outer one within its scope.

In λx.λx.x, there are two lambdas both named x. The body x is bound by the inner λx, not the outer one. The outer λx's parameter is shadowed -- it has no visible effect on the innermost x.

The rule is simple: the nearest enclosing λ with the same name wins.

The Inner Binder Wins

When multiple lambdas share the same parameter name, the innermost one binds any occurrence in its body. This is the shadowing rule: nearest enclosing binder wins.

In λx.(λx.x):

  • The inner λx binds the body x
  • The outer λx is shadowed -- it cannot reach x through the inner λx

Think of it like nested instructions: "fill x with A" wrapping "fill x with B." Inside the inner instruction, B wins.

The Shadowed Parameter Is Invisible

When a nested composing stick has its own blank tagged x, the outer stick's x blanks are completely hidden within the inner stick. If someone fills the outer stick's x tag, the inner stick's x blanks are untouched. The inner stick does not even know the outer x exists.

When shadowing occurs, the outer parameter is completely invisible inside the inner lambda's scope. It has no effect there.

In λx.λx.x:

  • The body x is bound by the inner λx
  • The outer λx's parameter cannot affect anything inside the inner λx's body
  • It is as if the outer x does not exist within that region

This means if the outer lambda receives an argument, that argument does not reach the inner x.

Which Binder?

When multiple lambdas share a parameter name, identifying the correct binder requires finding the nearest enclosing λ with that name.

In λx.λy.λx.x:

  • There are two λx lambdas: one outermost, one innermost
  • The body x is enclosed by both, but the inner λx is closer
  • So the inner λx (the third lambda) binds x
  • The middle λy is irrelevant -- it binds y, not x

The rule is always the same: find the closest enclosing λ with the matching name.

Shadowing Is Not an Error

Shadowing might look like a problem -- two lambdas claiming the same name sounds like a conflict. But in lambda calculus, shadowing is perfectly legal and completely unambiguous.

The rule -- nearest enclosing binder wins -- always gives a single, clear answer about which λ binds each occurrence. There is never a case where the answer is "it depends" or "it could be either."

λx.λx.x is a valid term. The inner λx binds x. No ambiguity, no error, no special handling needed.

Unshadowed Occurrences

The outer composing stick tagged x has two blanks. One blank sits before the nested stick; the other is inside it. The nested stick also has tag x. The blank before the nested stick belongs to the outer stick -- it is not shadowed. The blank inside the nested stick belongs to the inner one. Same tag, different owners.

Shadowing only affects occurrences inside the inner lambda's body. Occurrences of the same variable outside the inner lambda are still bound by the outer one.

In λx.(x (λx.x)):

  • The first x in the body (before (λx.x)) is bound by the outer λx -- it is not inside the inner lambda's scope
  • The x inside (λx.x) is bound by the inner λx

Each occurrence is bound by its own nearest enclosing λx.

Different Names, No Shadowing

Shadowing requires two lambdas with the same parameter name, one nested inside the other. If the names are different, there is no shadowing -- each lambda independently binds its own parameter.

In λx.λy.x:

  • λx binds x in the body
  • λy binds y (though y does not appear in the body)
  • No shadowing -- x and y are different names
  • The x in the body is bound by the outer λx, clearly and without interference from λy

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 Shadowing →