1
$\begingroup$

On page 77 (section 6.1) of Types and Programming Languages by Benjamin C. Pierce (1st and only edition thus far), there is the following quote regarding naming contexts and de Bruijn indices:

Γ = x ↦ 4, y ↦ 3, z ↦ 2, a ↦ 1, b ↦ 0

Then x (y z) would be represented as 4 (3 2), while λw. y w would be represented as λ. 4 0 and λw.λa.x as λ.λ.6.

In the second example how do we distinguish between the free variables 0 and the bound variable zero if there were a free variable b in the same term? For instance, it seems like λw. b w would have the name less term λ. 0 0, but this appears ambiguous to me. Maybe I missed something or haven't read far enough ahead.

Update

Another point of confusion I had was my misunderstanding that the context Γ was global, but in 6.2 it is stated:

... the context in which the substitution is taking place becomes one variable longer than the original; we need to increment the indices of the free variables [in the substituted term] so that they keep referring to the same names in the new context as they did before.

So, it appears Γ is local to each abstraction.

Improve this question
$\endgroup$
0

2 Answers 2

Reset to default
1
$\begingroup$

The best way to view this, in my opinion, is by looking at the abstract syntax tree. For λw. b w, this would be something like:

 λw | @ / \ b w

Here, we're going to assign w the de Bruijn index 0, because you do not pass any binders in order to get to its definition. However, for b we will assign it de Bruijn index 1, since you pass one binder, and it then has index 0 in the context. In general, you add 1 to the index in the context for every binder you pass along the way to reach a use of a variable to compute its de Bruijn index at that point. Thus, λw. b w would be represented as λ. 1 0.

Improve this answer
$\endgroup$
1
  • $\begingroup$ Thanks for the explanation - I see this was also the approach taken in a subsequent example with the same context: λw.λa.x as λ.λ.6. $\endgroup$ Commented Feb 16, 2024 at 13:40
0
$\begingroup$

Working on exercise 6.1.5 part 1 provided some clarity on the issue (at least I believe so). However, the solution provided in the appendix doesn't seem to get into the weeds (implementation details) enough to address this question.

It seems that we can get around this by starting the de Bruijn indices for bound variables after those for free variables; since we are given the context Γ as part of the function, we know all the free variables. Instead of starting an innermost λ-abstraction's de Bruijn index at 0, it would start at max(range(Γ)) + 1, ensuring no conflict.

Update The wording in 6.1.5 part 2 seems to confirm this approach: “choose the first variable name that is not already in dom(Γ)”.

Improve this answer
$\endgroup$

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.