1
$\begingroup$

today I found this term in our exercises: ((^fx.f(f(f x)) ^gy.g(g y )) ^z.z + 1) (0)

I am quit unaware how to solve this type of question. I know this is the church numeral 3 , 2 , the identity function +1 and zero. But for my understanding it lacks an operator like +-*/ as ex.

(λmn.m (succ n)) to connect two church numerals?

Some hints will be greatly appreciated.

$\endgroup$
  • 5
    $\begingroup$ What does it mean to 'solve' this exercise? What do you want to do with this term? $\endgroup$ – Discrete lizard Apr 23 at 16:10
4
$\begingroup$

Your term is the application $3\ 2\ succ\ 0$, where $succ$ is the successor function.

If you task is to reduce this term to a beta normal form:

First we can observe that for terms $M$ and $N$, the application $MN$ beta-reduces to the $M$-fold application of $N$, which is

  • in the case of $N$ an operation: the $M$-fold application of the operation $N$ to whatever term $P$ the term $MN$ is applied to; i.e., $MNP$ is $\underbrace{N(N(...N(}_{M\text{ times}} P)))$,
  • in the case of $N$ a church number: the (church number representation of the) exponentiation of $N$ with $M$; i.e, $MN$ with $M,N$ numbers is $N^M$.

as you can easily verify with simple numbers like $2$ and $3$.

So $3\ 2$ is $2^3$, which beta-reduces to $8$, and $3\ 2\ succ$ creates an 8-fold application of $succ$, which is then applied to $0$.
So your term is the $2^3$-fold = $8$-fold application of the $succ$-function to the number $0$, that is, $\underbrace{succ(succ(...succ(}_{8 \text{ times}} 0)))$, which eventually beta-reduces to the church number $8$, $\lambda fx.f(f(f(f(f(f(f(f(x))))))))$.

$\endgroup$
2
$\begingroup$

Essentially your term is the application $3\ 2\ {\sf succ}\ 0$. So we start performing beta reduction steps. Since $3\ f\ x = f(f(f x))$, we get $2\ (2\ (2\ {\sf succ}))\ 0$. From here, we get $(2\ (2\ {\sf succ}))\ ((2\ (2\ {\sf succ}))\ 0)$. And so on -- I'll leave the steps to you.

If I see correctly, after a long-ish sequence of beta steps we should reach the numeral $8$ as a normal form. Try checking that $(2\ (2\ {\sf succ}))\ 0 = 4$, and after that check that $(2\ (2\ {\sf succ}))\ 4 = 8$.

$\endgroup$

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.