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

ignougroup
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