Recently I got curious about p-adic numbers and was wondering how to construct them just using lambda calculus. Why? No real reason except to entertain myself. I realized that to do that I need to first represent modular numbers – i.e. numbers as equivalence classes of the natural numbers – and the arithmetic around them before I can proceed to do this. So this is a follow on to the earlier workout involving paired up functions and their inverses applied to representing integers - in Church-Brahmagupta numerals.

Now, it is not that nobody has tried to do modular arithmetic in lambda calculus. ¹ But I want to do it in the same spirit as the earlier attempt, in plain Racket so that students can follow the code and also run it and play with it to convince themselves. We’ll initially formulate it using #lang lazy and then point out where modifications are needed to implement it in #lang racket.

The basic Church numerals

We’ll start off with the basic Church numerals and the Kleene construction.

#lang lazy 

; Pairs
(define (pair x y) (λ (f) ((f x) y)))
(define ((.first x) y) x)
(define ((.second x) y) y)

; Function composition
(define (⊙ f g) (λ (x) (f (g x))))

; Church numerals and the Kleene construction
(define zero (λ (f) (λ (x) x)))
(define (succ n) (λ (f) (⊙ f (n f))))
(define kzero (pair zero zero))
(define (ksucc kn) (pair (kn .second) (succ (kn .second))))
(define (pred n) (((n ksucc) kzero) .first))

; Some common numbers we'll use.
(define one (succ zero))
(define two (succ one))
(define three (succ two))

; For reading convenience, we define the zero? predicate like this.
(define (ifzero n a b)
  ((((n (λ (f) .second)) .first) a) b))

; Convenience converters from Racket naturals to Church encoding
; and back. Helps with debugging.
(define (i->n i) (if (= i 0) zero (succ (i->n (sub1 i)))))
(define (n->i n) ((n add1) 0))

How can we represent the equivalence classes required for, say, “modulo 3 arithmetic”? ² One way is to define a circular structure, perhaps like this -

(define zero3 
  (pair zero (pair one (pair two zero3))))

The idea here is that zero3 is a pair whose .first will give you the Church numeral corresponding to the equivalence class. To get the next one, you pick the .second, and if you keep doing that, eventually you end up looping back to zero3. So -

; ... where `n` is a modular numeral and `msucc` stands
; for successorship of such a numeral. Note that for this
; we don't need to know the modulus itself.
(define (msucc n) (n .second))

; For the modular predecessor, we need to know the modulus.
; Here `m` is a Church numeral representing the modulus and
; `n` is a modular number whose predecessor we want.
(define ((mpred m) n) (((pred m) msucc) n))

We’re almost in business now. Let’s also define some convenience functions to go between Racket’s natural numbers and our modular numbers.

(define (i->m3 i) (((i->n i) msucc) zero3))
(define (m3->i n) (n->i (n .first)))

The actual arithmetic

Since we have a nice mapping from the equivalence classes to the corresponding Church numerals, ordinary modular arithmetic is rather easy. Here we use the short cut of getting the “zero” in a particular modulus by subtracting a from itself. We also assume that the numerals being operated on are all represented using the same modulus.

; `m` is given in Church encoding but that arguments are
; in the representation for that modulus.
(define (((madd m) a) b) (((a .first) msucc) b))
(define (((msub m) a) b) (((b .first) (mpred m)) a))
; Add b to mzero a times.
(define (((mmul m) a) b) (((a .first) ((madd m) b))
                          (((msub m) a) a)))
; Multiply a to 1 b times.
(define (((mexp m) a) b) (((b .first) ((mmul m) a))
                          (msucc (((msub m) a) a))))

The sequence of moduli

“Modulo 1” is a useless one since we can’t even count in it, with zero being the only member of this set. However it gives us a basic case to define.

(define zero1 (pair zero zero1))

Now let’s look at the structure of zero2, zero3 and so on.

(define zero2 (pair zero (pair one zero2)))
(define zero3 (pair zero (pair one (pair two zero3))))
(define zero4 (pair zero (pair one (pair two (pair three zero4)))))
; ...

The pattern there is staring right back at us. We can write that “sequence of modular representations” as -

(define zero1f
  (λ (f) (pair zero f)))
(define zero2f
  (λ (f) (zero1f (pair one f))))
(define zero3f
  (λ (f) (zero2f (pair two f))))
(define zero4f
  (λ (f) (zero3f (pair three f))))
; ...

Here, the zero1/zero2/zero3 are fixed points of the corresponding zero1f/zero2f/zero3f.

We can therefore generalize that like so –

; m is a Church numeral for the modulus
(define (zeromf m)
  (ifzero (pred m)
    zero1f
    ((zeromf (pred m)) (pair (pred m) f))))

So now, given zero1f, we can define the other moduli as –

(define zero2f (zeromf two))
(define zero3f (zeromf three))
; ...

To wrap it up, we’ll need to complete the definitions of the zerom using a fixed point combinator. We can use the 𝚯 combinator for it.

(define (𝚯 f) (f (𝚯 f)))
(define zero1 (𝚯 zero1f))
(define zero2 (𝚯 zero2f))
(define zero3 (𝚯 zero3f))
;...

Now a simple test that the equivalence classes are working -

(!! (map (λ (n) (m3->i (i->m3 n))) '(1 2 3 4 5 6 7)))
; prints 
; '(1 2 0 1 2 0 1)

In eager #lang racket

Lazy/recursive defines are doing some heavy lifting in the code we’ve written so far. If we change the language to #lang racket and run the last example, we can see that it eventually blows up.

The blow up is primarily due to the definition of zeromf where the ifzero eagerly evaluates both branches and therefore descends without stopping. We can get around that by η-abstracting the recursive else part.

#lang racket

; m is a Church numeral for the modulus
(define (zeromf m)
  (ifzero (pred m)
    zero1f
    (λ (k) (((zeromf (pred m)) (pair (pred m) f)) k))))

To be even more pedantic and not assume the named recursion facility provided by Racket’s define construct even in the eager mode, we can transform the recursive definition accordingly.

(define ((zeromf/norec f) m)
  (ifzero (pred m)
    zero1f
    (λ (k) (((f (pred m)) (pair (pred m) f)) k))))
(define zeromf (𝚯 zeromf/norec))

Since the combinator itself cannot rely on recursive defines now, we can rewrite it as …

; From ((theta g) f) = (f ((g g) f))
; η-abstracting the argument to f in the RHS ...
(define ((theta g) f) (f (λ (k) (((g g) f) k))))
(define 𝚯 (theta theta))

Concluding

What we have here is a pure lambda-calculus representation of modular numbers and their required arithmetic operations, constructed based on Church numerals. We could’ve done that by first implementing remainder computation on Church numerals, but this approach, in my opinion, is more fun as it directly captures the equivalence classes and the remainder computation emerges as a consequence of the cyclical structure that represents them.

Next up

I suppose the next itch to scratch would be representing p-adic numbers. However, we really can’t do that except by constraining to a “rational” subset, similar to how we can’t represent the entire real number set directly since the set of all expressions that can compute numbers is only countably infinite, but the reals are uncountably infinite, and so are the p-adic numbers (though with a different topology I gather).

Anyway, I’m just dipping my toes in the p-adic waters and haven’t yet learnt to swim.