什么是“避免捕获替代”？

Question

什么是“避免捕获替代”？

programming-languageslambda-calculus

41

在维基百科阅读λ演算时，看到了术语避免变量捕获的替换。有人能解释一下它是什么意思吗？我无法在任何地方找到定义。

谢谢

PS

我想知道称之为避免变量捕获的替换操作的原因。如果有人能解释一下，那将是极大的帮助。

- Pradeep

3个回答

11

如果将一个变量放在lambda函数（或其他绑定构造函数）下，使其与该变量绑定，则该变量被称为“捕获”变量。这个过程称为“避免捕获替换”，因为该过程避免了在替换中意外地允许自由变量被捕获到原始表达式内部。

- Asumu Takikawa

5

将E中的x替换为E'（写作[E'/x]E）

步骤1. 重命名E和E'中的绑定变量，使它们唯一
步骤2. 对E进行文本替换，用E'替换x，这被称为“避免捕获的替换”。

示例：[y (λx. x) / x] λy. (λx. x) y x

重命名后：[y (λv. v)/x] λz. (λu. u) z x
替换后：λz. (λu. u) z (y (λv. v))

- Jainendra

我真正想知道的是为什么它被称为避免捕获替换。我的意思是从概念上讲。 - Pradeep

@Jaguar，x是否被绑定在(λx.(λy.yx))中？因为外部表达式有x作为参数。或者它是相对于(λx.(λy.yx))被绑定而相对于(λy.yx)自由的？ - anon

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Ord · Accepted Answer

通常情况下，我们在λ演算中选择的特定变量名称是没有意义的 - 对于x的函数与a或b或c的函数相同。换句话说：(λx.(λy.yx))等同于(λa.(λb.ba)) - 将x更名为a，将y更名为b不会改变任何东西。

由此，您可能会得出结论，允许任何替换 - 即任何lambda术语中的任何变量都可以被替换为任何其他变量。但并非如此。考虑上述第一个表达式中的内部lambda：

(λy.yx)

在这个表达式中，x是“自由”的 - 它没有被lambda抽象“绑定”。如果我们用x替换y，该表达式将变为：

(λx.xx)

这具有完全不同的含义。两个x现在都指向lambda抽象的参数。最后一个x（最初是“自由”的）已被“捕获”；它被lambda抽象“绑定”。

避免意外捕获自由变量的替换称为“避免捕获替换”。

现在，如果我们在λ演算中所关心的只是将一个变量替换为另一个变量，那么生活将会相当无聊。更现实地说，我们想要做的是用lambda术语替换变量。因此，我们可能会用lambda抽象（λx.t）或应用（x t）替换变量。在任何情况下，都适用相同的考虑 - 当我们进行替换时，我们希望通过意外“捕获”原始自由变量来确保不改变原始表达式的含义。