Search code examples
functionlambdafunctional-programmingtheorylambda-calculus

What is the name of the lambda notation that uses integer offsets to refer to implicit single arguments?


Looks kind of like this (the example shows church numerals and the 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))

What is the name of this type of notation? I seem to have forgotten.


Solution

  • It is the De Bruijn index of the lambda calculus