Lambda Calculus Beta reductions

Solution 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.