Как использовать контекст именования, чтобы найти индексы де Брейна свободных переменных?

Question

В разделе «Типы и языки программирования» в разделе 6.1.2 говорится о контексте именования , используемом для нумерации свободных переменных в лямбда-выражениях. Используя предоставленную ими примерную схему, оба значения λx.xb и λx.xx будут иметь представление де Брюина как λ.00, когда они явно различаются. Как это работает?

Answer 1

Как вы упомянули, в книге используется контекст именования, который отображает n свободные переменные в числа от 0 до n-1.Однако, если вы внимательно посмотрите на примеры в книге, вы заметите, что эти числа не используются непосредственно для представления переменных.Например, он представляет λw. y w как λ. 4 0, хотя отображение для y равно 3, а не 4.

Здесь происходит то, что он добавляет глубину вложения переменной к числу.Т.е. если свободная переменная v вложена в d лямбда-выражения, она получает индекс Γ(v)+d, а не просто Γ(v).

Так что в вашем примере использование контекста Γ {b -> 0} λx.xbбыть представленным как λ. 0 1, а не λ. 0 0.Таким образом, нет никакой двусмысленности.