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

Problem Detail: 

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?

Asked By : jcsmnt0

Answered By : jcsmnt0

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$

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/16454

 Ask a Question

 Download Related Notes/Documents