encoding binary numerals in lambda calculus

Question

I have not seen any mention of binary numerals in lambda calculus. Church numerals are unary system. I had asked a question of how to do this in Haskell here: How to implement Binary numbers in Haskell But even after I saw and understood that answer, I could not understand how to do this in pure untyped lambda calculus.

So here is my question: Are binary numerals defined in untyped lambda calculus and have the successor and predecessor functions also been defined for them?

Answer 1

Church encoding of a recursive data type is precisely its fold (catamorphism). Before we venture into the messy and not-very-readable world of Church encoded data types, we'll implement these two functions on the representation given in the previous answer. And because we'd like to transfer then easily to the Church encoded variants, we'll have to do both via fold.

Here's the representation from the previous answer (I picked the one which will be easier to work with) and its catamorphism:

data Bin = LSB | Zero Bin | One Bin

foldBin :: (r -> r) -- ^ Zero case.
        -> (r -> r) -- ^ One  case.
        -> r        -- ^ LSB  case.
        -> Bin
        -> r
foldBin z o l = go
  where
    go LSB      = l
    go (Zero n) = z (go n)
    go (One  n) = o (go n)

The suc function adds one to the least significant bit and keeps propagating the carries we get. Once the carry is added to Zero (and we get One), we can stop propagating. If we get to the most significant bit and still have a carry to propagate, we'll add new most significant bit (this is the apLast helper function):

suc :: Bin -> Bin
suc = apLast . foldBin
    (\(c, r) -> if c
        then (False, One r)
        else (False, Zero r))
    (\(c, r) -> if c
        then (True,  Zero r)
        else (False, One r))
    (True, LSB)
  where
    apLast (True,  r) = One r
    apLast (False, r) = r

The pre function is very similar, except the Boolean now tells us when to stop propagating the -1:

pre :: Bin -> Bin
pre = removeZeros . snd . foldBin
    (\(c, r) -> if c
        then (True,  One r)
        else (False, Zero r))
    (\(c, r) -> if c
        then (False, Zero r)
        else (False, One r))
    (True, LSB)

This might produce a number with leading zero bits, we can chop them off quite easily. full is the whole number at any given time, part is full without any leading zeros.

removeZeros :: Bin -> Bin
removeZeros = snd . foldBin
    (\(full, part) -> (Zero full, part))
    (\(full, part) -> (One full, One full))
    (LSB, LSB)

---

Now, we have to figure out the Church encoding. We'll need Church encoded Booleans and Pairs before we start. Note the following code needs RankNTypes extension.

newtype BoolC = BoolC { runBool :: forall r. r -> r -> r }

true :: BoolC
true = BoolC $ \t _ -> t

false :: BoolC
false = BoolC $ \_ f -> f

if' :: BoolC -> a -> a -> a
if' (BoolC f) x y = f x y


newtype PairC a b = PairC { runPair :: forall r. (a -> b -> r) -> r }

pair :: a -> b -> PairC a b
pair a b = PairC $ \f -> f a b

fst' :: PairC a b -> a
fst' (PairC f) = f $ \a _ -> a

snd' :: PairC a b -> b
snd' (PairC f) = f $ \_ b -> b

Now, at the beginning I said that Church encoding of a data type is its fold. Bin has the following fold:

foldBin :: (r -> r) -- ^ Zero case.
        -> (r -> r) -- ^ One  case.
        -> r        -- ^ LSB  case.
        -> Bin
        -> r

Given a b :: Bin argument, once we apply foldBin to it, we get a precise representation of b in terms of a fold. Let's write a separate data type to keep things tidy:

newtype BinC = BinC { runBin :: forall r. (r -> r) -> (r -> r) -> r -> r }

Here you can clearly see it's the type of foldBin without the Bin argument. Now, few helper functions:

lsb :: BinC
lsb = BinC $ \_ _ l -> l

zero :: BinC -> BinC
zero (BinC f) = BinC $ \z o l -> z (f z o l)

one :: BinC -> BinC
one (BinC f) = BinC $ \z o l -> o (f z o l)

-- Just for convenience.
foldBinC :: (r -> r) -> (r -> r) -> r -> BinC -> r
foldBinC z o l (BinC f) = f z o l

We can now rewrite the previous definitions in terms of BinC nearly with 1:1 correspondence:

suc' :: BinC -> BinC
suc' = apLast . foldBinC
    (\f -> runPair f $ \c r -> if' c
        (pair false (one r))
        (pair false (zero r)))
    (\f -> runPair f $ \c r -> if' c
        (pair true (zero r))
        (pair false (one r)))
    (pair true lsb)
  where
    apLast f = runPair f $ \c r -> if' c
        (one r)
        r

pre' :: BinC -> BinC
pre' = removeZeros' . snd' . foldBinC
    (\f -> runPair f $ \c r -> if' c
        (pair true (one r))
        (pair false (zero r)))
    (\f -> runPair f $ \c r -> if' c
        (pair false (zero r))
        (pair false (one r)))
    (pair true lsb)

removeZeros' :: BinC -> BinC
removeZeros' = snd' . foldBinC
    (\f -> runPair f $ \full part -> pair (zero full) part)
    (\f -> runPair f $ \full part -> pair (one full) (one full))
    (pair lsb lsb)

The only significant difference is that we can't pattern match on pairs, so we have to use:

runPair f $ \a b -> expr

instead of:

case f of
    (a, b) -> expr

---

Here are the conversion functions and a few tests:

toBinC :: Bin -> BinC
toBinC = foldBin zero one lsb

toBin :: BinC -> Bin
toBin (BinC f) = f Zero One LSB

numbers :: [BinC]
numbers = take 100 $ iterate suc' lsb

-- [0 .. 99]
test1 :: [Int]
test1 = map (toInt . toBin) numbers

-- 0:[0 .. 98]
test2 :: [Int]
test2 = map (toInt . toBin . pre') numbers

-- replicate 100 0
test3 :: [Int]
test3 = map (toInt . toBin) . zipWith ($) (iterate (pre' .) id) $ numbers

---

Here's the code written in untyped lambda calculus:

lsb  =      λ _ _ l. l
zero = λ f. λ z o l. z (f z o l) 
one  = λ f. λ z o l. o (f z o l)   
foldBinC = λ z o l f. f z o l

true  = λ t _. t
false = λ _ f. f
if' = λ f x y. f x y

pair = λ a b f. f a b
fst' = λ f. f λ a _. a
snd' = λ f. f λ _ b. b

(∘) = λ f g x. f (g x)


removeZeros' = snd' ∘ foldBinC
    (λ f. f λ full part. pair (zero full) part)
    (λ f. f λ full part. pair (one full) (one full))
    (pair lsb lsb)

apLast = λ f. f λ c r. if' c (one r) r

suc' = apLast ∘ foldBinC
    (λ f. f λ c r. if' c
        (pair false (one r))
        (pair false (zero r)))
    (λ f. f λ c r. if' c
        (pair true (zero r))
        (pair false (one r)))
    (pair true lsb)

pre' = removeZeros' ∘ snd' ∘ foldBinC
    (λ f. f λ c r. if' c
        (pair true (one r))
        (pair false (zero r)))
    (λ f. f λ c r. if' c
        (pair false (zero r))
        (pair false (one r)))
    (pair true lsb)

Answer 2

The following paper answers your question. As you can see, there have been investigated several ways to encode binary numerals in lambda calculus.

An Investigation of Compact and Efficient Number Representations in the Pure Lambda Calculus Torben AE. Mogensen http://link.springer.com/content/pdf/10.1007%2F3-540-45575-2_20

Abstract. We argue that a compact right-associated binary number representation gives simpler operators and better efficiency than the left-associated binary number representation proposed by den Hoed and investigated by Goldberg. This representation is then generalised to higher number-bases and it is argued that bases between 3 and 5 can give higher efficiency than binary representation.