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

Question

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

Answer 1

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

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

因此，在您的示例中，使用上下文Γ {b -> 0} λx.xb将表示为λ. 0 1，而不是λ. 0 0。这样就没有歧义了。