Confused about beta-reduction/shifting in untyped $\lambda$-calculus with de Bruijn terms

Question

In Types and Programming Languages, the family of sets of terms with de Bruijn indices in the untyped $\lambda$-calculus is defined in this way:

Let $T$ be the smallest family of sets $\{T_0, T_1, T_2, ...\}$ such that

1. $k \in T_n$ whenever 0ドル \le k \lt n$;
2. if $t_1 \in T_n$ and $n \gt 0,ドル then $\lambda. t_1 \in T_{n-1}$;
3. if $t_1 \in T_n$ and $t_2 \in T_n,ドル then $(t_1\ t_2) \in T_n$.

The $\beta$-reduction operation is then defined as $(\lambda. t_{12})\ v_2 \rightarrow\ \uparrow^{-1}([0 \mapsto\ \uparrow^1(v_2)]t_{12}),ドル where $\uparrow^d(t)$ is the function to add $d$ to the indices of all free variables in $t$. By the definition of the $\uparrow$ function, if $t \in T_n,ドル then $\uparrow^d(t) \in T_{n+d}$. Substitution is defined like so:

1. $[j \mapsto s]k = s\ $if $k = j; k$ otherwise
2. $[j \mapsto s](\lambda. t_1) = \lambda. [j+1 \mapsto\ \uparrow^1(s)]t_1$
3. $[j \mapsto s](t_1\ t_2) = ([j \mapsto s]t_1\ [j \mapsto s]t_2)$

I can't seem to get these definitions to work properly in manually reducing the term $((\lambda. 0)\ (\lambda. 0))$ (i.e. the identity function applied to itself). Here are the steps I've gone through in attempting to apply the $\beta$-reduction rule; I'll add a subscript to each term indicating which set in $T$ I think the term is in, so e.g. $(\lambda. 0_1)_0$ is an abstraction of 0ドル \in T_1,ドル and the abstraction itself is in $T_0$. I believe that if done properly, $((\lambda. 0_1)_0\ (\lambda. 0_1)_0)$ should reduce to $(\lambda. 0_1)_0$.

• $(\lambda. 0_1)_0\ (\lambda. 0_1)_0$
• (by def. of $\beta$-reduction) $\rightarrow\ \uparrow^{-1}([0 \mapsto\ \uparrow^1((\lambda. 0_1)_0)] (\lambda. 0_1)_0)$
• (by def. of $\uparrow$) $\rightarrow\ \uparrow^{-1}([0 \mapsto (\lambda. 0_2)_1] (\lambda. 0_1)_0)$
• (by def. 2 of substitution) $\rightarrow\ \uparrow^{-1}(\lambda. [1 \mapsto\ \uparrow^1((\lambda. 0_2)_1)]0_1)$
• (by def. of $\uparrow$) $\rightarrow\ \uparrow^{-1}(\lambda. [1 \mapsto (\lambda. 0_3)_2]0_1)$
• (by def. 1 of substitution) $\rightarrow\ \uparrow^{-1}(\lambda. 0_1)$

Now I've worked myself into a corner - $\uparrow^{-1}(\lambda. 0_1)$ should reduce to $(\lambda. 0_0)_{-1},ドル which is nonsensical. I also haven't actually performed any substitutions, which seems like it must be incorrect. Am I misapplying these definitions somehow?

Answer 1

I figured it out - I was messing up the $\beta$-reduction in the first step by applying the substitution to $(\lambda. 0_1)_0$ instead of just 0ドル_1$. This is the correct sequence of reduction steps:

• $(\lambda. 0_1)_0\ (\lambda. 0_1)_0$
• (by def. of $\beta$-reduction) $\rightarrow\ \uparrow^{-1}([0 \mapsto\ \uparrow^1((\lambda. 0_1)_0)] 0_1)$
• (by def. of $\uparrow$) $\rightarrow\ \uparrow^{-1}([0 \mapsto (\lambda. 0_2)_1] 0_1)$
• (by def. 1 of substitution) $\rightarrow\ \uparrow^{-1}((\lambda. 0_2)_1)$
• (by def. of $\uparrow$) $\rightarrow\ (\lambda. 0_1)_0$

• bbarker: 11 years later but this turned out to be very helpful ... i was also debugging an issue in my interpreter when evaluating id id, though the issue was different. Your step-by-step analysis saved me a lot of time.