We distinguish two kinds of variables: Bound variables and
Free ones. The first kind of variables is called De Bruijn
indices: each bound variable is a natural number (starting
from zero) that designates the number of binders between
itself and a corresponding binder. For example, the term \x -
> \y -> x (the “K combinator”) is represented as \_ -> \_ -> 1.
(If we were returning y instead of x, we would write 0
instead.)
The footnote says:
Contrary to a De Bruijn index, a De Bruijn level is a natural
number indicating the number of binders between the
variable’s binder and the term’s root. For example, the term
\x -> \y -> x is represented as \_ -> \_ -> 0, where 0 is the
De Bruijn level of x. The De Bruijn level of y would be 1 if
we used it instead of x.↩
That doesn't look contradictory. An expression is a (syntax) tree, and every variable use has a unique path from the root to that use. This path crosses some sequence of binders, which we can label with integers.
If you assign integers from the inside out, as DB indices do, then the `x` usage in `\x -> \y -> x` passes one binder (`\y`) before landing on the correct one (`\x`), yielding `\_ -> \_ -> 1`.
If you assign integers from the outside in, as DB levels do, then the `x` usage lands on `\x` instantly, yielding `\_ -> \_ -> 0`.
De Bruijn came up with both systems, and it can be confusing to keep track of which one is which; but they are different systems.
I would have said, "that LOOKS contradictory but isnt"
because one is index and the other is a level but notationally they refer to the same syntactic construct, and therefore an assertion of value differs by intent. Index 1, level 0, Same syntax to represent.
To me, it "looks" contradictory. It has to be explained by word not by statement in notation.
If you combine these two naming schemes in the same syntax, of course it will be ambiguous. In the examples of the K combinator, they don't clash with each other though, as those are different examples.
