Alonzo Church’s insight that lambda
is sufficient to express all of
computation is a nonintuitive 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 righttoleft 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 chzero (λ (f) (λ (x) x)))
; Successor of n is n applications of f followed by one more.
(define (chsucc n) (λ (f) (⊙ f (n f))))
; Adding 2 numbers amounts to computing a function
; that's the nth successor of m.
(define (chadd m n) ((n chsucc) m))
(define (chmul m n) (⊙ m n)) ; chmul is just ⊙
;  i.e. m applications of n applications of f
; Utility functions for display purposes.
(define (i>ch i)
(if (equal? i 0)
chzero
(chsucc (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 kzero (pair chzero chzero))
(define (ksucc p)
(pair (p .second) (chsucc (p .second))))
(define (chpred n)
(((n ksucc) kzero) .first))
(define (chsub m n) ; for m > n, this is just
; n applications of chpred on m
((n chpred) m))
Now you can use the chpred
function to get the opposite
of the successor.
(ch>i (chpred (i>ch 10))) ; displays 9
(ch>i (chsub (i>ch 10) (i>ch 3))) ; displays 7
However, this has an irksome end point –
(ch>i (chpred (i>ch 0))) ; display 0
… which is not true for integers.
ChurchBrahmagupta numerals
Enter Brahmagupta, who defined integers, in effect, as equivalence classes.
0
stands for combinations of equal counts of “positives” and “negatives”. A positive integer
n
stands for “a combination ofn
more positives than negatives” and a negative integern
stands for “a combination ofn
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 chzero, but what we mean
; by the `fp` argument is different. `fp` is a pair of functions
; that are inverses of each other.
(define bzero (λ (fp) (λ (x) x)))
(define (bsucc n)
(λ (fp)
(⊙ (fp .first) (n fp))))
(define (bpred n)
(λ (fp)
(⊙ (fp .second) (n fp))))
(define (bneg n) (⊙ n swap))
(define (badd m n) ((n (pair bsucc bpred)) m))
(define (bsub m n) ((n (pair bpred bsucc)) m))
(define bp (pair bsucc bpred))
(define (bmul m n) ((n (pair (λ (k) (badd k m))
(λ (k) (bsub k m))))
bzero))
(define (i>b i)
(if (equal? i 0)
bzero
(if (> i 0)
(bsucc (i>b (sub1 i)))
(bpred (i>b (add1 i))))))
(define (b>i b)
((b (pair add1 sub1)) 0))
Note the nice symmetry between the definitions of bpred
and bsucc
as well
as between badd
and bsub
. This now gives us what we expect of the full
integers –
(b>i (bpred (i>b 0))) ; 1
(b>i (bpred (i>b 10))) ; 9
(b>i (bsucc (i>b 10))) ; 11
(b>i (bpred (i>b 5))) ; 6
(b>i (bsucc (i>b 5))) ; 4
(b>i (badd (i>b 7) (i>b 5))) ; 12
(b>i (bsub (i>b 7) (i>b 5))) ; 2
(b>i (bsub (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 bmul
suggests the kind of function composition that
could work 
(define (b⊙ f1 f2)
(λ (fp)
(f1 (pair (f2 fp) (f2 (swap fp))))))
(define (bmul m n) (b⊙ m n))
This “new function composition” accounts for the fact that our functions expect pairs as arguments but produce nonpair 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! ^{1}
Thoughts
To me, these “ChurchBrahmagupta numerals” (CBN) above seem less tricky than
Kleene’s construction and, if I may add, a tad cleaner due to the symmetric
treatment of bsucc
and bpred
– 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

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.

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 :)

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.

I’m now rather curious about this composition operation, but am not waiting to figure out more of that to post this. ↩︎