在阅读 Wiki 中的 Lambda Calculus 时，遇到了Capture-avoiding substitutions一词。有人可以解释它的含义，因为我在任何地方都找不到定义。
谢谢
附言
我想知道的是告诉操作Capture-avoiding substitutions的原因。如果有人能做到这一点，那将是一个很大的帮助
问问题
8969 次
3 回答
62
通常，我们在 lambda 演算中选择的特定变量名是没有意义的 - 的函数与or或x的函数是一样的。换句话说：abc
(λx.( λy.yx )) 等价于 (λa.(λb.ba)) - 重命名x为a和y不改变任何东西b。
由此，您可能会得出结论，允许任何替换 - 即任何 lambda 项中的任何变量都可以被任何其他变量替换。事实并非如此。考虑上面第一个表达式中的内部 lambda：
(λy.yx)
在这个表达式中，x是“免费的”——它不受 lambda 抽象的“约束”。如果我们用 替换y，x表达式将变为：
(λx.xx)
这有着完全不同的含义。两者x现在都指向 lambda 抽象的参数。最后一个x（最初是“免费的”）已被“捕获”；它被 lambda 抽象“绑定”。
避免意外捕获自由变量的替换被称为“避免捕获替换”。
现在，如果我们在 lambda 演算中关心的只是用一个变量替换另一个变量，那么生活会很无聊。更现实地说，我们想要做的是用lambda term替换变量。因此，我们可以用lambda 抽象(λx.t) 或应用程序(xt) 替换变量。在任何一种情况下，都适用相同的考虑 - 当我们进行替换时，我们希望确保不会通过意外“捕获”一个最初是自由的变量来改变原始表达式的含义。
于 2012-07-04T16:24:00.890 回答
8
如果将变量放置在绑定变量的 lambda（或其他绑定构造，如果它们存在）下，则该变量被捕获。它被称为避免捕获替换，因为该过程避免意外地允许替换中的自由变量被捕获到原始表达式中。
于 2012-06-28T20:28:22.230 回答
5
用 E' 代替 E 中的 x（写成 [E'/x]E ）
- 步骤 1. 重命名 E 和 E' 中的绑定变量，使它们是唯一的
- 步骤 2. 对 E 中的 x 执行 E' 的文本替换
称为避免捕获替换。
示例： [y (λx. x) / x] λy。(λx.x) yx
重命名后：[y (λv. v)/x] λz。(λu.u) zx
代入后：λz。(λu. u) z (y (λv. v))
于 2012-06-28T06:45:39.177 回答