What is the meaning of this Church numeral example?

Question

There is an example of Church numeral, on the secion Encoding Datatypes of lambda calculus's wikipedia page.

One way of thinking about the Church numeral n, which is often useful when analysing programs, is as an instruction 'repeat n times'. For example, using the PAIR and NIL functions defined below, one can define a function that constructs a (linked) list of n elements all equal to x by repeating 'prepend another x element' n times, starting from an empty list. The lambda term is

λn.λx.n (PAIR x) NIL By varying what is being repeated, and varying what argument that function being repeated is applied to, a great many different effects can be achieved.

By varying what is being repeated, and varying what argument that function being repeated is applied to, a great many different effects can be achieved.

We can define a successor function, which takes a Church numeral n and returns n + 1 by adding another application of f, where '(mf)x' means the function 'f' is applied 'm' times on 'x':

SUCC := λn.λf.λx.f (n f x)

I don't understand what the PAIR , NIL and SUCC means right now. Since "the PAIR and NIL functions" are "defined below", let's skip them for now and consider SUCC.

What the SUCC means here? Does it mean success, succeed or something else?

I am trying to use Scheme language to define SUCC:

(define succ
  (lambda (n)
    (lambda (f)
      (lambda (x)
        (f ((n f) x))))))

Am I right? If so, what can this succ function do? If not, what is the right definition, and what can it do?

Can you give me some example to explain this? If I can understand SUCC I think I can understand PLUS which defined just below it.

Answer 1

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