TONIATUH

A Short Recap

In the last post, we used Alonzo Church’s lambda calculus to define the natural numbers. We then proved that the set thus obtained was indeed equivalent to the set of natural numbers we are all familiar with.

As a second step in the process of defining numbers up to the rationals exclusively using functions, we now set out to define the relative integers.

To begin with, although it might not be apparent why just yet, we need to define a means to use pairs. In fact, pairs are an integral part of the method we will use to define church-ints in this post, and church-rats in the future.

Church Pairs

As a first step to create church pairs and access the elements stored within, we define functions that take in two parameters and return the first, or the second one.

• The function that takes in two values and returns the first is λx.λy. x
• The one that takes in two values and returns the second one is λx.λy. y

Now, with these two functions, we are most of the way there. All we are left to do is to find a way to create a church pair structure, and interface it with the above functions. We choose to define make-pair, the function to construct church pairs, in the following way: make-pair:= λa.λb.λf. ((f a) b).

This function is then very easy to interface with the functions previously defined to get the first and second element of a church pair. We define first this way: first:= λp.p (λa.λb. a). We then define second this way: second:= λp.p (λa.λb. b).

In scheme, these functions can be defined like this:

(define (make-pair a b)
  (lambda (z) (z a b)))

(define (first p)
  (p (lambda (a b) a)))

(define (second p)
  (p (lambda (a b) b)))

Constructing Z

Now that we know how to create pairs and how to represent Natural numbers with lambda calculus, we have all we need to construct the relative integers. All that is left is to combine these two pieces in an elegant way.

To do so, we first draw attention to the fact that Natural numbers can be thought of as a ray originating in zero and continuing into infinity. We can extend this representation and imagine a similar ray that originates in zero and continues into minus infinity. What is striking is that those two rays are objectively the same, they both describe the Natural numbers but are oriented differently. It thus appears that we can construct the Relative integers using a pair of natural numbers.

In such a pair, the first of the elements would represent the negative part of the number, while the second part of the element would represent the positive part of the number. To give you an example, 2 could be written as (0,2) or (5,7) or in infinitely many other ways, as long as the second element minus the first is 2. All those representations are said to be equivalent. Similarly, -3 can be written as (3,0) or (8,5) for example.

Now that we know how to conceptualize relative integers using pairs and natural numbers, we just have to define the functions to use and manipulate them.

First of all, we note that zero does not change much. With nat-zero:= λf.λx. x, we have zero:= (make-pair nat-zero) nat-zero.

Increment now only increments the right element of the pair: With nat-inc:= λn.λf.λx. f ((n f) x), we now have inc:= λn. (make-pair (first n)) (nat-inc (second n)). Similarly, we can define dec, the function that decrements our relative integer in the following way: dec:= λn. (make-pair (nat-inc (first n))) (second n).

This notation is a nice generalization of the one we used for our Church-nats.

In scheme, the functions can be defined in that way:

(define zero
  (make-pair n-zero n-zero))

(define (inc n)
  (make-pair (first n)
             (n-inc (second n))))

(define (dec n)
  (make-pair (n-inc (first n))
             (second n)))

Z-Ring Operations

To complete our definition of the rational numbers, we need to define the two ring operations on our newly defined relative integers.

As a first step, we define addition and multiplication on the natural numbers.

Addition and Multiplication in N

Addition

We first define addition in the following way: n-add:= λm.λn.λf.λx.((m f) ((n f) x)).

To show that it is, in fact, addition as we know it over the natural numbers, we need to show that it is associative, commutative, and that there exists an additive identity element.

To show that n-add is associative, we develop (a+b)+c and a+(b+c) separately for three church naturals a, b, c and show that the two sums are the same.

(n-add (n-add a b) c) = (n-add (λf.λx.((a f) ((b f) x))) c) = λf.λx.((a f) ((b f) ((c f) x)))

(n-add a (n-add b c)) = (n-add a (λf.λx.((b f) ((c f) x)))) = λf.λx.((a f) ((b f) ((c f) x)))

We see that the two sums are equal to each other, hence we have shown that n-add is associative.

To show that n-add is commutative, we have to show that a+b and b+a are equivalent, for any two church naturals a and b.

(n-add a b) = λf.λx.((a f) ((b f) x)) of the form (f^a (f^b x)) = f^(a+b) x

(n-add b a) = λf.λx.((b f) ((a f) x)) of the form (f^b (f^a x)) = f^(b+a) x

We see that the two sums are equivalent, hence we have show that n-add is commutative.

Finally, it is easy to show that we have an additive identity element. It is sufficient to partially apply n-add to n-zero to be convinced of it; we get n-add n-zero = λn.λf.λx.((n f) x), which is an identity function over the Church-nats.

We have shown that the n-add function is associative, commutative and has an additive identity element in the set of natural numbers, it is thus an addition¹.

Multiplication

We now define multiplication in the following way: n-mul:= λm.λn.λf.λx.((m (n f)) x).

To show that this operation is multiplication as we know it over the natural numbers, we need to show that it is associative, distributive over addition and that there exists a multiplicative identity element.

To show that n-mul is associative, we develop (a×b)×c and a×(b×c) separately for three church naturals a, b, c and show that the two products are the same.

(n-mul (n-mul a b) c) = (n-mul (λf.λx.(a (b f)) x) c) = λf.λx.((a (b (c f))) x)

(n-mul a (n-mul b c)) = (n-mul a (λf.λx.(b (c f)) x)) = λf.λx.((a (b (c f))) x)

We see that the two products are equal to each other, hence we have shown that n-mul is associative.

To show that n-mul is distributive over addition, we show that a×(b+c) develops into a×b + a×c.

First, we develop (n-mul α (n-add β γ)):

We have shown that a×(b+c) develops into a×b + a×c, we thus conclude that n-mul is distributive over addition.

Finally, we show that one := λf.λx.(f x) is a a valid multiplicative identity element. If we partially apply n-mul to one, we end up with n-mul one = λn.λf.λx.((n f) x), which is an identity function over the Church-nats.

We have shown that the n-mul function is associative, distributive over addition and that there exists a multiplicative identity element in the set of natural numbers, it is thus a multiplication².

In scheme

In scheme, we can implement the two operations this way.

(define (n-add a b)
  (lambda (f)
    (lambda (x) ((a f) ((b f) x)))))

(define (n-mul a b)
  (lambda (f)
    (lambda (x) ((a (b f)) x))))

Ring Operations in Z

Now that we have the ring operations in N, we can extend them in order for them to work in Z.

This time, since scheme offers a clearer and cleaner notation than that of raw λ-calculus, we directly present the function’s implementation in scheme. Here the let form is used exclusively to make it easier to understand and grasp the functions. The left and right variables in the make-pair call at the end can easily be replaced by the content of their respective let forms.

(define (add a b)
  (let ((left (n-add (first a)
                     (first b)))
        (right (n-add (second a)
                      (second b))))
    (make-pair left right)))

(define (mul a b)
  (let ((left (n-add (n-mul (first a) (second b))
                     (n-mul (second a) (first b))))
        (right (n-add (n-mul (first a) (first b))
                      (n-mul (second a) (second b)))))
    (make-pair left right)))

Now, with these two operations defined, all we are left to do is to check that they follow the three ring axioms.

Addition

We first notice that our addition over church-ints is indeed an addition. Indeed, we have shown that n-add is associative and commutative, and add only serves as a wrapper to extend n-add to our church-ints. We also note that the identity element is still zero.

Now, to prove that our set is indeed a ring, we must also show that all of our church-ints have an inverse element with respect to addition. To do so, we define the operation inv the operation that switches the first and second element of a pair. In scheme:

(define (inv n)
  (make-pair (second n)
             (first n)))

We then set out to prove that inv actually returns the additive inverse of any church-int. Fix α the church-int with positive part a and negative part b, that is to say α = (make-pair a b), with a, b church-nats. Then:

Which is in fact equivalent to zero, from our definition of equivalence. Moreover, since zero is the additive identity element, we have shown that every church-int has an additive inverse.

We have thus shown that, under our definition, our addition function respects all that it should for the set of church-ints to be a ring.³

Multiplication

Okay, so here, we’re gonna cheat a little. Since even the function is terribly painstaking to write, and we proved that all the relevant properties held for n-mul, we will assume they carry over to our definition of mul as well. We also note that the multiplicative identity is still one, in any of its equivalent forms.

With this efficient dodging maneuver, we conclude that the set of church-ints is indeed a ring when adjoined to add and mul.

Conclusion

In the previous post, we used lambda calculus to define the set of natural numbers.

Using it as a basis, in this article we set out to construct the ring of integers. We succeeded, proving (mostly) everything along the way, once again highlighting the power and versatility of functions in the process.

If you found anything that you don’t understand or spot a mistake that I made, don’t hesitate to send me a mail.