3

Expanding on the following question here and on the book on the $\lambda$-calculus I'm reading, I'm trying to prove the correctness of the given solution in a more complicated manner.

Let $(F_n')_{n \in \mathbb{N}}$ be the family of terms defined by induction on $n \in \mathbb{N}$ as follows:

\begin{align} F_0' &= m & F_{n+1}' &= c \, \underline{n+1} \, F_n' \end{align}

where $c$ and $m$ are variables, and $\underline{n}$ is the Church numeral representing $n \in \mathbb{N}$.

I'm trying to prove by induction on $n \in \mathbb{N}$ that $$F'_n[\mathsf{times}/c,\underline{1}/m] →_\beta^* \underline{n!}$$ and thus, by setting $F_n = \lambda c. \lambda m. F_n'$, $$F_n \, \mathsf{times} \, \underline{1} →_\beta^* \underline{n!}$$ where $!$ is factorial, and $\mathsf{times}$ is a term such that $\mathsf{times} \, \underline{a} \, \underline{b} \to_\beta^* \underline{a \times b}$ for any $a, b \in \mathbb{N}$. How can I do it?

The proof should hopefully prove that the solution given in the previous question is valid and demonstrate the functionality of foldr function from haskell.

Arturo Magidin
  • 398,050
gaming4 mining
  • 125

1 Answers1

1

It is possible to prove that, for every $n \in \mathbb{N}$, we have $F_n'[\mathsf{times}/c, \underline{n}/m] \to_\beta^* \underline{n!}$, by straightforward induction on $n \in \mathbb{N}$.

  • Base case $n = 0$: By definition, $F_0' = m$ and so $F_0'[\mathsf{times}/c, \underline{1}/m] = \underline{1} = \underline{0!}$ (remember that $0! = 1$), and so $F_0'[\mathsf{times}/c, \underline{1}/m] \to_\beta^* \underline{0!}$ because $\to_\beta^*$ is a reflexive relation.

  • Inductive case: Given $n \in \mathbb{N}$, we suppose that $F_n'[\mathsf{times}/c, \underline{n}/m] \to_\beta^* \underline{n!}$ (this is our inductive hypothesis) and we want to show that $F_{n+1}'[\mathsf{times}/c, \underline{n\!+\!1}/m] \to_\beta^* \underline{(n\!+\!1)!}$. By definition, $F_{n+1}' = c \, \underline{n\!+\!1} \, F_n'$ and hence \begin{align} F_{n+1}'[\mathsf{times}/c, \underline{n\!+\!1}/m] &= \mathsf{times} \, \underline{n\!+\!1} \, (F_n'[\mathsf{times}/c, \underline{n}/m]) \\ &\to_\beta^* \mathsf{times} \, \underline{n+1} \, \underline{n!} &&\text{(by inductive hypothesis)} \\ &\to_\beta^* \underline{(n+1) \times n!} &&\text{(by definition of $\mathsf{times}$)} \\ &= \underline{(n+1)!} \end{align}

So, we have proved that, for every $n \in \mathbb{N}$, $$\tag{$*$} F_n'[\mathsf{times}/c, \underline{n}/m] \to_\beta^* \underline{n!}$$ As a consequence, $F_n \, \mathsf{times} \, \underline{1} \to_\beta^* \underline{n}$ for every $n \in \mathbb{N}$. Indeed, \begin{align} F_n \, \mathsf{times} \, \underline{1} &= (\lambda c. \lambda m. F_n') \mathsf{times} \, \underline{1} \\ &\to_\beta (\lambda m. F_n'[\mathsf{times}/c])\underline{1} \\ &\to_\beta F_n'[\mathsf{times}/c, \underline{n}/m] \\ &\to_\beta^* \underline{n!} &&\text{(by $(*)$)} \end{align}

Taroccoesbrocco
  • 16,964