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

Question

在"类型和编程语言"的6.1.2节中,他们讨论了用于对lambda表达式中的自由变量进行编号的命名上下文.使用示例方案,他们已经提供了,都?x.xb和?x.xx都会有自己的德布鲁因表示形式?.00时,他们明显不同的术语.这是如何运作的？

Answer 1

至于你提到书中使用它映射命名上下文n自由变量的数量从0到n-1.但是,如果仔细观察本书中的示例,您会注意到它不直接使用这些数字来表示变量.例如?w. y w,?. 4 0即使映射为y3而不是4,它也表示为.

这里发生的是他将变量的嵌套深度添加到数字中.即如果一个自由变量v嵌套在dlambda中,它就会获得索引?(v)+d,而不仅仅是?(v).

因此,在您的示例中,使用上下文? {b -> 0} ?x.xb将表示为?. 0 1,而不是?. 0 0.因此没有歧义.