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

【问题标题】：Is renaming necessary for pure lambda expressions (let-free expressions)?纯 lambda 表达式（let-free 表达式）是否需要重命名？
【发布时间】：2016-03-07 00:43:10
【问题描述】：

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

【问题讨论】：

ML 没有该属性：(fn a => fn a => a + 1) "foo" 1.
你能解释更多你的例子吗？
当问题宽泛且未明确说明时，很难解释。
问题是关于类型推断的算法。 Core-ML 是 lambda 演算 + “let”。我想知道如果我们从 ML 中删除“let”，我是否需要在类型推断算法中重命名有界变量？

标签： types lambda ml inference principal

【解决方案1】：

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

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

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

                          (\x.\y.x y) y

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

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

                          (\x.\z.x z) y

在归约后，我们得到新的正确结果 \z.y z。

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

【讨论】：