types - 纯 lambda 表达式（let-free 表达式）是否需要重命名？

Question

纯 lambda 表达式是否需要重命名？在 ML 中，输入程序表达式必须具有每个绑定变量都是不同的属性。我想知道纯 lambda 表达式（let-free 表达式）是否相同？

Answer 1

当您有活页夹时，唯一重要的是变量出现与其活页夹之间的关系。使用名称只是表达这种关系的一种方便方式（但您可以使用其他技术，例如指针、显式连接——如在交互网络中——、De Bruijn 索引等）。

如果您使用名称，当两个嵌套的活页夹使用相同的名称时，可能会发生冲突。在这种情况下，您需要一些策略来区分它们，并且所有编程语言中的典型解决方案是变量与最里面的同名绑定器相关联，其范围涵盖变量。

在实践中，变量重命名仅在（手动）减少术语期间相关，因为您需要避免变量捕获现象。例如考虑这个术语

                          (\x.\y.x y) y

其中最外面的 y 是自由的。通过 beta 归约，这是 (\yx y)[y/x]，如果我们天真地执行替换，我们得到项 (\yy y)。这是错误的，因为参数变量 y 在进入其作用域时已被同名的绑定程序秘密捕获。

在这种情况下，我们需要在执行归约之前重命名变量，例如。

                          (\x.\z.x z) y

那，在归约之后，给了我们新的和正确的结果 \zy z。

当然，在类型化设置中，由不同标识符绑定的变量具有不同的类型，因此重命名它们以避免混淆可能是一个好习惯。