# Representation of Church numerals

In the $$\lambda$$-calculus, is the family of $$\lambda$$-terms $$(N_i)_{i \in \mathbb{N}}$$, defined below, a representation of Church numerals? I think it is, but how do I (sufficiently) show it? If not, what is it?

The terms $$N_i$$ and $$N'_i$$ for each natural number $$i$$ are defined as follows. ($$x$$ and $$c$$ are variables while $$i$$ stands for a number.) \begin{align} N'_0 &= x \\ N'_i &= c \,i\, N'_{i−1} &&\text{for } i > 0 \\ N_i &= \lambda c. \lambda x. N'_i &&\text{for any }i \in \mathbb{N} \end{align}

• I don't understand the definition of $N_i' = c \, i \, N_{i-1}'$. Indeed, $i$ is a natural number, not a $\lambda$-term, so $N_i'$ would not be a $\lambda$-term. Maybe do you mean $N_i'= c \, N_{i-1}'$? Jan 2, 2021 at 6:38
• First off @Taroccoesbrocco, what do you use to get such nice formatting? To answer your question: what if in addition to i being a number (as stated) it was also its Church encoding?
– user156182
Jan 2, 2021 at 9:56
• To write mathematical notations with a nice and readable layout, please use MathJax. A quick tutorial is here. It takes a bit of time to become familiar with it, but it helps a lot yourself and your readers. Jan 2, 2021 at 10:33
• If $i$ is not only a natural number but also the Church numeral representing $i$, then your question becomes an abstract nonsense. In your question you're defining Church numerals inductively, but in the definition of $N_i'$ (which is mandatory to define then the Church numeral for $i$) you assume that the Church for $i$ is already defined. An unsolvable vicious circle. Jan 2, 2021 at 10:38
• @Taroccoesbrocco well to avoid nonsense perhaps lets go with your initial suggestion of a correction. I really appreciate your time helping me here!!!!
– user156182
Jan 2, 2021 at 10:45

Disclaimer. I assume that the inductive definition of the $$\lambda$$-terms $$(N_n')_{n \in \mathbb{N}}$$ given in the original question, i.e., \begin{align} N_0' &= x \\ N_n' &= f \, n \, N_{n-1}' &\text{if } n > 0 \end{align}

contains a typo: $$N_n'$$ should be defined as $$f \, N_{n-1}'$$ when $$n > 0$$, because $$n$$ is a natural number and not a $$\lambda$$-term, so the expression$$f \, n \, N_{n-1}'$$ does not make any sense in the $$\lambda$$-calculus. My answer below considers the amended version of that definition.

Church numerals are the $$\lambda$$-terms used to encode natural numbers in the $$\lambda$$-calculus.

Usually, for every natural number $$n$$, the Church numeral $$\underline{n}$$ representing $$n$$ is defined as the $$\lambda$$-term $$\tag{1} \underline{n} = \lambda f. \lambda x. f^n x = \lambda f. \lambda x. \overbrace{f(f( \cdots (f}^{n \text{ times }}x)\cdots))$$ ($$f^n x$$ is just a shorthand for $$\overbrace{f(f( \cdots (f}^{n \text{ times }}x)\cdots))$$, for any $$n \in \mathbb{N}$$).

This definition is slightly informal because it uses dots, which$$-$$strictly speaking$$-$$are not in the syntax of the $$\lambda$$-calculus. How can we define Church numerals in a more rigorous way?

As human beings, we are perfectly able to understand what dots mean. If we fix $$n \in \mathbb{N}$$, from $$(1)$$ we are able to write the concrete Church numeral for $$n$$. For instance: \begin{align} \underline{0} &= \lambda f. \lambda x. x & \underline{1} &= \lambda f. \lambda x. fx & \underline{4} &= \lambda f. \lambda x. f(f(f(fx))) \end{align} So, for the usual practice, definition $$(1)$$ is perfect. But if we want to write a very rigorous proof of a property of the $$\lambda$$-calculus involving all Church numerals, what do we do? Are we sure that dots cannot hide some pathological and unexpected behavior of Church numerals?

This search for a more rigorous definition is not only a pedantic issue, but it is of practical interest. Suppose that we want to implement the $$\lambda$$-calculus in a computer, for instance to use automated theorem provers to verify some property of the $$\lambda$$-calculus involving Church numerals. How can a computer understand dots?

In mathematics, when you use dots to define an object, it usually means that the object is defined by induction. In the case of Church numerals, we proceed by induction on $$n \in \mathbb{N}$$. Actually, in $$(1)$$ dots appear only in the $$f^n x$$ part, so the inductive definition is required only for a rigorous definition of $$\tag{2} f^n x = \overbrace{f(f( \cdots (f}^{n \text{ times }}x)\cdots))$$ Formally, for every $$n \in \mathbb{N}$$ we define the $$\lambda$$-term $$N_n'$$ by induction on $$n$$ as follows: \begin{align} N_0' &= x &&\text{(base case)} \\ N_{n}' &= f \, N_{n-1}' &&\text{(inductive step, for n > 0)} \end{align}

What is the relation between this inductive definition and $$(2)$$?

Property. For every $$n \in \mathbb{N}$$, we have $$\tag{3} f^n x = N_n'.$$

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

• Base case ($$n = 0$$): $$f^0 x = \overbrace{f(f( \cdots (f}^{0 \text{ times }}x)\cdots)) = x = N_0'.$$
• Inductive step: We suppose that property $$(3)$$ holds for some $$n \in \mathbb{N}$$ (induction hypothesis, IH) and we show that it holds for $$n+1$$.

$$f^{n+1} x = \overbrace{f(f( \cdots (f}^{n+1 \text{ times }}x)\cdots)) = f \,(\overbrace{f(f( \cdots (f}^{n \text{ times }}x)\cdots))) = f (f^n x) \overset{\text{IH}}{=} f \, N_{n}' = N_{n+1}'. \quad \square$$

We have just proved $$(3)$$, that is, that for every $$n \in \mathbb{N}$$ the $$\lambda$$-term $$f^nx$$ defined via dots in $$(2)$$ is the same as the $$\lambda$$-term $$N_n'$$ defined inductively. From $$(3)$$ it follows that Church numerals defined in $$(1)$$ are exactly the same as the $$\lambda$$-terms $$(N_n)_{n \in \mathbb{N}}$$ defined as follows:

\begin{align} N_n &= \lambda f. \lambda x. N_n' &\text{for every } n \in \mathbb{N}. \end{align}

Indeed, for every $$n \in \mathbb{N}$$, we have $$\underline{n} = \lambda f. \lambda x. f^n x \overset{(3)}{=} \lambda f. \lambda x. N_n' = N_n.$$