2
$\begingroup$

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?

$\endgroup$
3
$\begingroup$

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$
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.