Lambda微积分自由变量

Question

以下是Slonneger的“编程语言的语法和语义”中的一些内容：

变量可能在同一个lambda表达式中同时出现绑定和空闲:例如，在λx.yλy.yx中，y的第一次出现是空闲的，而其他两个则是绑定的。

我假设自由变量是在λx之后的y，而界y是λy.y，我可以直观地理解它。所以((λx.yλy.yx)a)(B)会降低到(yλy.ya)b，然后降到bba？有人能解释一下这是怎么回事吗？最后，它是表达b两次。也许有人能提供更多的约束变量和自由变量的例子吗？

Answer 1

您正确地将第一个y标识为空闲变量。基本上，lambda抽象为它们的绑定变量定义了一个范围。该作用域覆盖相同变量名的任何其他用途，因此相同的变量名可以在不同的抽象中多次使用或作为空闲变量使用。

(y(λy.ya))b不能进一步降低。在beta约简中，无界变量永远不会被替代。

如果它是(y(λy.ya)b)，你可以将其还原为y(ba)。