Quel est le nom de la notation lambda qui utilise des offsets entiers pour faire référence à des arguments simples implicites?

Question

ressemble un peu comme celui-ci (l'exemple montre les chiffres de l'église et le Y-Combinator):

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)) 

Quel est le nom de ce type de notation? J'ai l'air d'avoir oublié.

Answer 1

Il est le De Bruijn index du lambda calculus