Alonzo Church’s insight that lambda is sufficient to express all of computation is a non-intuitive stunning revelation. Showing that numbers can be represented using lambda alone using what’s come to be known as “Church numerals” is also brilliant. However, subtraction was a problem with plain Church numerals. Kleene solved that by using a pair of numbers instead. However even Kleene’s construction doesn’t give us a representation for negative numbers. Here we’ll look at a possible way to use Brahmagupta’s formulation to represent integers using lambda.

Preparatory steps

First off, lambda is adequate to represent data structures. We’re going to need the simplest data structure – a “pair” – for what is to follow, so we present how to do that below first. We’ll be doing all this in Scheme.

; Simple function composition operator. Does right-to-left composition.
(define (⊙ f1 f2) (λ (x) (f1 (f2 x))))

; The pair constructor function simply postpones the method to
; destructure the contents of the pair to a selector function to be
; provided later.
(define (pair x y)
    (λ (selector)
        (selector x y)))

(define (.first x y) x)
(define (.second x y) y)

(define (swap p)
    (pair (p .second) (p .first)))

; Now we can make pairs of things and get the things back out.
(let ([p (pair 2 3)])
   (display (p .first))
   (display (p .second)))

Church numerals

The main idea behind Church numerals is that we represent the numer n as a function f applied to a value x that many times. What are f and x? We don’t really care about that except that the domain and codomain of f must be the same, so that f can be repeatedly applied. For zero, we apply f zero times - i.e. we don’t apply it at all, so we simply have x.

(define ch-zero (λ (f) (λ (x) x)))

; Successor of n is n applications of f followed by one more.
(define (ch-succ n) (λ (f) (⊙ f (n f))))

; Adding 2 numbers amounts to computing a function
; that's the nth successor of m.
(define (ch-add m n) ((n ch-succ) m))
(define (ch-mul m n) (⊙ m n)) ; ch-mul is just ⊙
                              ; - i.e. m applications of n applications of f

; Utility functions for display purposes.
(define (i->ch i)
    (if (equal? i 0)
        ch-zero
        (ch-succ (i->ch (sub1 i)))))

(define (ch->i n)
    ((n add1) 0))

We can’t subtract using this scheme because we don’t have a notion of equality to rely on.

Kleene’s construction

Stephen Kleene solved the subtraction problem by constructing a representation using which the predecessor of a number can be obtained. The idea is simple. You use pairs of Church numerals. You start with [0,0] and the successor of [m,n] is [n,n+1].

(define k-zero (pair ch-zero ch-zero))

(define (k-succ p) 
    (pair (p .second) (ch-succ (p .second))))

(define (ch-pred n)
    (((n k-succ) k-zero) .first))

(define (ch-sub m n) ; for m > n, this is just
                     ; n applications of ch-pred on m
    ((n ch-pred) m))

Now you can use the ch-pred function to get the opposite of the successor.

(ch->i (ch-pred (i->ch 10))) ; displays 9
(ch->i (ch-sub (i->ch 10) (i->ch 3))) ; displays 7 

However, this has an irksome end point –

(ch->i (ch-pred (i->ch 0))) ; display 0

… which is not true for integers.

Church-Brahmagupta numerals

Enter Brahmagupta, who defined integers, in effect, as equivalence classes.

1. 0 stands for combinations of equal counts of “positives” and “negatives”.
2. A positive integer n stands for “a combination of n more positives than negatives” and a negative integer -n stands for “a combination of n more negatives than positives”.

There is a nice symmetry between positive and negative integers that we can exploit for our purpose here.

We can now take Church’s idea of “n stands for applying a function f that many times” and restate it as “n stands for applying a function f that many more times than its inverse finv” for positive n and “-n stands for applying the inverse n more times than the function f”. Obviously, zero is represented as applying f and finv an equal number of times.

But how do we get the inverse of an arbitrary function f? We can use the same Church trick and say “we don’t need to”. We’ll just assume that the caller can provide it and always keep functions in pairs [f,finv].

; This looks the same as ch-zero, but what we mean
; by the `fp` argument is different. `fp` is a pair of functions
; that are inverses of each other.
(define b-zero (λ (fp) (λ (x) x))) 

(define (b-succ n) 
    (λ (fp)
      (⊙ (fp .first) (n fp))))
            
(define (b-pred n)
    (λ (fp)
      (⊙ (fp .second) (n fp))))
           
(define (b-neg n) (⊙ n swap))

(define (b-add m n) ((n (pair b-succ b-pred)) m))
(define (b-sub m n) ((n (pair b-pred b-succ)) m))

(define bp (pair b-succ b-pred))

(define (b-mul m n) ((n (pair (λ (k) (b-add k m))
                              (λ (k) (b-sub k m))))
                     b-zero))
                                    
(define (i->b i)
    (if (equal? i 0)
        b-zero
        (if (> i 0)
            (b-succ (i->b (sub1 i)))
            (b-pred (i->b (add1 i))))))
            
(define (b->i b)
    ((b (pair add1 sub1)) 0))

Note the nice symmetry between the definitions of b-pred and b-succ as well as between b-add and b-sub. This now gives us what we expect of the full integers –

(b->i (b-pred (i->b  0))) ; -1
(b->i (b-pred (i->b 10))) ;  9
(b->i (b-succ (i->b 10))) ; 11
(b->i (b-pred (i->b -5))) ; -6
(b->i (b-succ (i->b -5))) ; -4
(b->i (b-add (i->b 7) (i->b 5))) ; 12
(b->i (b-sub (i->b 7) (i->b 5))) ; 2
(b->i (b-sub (i->b 5) (i->b 7))) ; -2

We sort of lost the simplicity of using the function composition operation to do number multiplication as with the Church numerals. However, the pattern in b-mul suggests the kind of function composition that could work -

(define (b⊙ f1 f2)
  (λ (fp)
    (f1 (pair (f2 fp) (f2 (swap fp))))))

(define (b-mul m n) (b⊙ m n))

This “new function composition” accounts for the fact that our functions expect pairs as arguments but produce non-pair values as result. So we “lift” the function composition to work on pairs. I’m actually quite amused that just trying to pick the simplest “composition function” that meets the type requirements gets us what we want! ¹

Thoughts

To me, these “Church-Brahmagupta numerals” (CBN) above seem less tricky than Kleene’s construction and, if I may add, a tad cleaner due to the symmetric treatment of b-succ and b-pred – i.e. negative numbers and subtraction are not “less privileged” in this representation.

From a pedagogic perspective, the purpose of these constructions is to show that lambda suffices to represent all kinds of entities we might need when writing a program, by showing how one would represent integers and pairs, which underpin other computations and data structures. The CBN seem easier to make that point without leaving logical gaps like “predecessor of 0 is 0”.

References and notes

1. Shriram Krishnamurthy’s Lambda lecture part of the PLAI course. I’ve used mostly the same notation, except using an extra prefix to indicate the choice of representation. Such a prefix helps when the entire code is copied into a single file to play with.

2. There are other ways to represent integers which is in the same spirit, such as using a pair of Church numerals and treating integers as the difference between the two numbers. The approach above, I feel, is a more direct translation of the idea. Besides, it’s always fun to know more ways of understanding the same thing :)

3. I also thank Jonathan Crabtree (founder of https://podometic.in/) for first bringing Brahmagupta’s formulation of integers to my attention. He presented a neat linguistic trick to help teach negative numbers to kids - treat a number like “-7” not as “negative seven” but flip the adjective and noun around as “seven negatives”. That’s essentially Brahmagupta’s formulation which you can see reflected in the way integers are represented in this post as operations on a pair of functions that are inverses of each other. I taught that “trick” to my kid when he was 8 and he picked it up in less than an hour and has not only not forgotten it, but can still do things like subtracting negatives from positives correctly. I’d documented my struggles to teach integers to my older son some years ago.