1
$\begingroup$

I am learning lambda calculus as my previous questions indicate . But in a different book , namely , The structure and interpretation of computer program I cam across the concept of "church numerals " and the stumbled upon the following link about church numerals :

https://www.cs.rice.edu/~javaplt/311/Readings/supplemental.pdf

It goes on stating the following in the first page :

The Church numerals that follow just have additional applications of the successor function:

$$\begin{align} C_2 &= \lambda f . \lambda x . f(fx) \\ C_3 &= \lambda f . \lambda x . f(f(fx))\\ C_4 &= \lambda f . \lambda x . f(f(f(fx)))\\ &\vdots\\ C_n &= \lambda f . \lambda x . f nx \end{align} $$

and then he mentions that had we been having a little more powerful language then we could define the following two functions : $$\begin{align} S &= \lambda r.\text{“ring the small bell (ding) and apply r”}\\ Z &= \lambda r.\text{“ring the big bell (dong)”} \end{align} $$ and then says that the application of

$C_4$ to $S$ and $Z$ would yield "ding ding ding ding dong"

How to explain the above result without even knowing what "f" is ?

POST EDIT : After I got the first answer , I tried computing the sequence by the help of clue provided .

By applying step by step I will get (lambda r.ding r)^4 (lambda r.dong) = (lambda r.ding r)^4 dong .

Now each evaluation of (lambda r.ding r) leads to "ding r " .

So the overall evaluation becomes "ding ding ding ding r dong ".

Am I doing it right ?If yes then , how to account for omission of r in the expression?

P.S : For some trivia information , has there been any known application of this idea of church numerals to any field of mathematics ?

$\endgroup$
  • 2
    $\begingroup$ By applying "C4 to S and Z" essentially you substitute all occurence of "f" within C4 with S. So you do know what "f" is with respect to that application. Try expanding the application step by step to confirm the result. $\endgroup$ – Apiwat Chantawibul Jun 17 '17 at 17:19
  • $\begingroup$ @Billiska :In the definition of S what is the significance of "apply r " ? And by applying step by step I will get (lambda r.ding r)^4 (lambda r.dong) = (lambda r.ding r)^4 dong . Now each evaluation of (lambda r.ding r) leads to "ding r " .So the overall evaluation becomes "ding ding ding ding r dong " ..right ? If yes then , how to account for omission of r in the expression ? $\endgroup$ – Agnivesh Singh Jun 17 '17 at 18:34
1
$\begingroup$

Using your definition for Church Numerals and trying to see what's going on:

$$ \begin{align} 0 &= \lambda f. \lambda x. x \\ 1 &= \lambda f. \lambda x. f x\\ 2 &= \lambda f. \lambda x. f f x\\ 3 &= \lambda f. \lambda x. f f f x\\ &\vdots \end{align} $$

Now let's say have a function $g$ and some $a$, try to use $g$ and $a$ as arguments to $0$, that is:

$$ \begin{align} 0 ~ g ~ a &= (\lambda fx. x)~g~a\\ \quad &\rhd_{1\beta} ([g/f] (\lambda x.x)) a = (\lambda x.x) a \\ \quad &\rhd_{1\beta} [a/x]x = a \end{align} $$

So $g$ applied $0$ times to $a$ returns $a$.

Now try to do the same with $1$.

$$ \begin{align} 1 ~ g ~ a &= (\lambda fx. f~x)~g~a\\ \quad &\rhd_{1\beta} ([g/f] (\lambda x.f~x)) a = (\lambda x.g~x) a \\ \quad &\rhd_{1\beta} [a/x]g~x = g ~ a \end{align} $$

So $g$ applied $1$ time to $a$ is indeed $g(a)$.

Your problem is $4 ~ g ~ a$, where $g$ is $S$ and $a$ is $Z$.

$$ \begin{align} S &= \lambda r.\text{“ring the small bell (ding) and apply r”}\\ Z &= \lambda r .\text{“ring the big bell (dong)}” \end{align} $$

Doing $1 ~ S ~ Z$ we already know that evaluates to $S(Z)$. And that translates to "print 'Ding' then apply $r$ ", where $r$ just prints 'Dong'. So it outputs 'Ding Dong'.

$\endgroup$
  • $\begingroup$ This answer is using the convention $ffx$ = $f(fx)$ which is (IMO) better but the opposite of the common way to do it. $\endgroup$ – DanielV Jul 9 '17 at 19:06

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.