-1

I have two questions about $\beta$-reduction in the $\lambda$-calculus. Please find them below. I have also included some background information about how lists (i.e. finite sequences) can be encoded in the $\lambda$-calculus.

Background information

Lists can be encoded in the $\lambda$-calculus in the following way: $$[N_1,N_2,...,N_k] ≜ λc.λn.c N_1 (c N_2 (...(c N_k n)...))$$

Intuitively, the variable $c$ represents the cons operation (which adds an item to the head of the list) and the variable $n$ represents the empty list, nil: note that the term for the empty list is $[\,] = λc.λn.n.$, according to the definition above.

Questions

Q1. Show that the following term $β$-reduces to $6$: $[3,2,1] \, \mathsf{times} \, 1$.

Here the natural numbers $1 , 2 , 3 , \dots$ denote the corresponding Church numerals, that is, the $\lambda$-terms encoding the corresponding natural numbers in the $\lambda$-calculus, and $\mathsf{times}$ is the $\lambda$-term for multiplication. You may use the fact that the $\lambda$-term $\mathsf{times} \, n \, m$ (i.e. $\mathsf{times}$ applied to the Church numerals $n$ and $m$) $\beta$-reduces to the numeral $n×m$.

Q2. The term $\mathsf{cons}$ appends an element to the front of a list.

$$\mathsf{cons} ≜ \lambda x. \lambda l. \lambda c. \lambda n. c x (l c n)$$

Show that it works by reducing $\mathsf{cons} \, 3 \, [2, 1]$ to $[3, 2, 1]$. Make sure to include every $\beta$-step, and try to use abbreviations for readability.

Taroccoesbrocco
  • 16,964

1 Answers1

1

Question 1. Just apply the definition of list and the fact that $\mathsf{times} \, \underline{n} \, \underline{m} \to_\beta^* \underline{n \times m}$, where $\underline{n}$ is the Church numeral of $n$, for every natural number $n$.

\begin{align} [\,\underline{3}, \underline{2}, \underline{1}\,] \, \mathsf{times} \, \underline{1} &= \big( \lambda c. \lambda n. c\,\underline{3} ( c \, \underline{2} (c \, \underline{1} \, n) ) \big) \mathsf{times} \, \underline{1} \\ &\to_\beta \big( \lambda n. \mathsf{times} \,\underline{3} ( \mathsf{times} \, \underline{2} (\mathsf{times} \, \underline{1} \, n) ) \big) \underline{1} \\ &\to_\beta \mathsf{times} \,\underline{3} ( \mathsf{times} \, \underline{2} (\mathsf{times} \, \underline{1} \, \underline{1}) ) \\ &\to_\beta^* \mathsf{times} \,\underline{3} ( \mathsf{times} \, \underline{2} (\underline{1 \times 1}) ) \\ &= \mathsf{times} \,\underline{3} ( \mathsf{times} \, \underline{2} \, \underline{1} ) \\ &\to_\beta^* \mathsf{times} \,\underline{3} ( \underline{2 \times 1} ) \\ &= \mathsf{times} \,\underline{3} \, \underline{2} \\ &\to_\beta^* \underline{3 \times 2} \\ &= \underline{6} \end{align}

Question 2. Just apply the definitions of $\mathsf{cons}$ and of list. \begin{align} \mathsf{cons} \, 3 \, [2, 1] &= (\lambda x. \lambda l. \lambda c. \lambda n. cx (lcn)) \, 3 \, [2,1] \\ &\to_\beta (\lambda l. \lambda c. \lambda n. c\,3 (lcn)) [2,1] \\ &\to_\beta \lambda c. \lambda n. c\,3 ([2,1] cn) \\ &= \lambda c. \lambda n. c\,3 \big((\lambda c'. \lambda n'. c' 2 (c' 1 \, n')) c\,n \big) \\ &\to_\beta \lambda c. \lambda n. c\,3 \big((\lambda n'. c \, 2 (c \, 1 \, n')) n \big) \\ &\to_\beta \lambda c. \lambda n. c\,3 ( c \, 2 (c \, 1 \, n) ) \\ &= [3,2,1] \end{align}

Note that in Question 2, the fact that $1, 2, 3$ are Church numerals do not play any role. Actually, $1, 2, 3$ here could be replaced by any $\lambda$-terms.

Taroccoesbrocco
  • 16,964
  • Thanks for your answer. Its interesting how the Church numerals dont play a role. Based on this, I was wondering, how you could write a λ -term that corresponds to the infinite list [0,1,2,...] ? –  Dec 30 '20 at 20:22
  • In solution 1: Please, what is the difference between →β and →∗β? (Sorry about the formatting of the reduction arrows) –  Dec 31 '20 at 09:50
  • 1
    @MrNemo - $\to_\beta$ is just one $\beta$-step, obtained by firing exactly one $\beta$-redex $(\lambda x.M)N$; while $\to_\beta^*$ is an arbrtrary number of consecutive $\beta$-steps. In general, reduction of $\mathsf{times} , \underline{n} , \underline{m}$ to $\underline{n \times m}$ requires several $\beta$-steps. – Taroccoesbrocco Dec 31 '20 at 10:01
  • Thanks very much for the clarification –  Dec 31 '20 at 10:03
  • Hi @Taroccoesbrocco I was wondering if the solution for your answer on Mr Nemos question (Infinite List) could also be typed? I dont have enough points to comment on that post unfortunately –  Jan 01 '21 at 11:42
  • @vatoslocos - The short answer is not. But it depends on the types system you refer to, there are many types systems. I guess you refer to simple types, which cannot type the fixpoint combinator. – Taroccoesbrocco Jan 01 '21 at 15:17