“避免捕获的替换"是什么意思? [英] What is meant by "Capture-avoiding substitutions"?

问题描述

在阅读 Wiki 中的 Lambda 演算时，遇到了术语避免捕获的替换.有人可以解释一下这是什么意思，因为我在任何地方都找不到定义.

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.

谢谢

附注

我想知道的是告诉该操作避免捕获替换的原因.如果有人能做到，那将是一个很大的帮助

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

推荐答案

通常，我们在 lambda 演算中选择的特定变量名称是没有意义的 - x 的函数与a 或 b 或 c 的函数.换句话说:

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)) 等价于 (λa.(λb.ba)) - 将 x 重命名为 a 和 y 到 b 不会改变任何东西.

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

由此，您可能会得出结论，允许任何替换 - 即任何 lambda 项中的任何变量都可以被任何其他变量替换.事实并非如此.考虑上面第一个表达式中的内部 lambda:

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)

在这个表达式中，x 是自由的"——它不受 lambda 抽象的约束".如果我们将 y 替换为 x，则表达式将变为:

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)

这有完全不同的含义.两个 x 现在都引用 lambda 抽象的参数.最后一个 x(最初是免费的")已被捕获"；它受 lambda 抽象的约束".

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."

现在，如果我们在 lambda 演算中只关心用一个变量替换另一个变量，那么生活将非常无聊.更现实地说，我们想要做的是用 lambda 项 替换变量.因此，我们可能会用 lambda 抽象 (λx.t) 或 应用程序 (x t) 替换变量.在任何一种情况下，同样的考虑都适用——当我们进行替换时，我们希望确保不会通过意外捕获"一个最初空闲的变量来改变原始表达式的含义.

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.

这篇关于“避免捕获的替换"是什么意思?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！