How to use a naming context to find de Bruijn indices of free variables?

Question

In "Types and Programming Languages", section 6.1.2 they talk about a naming context used to number free variables in lambda expressions. Using the example scheme they've provided, both λx.xb and λx.xx will have their de Bruijn representation as λ.00 when they're clearly different terms. How does this work?

Answer 1

As you mentioned the book uses a naming context which maps n free variables to the numbers from 0 to n-1. However if you look closely at the examples in the book, you'll notice that it doesn't use those numbers directly to represent the variables. For example it represents λw. y w as λ. 4 0 even though the mapping for y is 3, not 4.

What's happening here is that he adds the nesting depth of the variable to the number. I.e. if a free variable v is nested in d lambdas, it gets the index Γ(v)+d, not just Γ(v).

So in your example using the context Γ {b -> 0} λx.xb would be represented as λ. 0 1, not λ. 0 0. Thus there's no ambiguity.