Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

What is meant by "Capture-avoiding substitutions"?

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

like image 448
Pradeep Avatar asked Jun 28 '12 06:06

Pradeep


People also ask

What is lambda calculus explain in detail?

Lambda calculus (also written as λ-calculus) is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution. It is a universal model of computation that can be used to simulate any Turing machine.

What is a redex lambda calculus?

y 1 Page 2 A reducible expression, or redex, is any expression to which the above (beta-reduction) rule can be immediately applied. For example, λx. (λy. y) z is not a redex, but its nested expression (λy.

Who invented lambda calculus?

(The lambda calculus itself was invented in 1936 by the Princeton University logician Alonzo Church while he was investigating…


2 Answers

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.

like image 113
Ord Avatar answered Oct 29 '22 16:10

Ord


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.

like image 44
Asumu Takikawa Avatar answered Oct 29 '22 16:10

Asumu Takikawa