Каково имя лямбда-нотации, которое использует целочисленные смещения для ссылки на неявные одиночные аргументы?

Question

Выглядит вроде как это (пример показывает Чёрча и Y-комбинатор):

zero := λ.λ.0 
one := λ.0    -- or more verbosely: λ.λ.1 0 
two := λ.λ.1 (1 0) 
three:= λ.λ.1 (1 (1 0)) 

add := λ.λ.λ.λ.3 1 (2 1 0) 

Y := λ.(λ.1 (0 0)) (λ.1 (0 0)) 

Что такое название этого типа обозначений? Кажется, я забыл.

Answer 1

Это De Bruijn index из lambda calculus