1
$\begingroup$

I have trouble, when attempting to :

1- prove mult defines the multiplication function.

2- Prove pred defines the predecessor function.

1- for mult:

Base Case:

mult 0x= 0

Inductive case:

:= $(\lambda m. \lambda n. \lambda f . \lambda x.m (nf)x) (\lambda f. \lambda x.x)(\lambda fx. \lambda x.(f^{(n)} x))$

the result is $(\lambda f. \lambda x.x)$.

2- for pred:

Base Case:

f(0,..)= 0

Inductive case:

$\lambda n.\lambda f. \lambda x.n (\lambda g. \lambda h.h (gf)) (\lambda u.x)( \lambda u.u)$.

(f(s(x),..) = n-1

And I am unsure of where to go from there, because I have no parameters for the n to be n-1.

$\endgroup$
  • $\begingroup$ The fact that $(λm.λn.λ f .λx.m (nf)x) (λf. λx.x)(λfx.λx.(f^{(n)} x))$ reduces to $(λf. λx.x)$ proves that $\text{mult} \, 0 \, n = 0$. The inductive case for $\text{mult}$ is completely lacking. $\endgroup$ – Taroccoesbrocco Jan 26 at 11:17
  • $\begingroup$ what about predecessor ? $\endgroup$ – Jared Jan 26 at 12:40
  • $\begingroup$ @Taroccoesbrocco I have been create post for multiplication question. $\endgroup$ – Jared Jan 28 at 1:06
1
$\begingroup$

The proof that the term $\text{pred}$ encodes the predecessor function over natural numbers is quite technical and requires a lemma.

For any $n \in \mathbb{N}$, let $\underline{n} = \lambda f \lambda x. f^{n} x = \lambda f \lambda x. \overbrace{f (\cdots (f}^{n \text{ times}} x) \cdots)$ (in particular, $\underline{0} = \lambda f \lambda x.x$).

Lemma. Given $n \in \mathbb{N}$, $(\lambda g \lambda h.h (g f))^{n+1} (\lambda u.x)$ reduces to $\lambda h.h (f^n x)$

Proof. By induction on $n \in \mathbb{N}$.

  • Base case ($n = 0$):

\begin{align} (\lambda g \lambda h.h (g f)) (\lambda u.x) \to \lambda h.h ((\lambda u.x) f) \to \lambda h.h x \,. \end{align}

  • Inductive step: we suppose that $(\lambda g \lambda h.h (g f))^{n+1} (\lambda u.x)$ reduces to $\lambda h.h (f^n x) \, $ (induction hypothesis) and we show that $(\lambda g \lambda h.h (g f))^{n+2} (\lambda u.x)$ reduces to $\lambda h.h (f^{n+1} x)$.

\begin{align} (\lambda g \lambda h.h (g f))^{n+2} (\lambda u.x) &= (\lambda g \lambda h.h (g f)) \big((\lambda g \lambda h.h (g f))^{n+1} (\lambda u.x) \big) \\ &\to^* (\lambda g \lambda h.h (g f)) (\lambda h.h (f^n x)) \quad \text{(by induction hypothesis)} \\ & \to \lambda h.h ((\lambda h.h (f^nx)) f) \to \lambda h.h (f (f^n x)) = \lambda h.h (f^{n+1} x) \, .\\ &\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad \square \end{align}

Let $\text{pred} = \lambda n \lambda f \lambda x.n (\lambda g \lambda h.h (g f)) (\lambda u.x) (\lambda u.u)$. Thanks to the lemma above, let us show that the term $\text{pred}$ encodes the predecessor function over natural numbers, i.e. that $\text{pred} \, \underline{0}$ reduces to $\underline{0}$, and $\text{pred} \, \underline{n+1}$ reduces to $\underline{n}$ for any $n \in \mathbb{N}$.

  • Case $n = 0$: \begin{align} \text{pred} \, \underline{0} =& \ \big(\lambda n \lambda f \lambda x.n (\lambda g \lambda h.h (g f)) (\lambda u.x) (\lambda u.u) \big) \lambda f \lambda x.x \\ \to& \ \lambda f \lambda x. (\lambda f' \lambda x'.x') (\lambda g \lambda h.h (g f)) (\lambda u.x) (\lambda u.u) \\ \to& \ \lambda f \lambda x. (\lambda x'.x') (\lambda u.x) (\lambda u.u) \\ \to& \ \lambda f \lambda x. (\lambda u.x) (\lambda u.u) \\ \to& \ \lambda f \lambda x. x = \underline{0} \end{align}

  • Case $n + 1$: \begin{align} \text{pred} \, \underline{n+1} =& \ \big(\lambda n \lambda f \lambda x.n (\lambda g \lambda h.h (g f)) (\lambda u.x) (\lambda u.u) \big) \lambda f \lambda x. f^{n+1}x \\ \to& \ \lambda f \lambda x. (\lambda f' \lambda x'. (f')^{n+1}x') (\lambda g \lambda h.h (g f)) (\lambda u.x) (\lambda u.u) \\ \to& \ \lambda f \lambda x. (\lambda x'. (\lambda g \lambda h.h (g f))^{n+1} x') (\lambda u.x) (\lambda u.u) \\ \to& \ \lambda f \lambda x. (\lambda g \lambda h.h (g f))^{n+1} (\lambda u.x) (\lambda u.u) \\ \to& \ \lambda f \lambda x. (\lambda h. h (f^n x)) (\lambda u.u) \quad \text{(by the lemma)}\\ \to& \ \lambda f \lambda x. (\lambda u.u) (f^n x) \\ \to& \ \lambda f \lambda x. f^n x = \underline{n} \, . \end{align}


The proof that the term $\text{mult}$ encodes the multiplication function over natural numbers is similar to (and slightly simpler than) the proof above.

$\endgroup$
  • $\begingroup$ Thanks. but for mult do I need to have exponential ? $\endgroup$ – Jared Jan 26 at 22:52
  • $\begingroup$ @Jared - Yes, but I guess a complete answer for $\text{mult}$ requires a new question, otherwise this answer becomes too long. $\endgroup$ – Taroccoesbrocco Jan 27 at 9:46
  • $\begingroup$ Ok , I will post it. math.stackexchange.com/questions/3089352/multiplication-prove $\endgroup$ – Jared Jan 27 at 9:49

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.