Proving terms using induction in LC

computer sciencediscrete mathematicsinductionlambda-calculusproof-writing

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.

Best Answer

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}

Related Solutions

[Math] How to prove a Fibonacci inequality using Strong Induction

You want to use the recurrence $F_{n+1} = F_{n} + F_{n-1}$ and apply the inductive hypothesis to both $F_{n}$ and $F_{n-1}$. What you'll get is that you need to verify:

$$x^{(n+1)-2} \geq x^{n-2} + x^{(n-1)-2}$$

Write out what the terms should be and see if you can show the inequality holds.

[Math] the meaning of this Church numeral example

The word succ means successor; informally, the successor of a natural number $n \in \mathbb N$ is the natural number $n + 1$.

Church numerals are one way to represent the natural numbers. The natural number $n \in \mathbb N$ is represented as the function which takes as its argument another function $f$, and returns the $n$-fold composite $$ \underbrace{f \circ f \circ \cdots \circ f}_{n \text{ times}}. $$ Thus, we have for example that $3(f) = f \circ f \circ f$, or in a more lambda calculus notation we have:

3 f = f . f . f

Or, a "non-point-free" version:

(3 f) x = f (f (f x))

As special cases we have that 0 f = id (or (0 f) x = x) and 1 f = f (or (1 f) x = f x).

Now the successor function has to take a natural number (Church numeral) $n$, and return $n + 1$; thus, it has to take a function which turns functions into their $n$-fold composite, and return a function which turns functions into their $n+1$-fold composite. (There are a lot of layers here, so try thinking about this until it starts to make sense to you.)

The way this is implemented is that it takes a natural number, n, and the resulting thing has to take a function, f, and the resulting thing should be the $n+1$-fold composition of $f$ -- that is, it should take an $x$ and return $$ \underbrace{f(f( \cdots f(x) \cdots ))}_{n+1 \text{ applications}}. $$ In yet other words, it should return f ((n f) x).

This is precisely the code you wrote:

(define succ               #Define function succ, which
  (lambda (n)              #Takes a natural number n, returns a function which
    (lambda (f)            #Takes a function and returns its n+1 fold composite:
      (lambda (x)          #It takes an x and applies f n + 1 times, namely
        (f ((n f) x))))))  #It applies f to "f applied n times to x".

Best Answer

Related Solutions

[Math] How to prove a Fibonacci inequality using Strong Induction

[Math] the meaning of this Church numeral example

Related Question