Pra*_*eep 30 programming-languages lambda-calculus
在Wiki中阅读Lambda微积分时,遇到了捕获避免替换的术语.有人可以解释它的含义,因为我无法从任何地方找到定义.
谢谢
PS
我想知道的是告诉操作Capture避免替换的原因.如果有人能做到这一点,那将是一个很大的帮助
Ord*_*Ord 49
通常,我们在lambda演算中选择的特定变量名称是无意义的 - x函数与aor b或or 的函数相同c.换一种说法:
(λ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术语替换变量.所以我们可以用lambda抽象(λx.t)或应用程序(xt)替换变量.在任何一种情况下,同样的考虑因素都适用 - 当我们进行替换时,我们希望确保我们不会通过意外地"捕获"最初自由的变量来改变原始表达式的含义.
在E中用E'代替x(写成[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))