lambda-calculus - 如何使用命名上下文来查找自由变量的 de Bruijn 索引？

Question

在“类型和编程语言”的 6.1.2 节中，他们讨论了用于为 lambda 表达式中的自由变量编号的命名上下文。使用他们提供的示例方案，λx.xb和 λx.xx将他们的 de Bruijn 表示为 λ.00当它们显然是不同的术语时。这是如何工作的？

Answer 1

正如你提到的，这本书使用了一个映射 n 的命名上下文。来自 0 的数字的自由变量至 n-1 .但是，如果您仔细查看本书中的示例，您会注意到它并没有直接使用这些数字来表示变量。例如它代表λw. y w如 λ. 4 0即使 y 的映射是 3，不是 4。

这里发生的事情是他将变量的嵌套深度添加到数字中。即如果一个自由变量 v嵌套在 d lambdas，它得到索引 Γ(v)+d ，不仅仅是 Γ(v) .

所以在你的例子中使用上下文 Γ {b -> 0} λx.xb将表示为 λ. 0 1 ，不是 λ. 0 0 .因此没有歧义。