Understanding church numerals

Question

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 ?

Answer 1

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'.