TONIATUH

A Little Background

Numbers are an integral part of our lives. Whether we like it or not, they govern the way we think, act and live.

Nevertheless, regardless of their ubiquity, little cause is made of why or how they come about.

This series of articles documents an attempt to construct numbers, from the natural numbers (0,1,…) to the rationals (fractions), exclusively using functions. This first post documents the creation of the natural numbers.

Lambda Calculus

To represent functions, we will use Alonzo Church’s lambda calculus. Lambda calculus is a very elegant and minimal notation for functions and applications. In lambda calculus, functions are first class residents and can be passed around as parameters to other, higher order functions.

The syntax we will use for lambda calculus is the following:

• standalone names or letters represent variables
• functions, or abstractions are written as: λx. M where x denotes the variable and M denotes the application; this notation is equivalent to the f(x) = M you are more likely to remember from school, except the function is anonymous
• the expression f N denotes the application of the function f to the argument N.

The basic operation of lambda calculus we will use in this article is called β-reduction. It is written as (λx.M)N → M[x:=N]. It consists in substituting the bound variable of an application with its argument, and allows us to “apply” functions to parameters. In the example above, the variable x is substituted by the value N in the body of the expression M.

As a parallel to this notation, we will also write the functions in a lisp language to allow for reader experimentation and provide another way to grasp these functions.

Uncle Peano

Giuseppe Peano is an Italian mathematician whose five axioms, introduced in 1889, provide a rigorous foundation for the natural numbers:

1. Zero is a natural number
2. all natural numbers have a successor
3. Zero is not the successor of any natural number
4. If two natural numbers have the same successor, then they are the same number
5. If a set contains Zero and the successor of every number in the set is in the set, then the set contains all the natural numbers

Peano axioms in lambda calculus

The first thing to do if we want to construct numbers is to define the natural numbers.

To do so, we define zero := λf.λx. x, and suggest the function inc := λn.λf.λx.(f ((n f) x)) as a means to get the successor of another church-natural.

Here are our functions implemented in scheme:

(define zero
  (lambda (f)
    (lambda (x) x)))

(define (inc n)
  (lambda (f)
    (lambda (x) (f ((n f) x)))))

To prove that this works, we check our two functions against the Peano axioms.

1. We have indeed defined zero so we are clear

2. We have defined a function to compute the successor of any church-natural, so all church-naturals have a successor

3. Let us show this by contradiction. Let us assume zero is the successor of a church-natural. Then:

   ∃a, (inc a) = 0 ⇒ λf.λx.(f ((a f) x)) = λf.λx.x

   Which is a contradiction

4. This can be proven easily:

   (inc a) = (inc b)

   ⇒ λf.λx.(f ((a f) x)) = λf.λx.(f ((b f) x))

   ⇒ a = b

5. Let us prove this by induction.

   • basis: if a set contains zero and the successor of every number in itself, then it contains zero
   • induction: if a set contains zero and the successor of every number in itself, and it contains n, then, by inductive hypothesis, it contains (inc n).

Bijection between church-naturals and naturals

An alternative way to show that the church notation is a convincing notation for natural numbers is to prove that there exists a bijection between church-naturals and natural numbers.

We first define a function to transform natural numbers to church-naturals:

nat->church := λn.λf.λx.fⁿ x

This function effectively composes f, n times.

We then define a function to transform church-naturals to naturals:

church->nat := λn. (n (λx. x+1)) 0

This function effectively counts how many times the function f is composed in a church-natural.

In scheme, these two functions can be implemented that way:

(define (church->nat n)
  ((n (lambda (x) (+ 1 x))) 0))

(define (nat->church n)
  (define (loop f x n)
    (if (zero? n) x
        (f (loop f x (- n 1)))))
  (lambda (f)
    (lambda (x) (loop f x n))))

All we are left to do is prove that these two functions are bijections.

Let us first prove that nat->church is injective. For all a, b naturals, we have:

We have proven that nat->church is injective. Now, let us prove it is surjective. For all \(b\), a church natural, we fix \(a = \text{church->nat } b\). We have:

We have proven that nat->church is both injective and surjective, we have thus proven it is bijective.

Now, let us prove that church->nat is injective. For all a, b church-naturals, we have:

church->nat a = church->nat b ⇒ (a (λx.x+1)) 0 = (b (λx.x+1)) 0

But a is of the form λf.λx.f^n_a x and b is of the form λf.λx.f^n_a x. Hence: