何时重命名lambda演算中的变量?

内容来源于 Stack Overflow,并遵循CC BY-SA 3.0许可协议进行翻译与使用

  • 回答 (1)
  • 关注 (0)
  • 查看 (7)

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

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

显然减少到

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

但不应x在任何改名(λf.λx.f(fx))(λf.λx.f(fx))?他们不是指不同的xs?

提问于
用户回答回答于

避免捕获是为了避免捕获自由变量。“捕获”绑定变量不会对此造成太大影响:In

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

两种用途x确实是不同的变量,但这已经在术语中编码:通常,子项中的新抽象将“覆盖”进一步最外层​​抽象的绑定。这仅仅是由于lambda术语的评估工作方式:如果对同一个变量有一个新的抽象,那么旧的抽象进一步将最终在新的抽象中的子项中失去效果,并且变量受到内部抽象实际上是不同于仅由外部抽象约束的变量。

你可以尝试这样做:如果你适用λx.(λf.λx.fx)((λf.λx.fx)x)于某个术语N,那么根据beta减少的定义,这个术语将减少到(λf.λx.fx)((λf.λx.fx)x)[N/x],即通过替换xin (λf.λx.fx)((λf.λx.fx)x)的每个自由(!)出现而获得的术语N(替换仅对自由变量进行操作)根据定义)。该x术语中唯一的自由发生是最后一次; 两个子项x中的另外两个es (λf.λx.fx)由各自λx的子句约束。所以唯一x被替换的N是最后一个,因此(λx.(λf.λx.fx)((λf.λx.fx)x))N将减少到(λf.λx.fx)((λf.λx.fx)N)- 子项x中的界限(λf.λx.fx)保持不变。

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

话虽如此,为了更容易阅读,进行这样的重命名有时会很有用。得到的术语与通过直接替换而不重命名获得的术语是α一致的。

扫码关注云+社区

领取腾讯云代金券