lambda-calculus - 何时重命名 lambda 演算中的变量？

Question

我理解为什么重命名变量以避免捕获很重要，但是在下面的示例中，我不明白为什么它不会发生。

(λf.λx.f(fx))(λf.λx.fx)

显然减少到

λx.(λf.λx.fx)((λf.λx.fx)x)

但不应该在其中一个或x中重命名？他们不是指不同的s吗？(λf.λx.f(fx))(λf.λx.f(fx))x

标签： lambda-calculus

Answer 1

捕获避免是为了避免捕获自由变量。“捕获”绑定变量并没有那么大的伤害：在

λx.(λf.λx.fx)((λf.λx.fx)x)

的两种用法x确实是不同的变量，但这已经在术语中进行了编码：通常，子术语中的新抽象将“覆盖”更远的抽象的绑定。这仅仅是由于 lambda 项的求值方式：如果对同一个变量有一个新的抽象，那么旧的抽象最终将在具有新抽象的子项中失去作用，并且由内部抽象实际上将是与仅受外部抽象约束的变量不同的变量。

你可以试试这个：如果你应用λx.(λf.λx.fx)((λf.λx.fx)x)到某个term ，那么根据betaN归约的定义，这个term会(λf.λx.fx)((λf.λx.fx)x)[N/x]归约为根据定义）。该术语中唯一自由出现的是最后一个；两个子项中的其他两个es 受其各自的约束。因此，唯一将被替换的是最后一个，因此将减少到- 子项中的' 界限保持不变。 x(λf.λx.fx)((λf.λx.fx)x)Nxx(λf.λx.fx)λxxN(λx.(λf.λx.fx)((λf.λx.fx)x))N(λf.λx.fx)((λf.λx.fx)N)x(λf.λx.fx)

所以x被内部抽象约束的 ' 和x术语末尾的 the 确实是属于不同抽象的不同变量。因此，在应用程序期间不重命名它们是没有问题的。

话虽如此，有时为了更易读而进行此类重命名会很有用。结果项将与通过直接替换而不重命名获得的项是 alpha 一致的。