Return to Question

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.

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.

On page 77 of Types and Programming Languages, 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.

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.

On page 77 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.

On page 77 of Types and Programming Languages, 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.