41

While reading the Lambda Calculus in Wiki, came across the term Capture-avoiding substitutions. Can someone please explain what it means as I couldn't find a definition from anywhere.

Thanks

PS

What I want to know is the reason for telling that operation Capture-avoiding substitutions. It would be a great help if anyone can do that

Asumu Takikawa
  • 8,447
  • 1
  • 28
  • 43
Pradeep
  • 647
  • 1
  • 7
  • 17

3 Answers3

68

Normally, the specific variable names that we chose in the lambda calculus are meaningless - a function of x is the same thing as a function of a or b or c. In other words:

(λx.(λy.yx)) is equivalent to (λa.(λb.ba)) - renaming x to a and y to b does not change anything.

From this, you might conclude that any substitution is allowed - i.e. any variable in any lambda term can be replaced by any other. This is not so. Consider the inner lambda in the first expression above:

(λy.yx)

In this expression, x is "free" - it is not "bound" by a lambda abstraction. If we were to replace y with x, the expression would become:

(λx.xx)

This has an altogether different meaning. Both x's now refer to the argument to the lambda abstraction. That last x (which was originally "free") has been "captured"; it is "bound" by the lambda abstraction.

Substitutions which avoid accidentally capturing free variables are called, unimaginatively, "capture-avoiding substitutions."

Now, if all we cared about in lambda calculus was substituting one variable for another, life would be pretty boring. More realistically, what we want to be doing is replacing a variable with a lambda term. So we might replace a variable with a lambda abstraction (λx.t) or an application (x t). In either case, the same considerations apply - when we do the substitution, we want to ensure that we don't change the meaning of the original expression by accidentally "capturing" a variable which was originally free.

Ord
  • 5,693
  • 5
  • 28
  • 42
  • 4
    Thank you so much! The relevance of the word "capture" was not explained in the materials I was reading, which left me at a loss for what the intention was. – Paul Jul 31 '17 at 16:49
  • @Ord, is x is bound in (λx.(λy.yx))? Because the outer expression has x as an argument. Or it's bound in relation to (λx.(λy.yx)) and free in relation to (λy.yx)? – Bulat M. Nov 17 '17 at 17:34
  • 2
    x would be bound in the expression (λx.(λy.yx)) and free in the expression (λy.yx). – Ord Nov 19 '17 at 00:48
9

A variable is captured if it is placed under a lambda (or other binding constructs if they exist) that binds the variable. It's called capture-avoiding substitution because the process avoids accidentally allowing free variables in the substitution to be captured inside the original expression.

Asumu Takikawa
  • 8,447
  • 1
  • 28
  • 43
5

The substitution of E’ for x in E (written [E’/x]E )

  • Step 1. Rename bound variables in E and E’ so they are unique
  • Step 2. Perform the textual substitution of E’ for x in E
    is called capture-avoiding substitution.

Example: [y (λx. x) / x] λy. (λx. x) y x

After renaming: [y (λv. v)/x] λz. (λu. u) z x
After substitution: λz. (λu. u) z (y (λv. v))

Jainendra
  • 24,713
  • 30
  • 122
  • 169
  • What I really want to know is why it's called capture-avoiding substitution. I mean conceptually. – Pradeep Jun 28 '12 at 07:07
  • @Jaguar, is x is bound in (λx.(λy.yx))? Because the outer expression has x as an argument. Or it's bound in relation to (λx.(λy.yx)) and free in relation to (λy.yx)? – Bulat M. Nov 17 '17 at 17:37