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.
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)))
The main idea behind Church numerals is that we represent the numer
n as a
f applied to a value
x that many times. What are
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
times - i.e. we don’t apply it at all, so we simply have
(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.
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
(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.
Enter Brahmagupta, who defined integers, in effect, as equivalence classes.
0stands for combinations of equal counts of “positives” and “negatives”.
- A positive integer
nstands for “a combination of
nmore positives than negatives” and a negative integer
-nstands for “a combination of
nmore 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
many times” and restate it as “
n stands for applying a function
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
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
; 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-succ as well
b-sub. This now gives us what we expect of the full
(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! 1
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
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
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. ↩︎