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?

Demented

any reason why not just a church list of regular church numerals? – Duppy

I didn't quite understand what do you mean by church list of regular church numerals. But then I don't want a solution to depend upon extrinsic structure like list – Demented

In pure lambda calculus you can easily use Scott encoding of any Haskell data type you want, so translating Haskell to pure lambda calculus is straight-forward. I prefer Scott encoding over Church encoding, since it doesn't force you in to using a catamorphism for everything. Instead you just use recursive functions as usual. – Selfpity

Answer 1

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.

Wolfram

Thanks. "Compact and Efficient Number Representations". This is exactly what I was looking for. Church numerals are way too inefficient. Now with hindsight, it seems I was beating around the bush. – Demented

Answer 2

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)

Dieselelectric

really very great answer but it still looks quite a bit of Haskellish. This answer uses quite a bit of Haskell types. I am looking for an answer in just lambda calculus, no Haskell or any other language. Am I missing anything? Is there a trivial way to get rid of all the Haskell part from this answer and translate it to a bunch of lambda expressions? – Demented

Technically this is Boehm-Berarducci encoding. Church encoding targets the untyped lambda calculus. When you BB encode a type into the polymorphic lambda calculus you get functions both way forming an isomorphism. Nothing of the sort is possible with Church encoding. To figure out the Church encoding, just take the terms and ignore the types – Nickynico

@TemPora: Replace all occurences of BinC with its definition. – Dennis

pre :: Bin -> Bin ???? I haven't followed through, but shouldn't this be Bin -> Maybe Bin? – Irremediable

@SassaNF: Maybe involves another Church... I mean Boehm-Berarducci encoded data type; for simplicity I didn't deal with the zero case. – Dieselelectric

@Dieselelectric I don't think Maybe is introducing anything extraordinary here. Your Bin is a fixed point of functor X = 1+X+X. Maybe Bin is the same as representing Bin as a fixed point of functor X = 1+1+X+X (just one more 1). (Compare Nat and CoNat) – Irremediable

@SassaNF: It's not the same in a same way that 1 + μX. X (which is isomorphic to the unit type) is not isomorphic to μX. 1 + X (which is list). Anyways, that was not the point: this question is about encoding numbers, not encoding bunch of other data types - my implementation relied on pairs and bools; I had no need to introduce yet another encoding. You can always check if the number is zero and return Nothing before calling pre'. – Dieselelectric

Sorry, μX. 1 + X is not a list but the type of natural numbers. – Dieselelectric

@Dieselelectric I am not sure what the difference between X=LSB | Zero X | One X and X=1+X+X is. The encoding of numbers using suc and pre has everything to do with the functors. These functions are merely a initial algebra (along with Bin) and terminal coalgebra (along with Maybe Bin, or CoBin={&inf;}|Bin) for those functors. – Irremediable

@SassaNF: No, I'm addressing your claim that Maybe Bin has the same representation as μX. 2 + X + X. 1 + μX. 1 + X + X has just one extra value over Bin, μX. 2 + X + X has twice as much, in a sense. – Dieselelectric

@Dieselelectric Not sure what muX is in your notation. Maybe X = 1+X. So if Bin=1+Bin+Bin, Maybe Bin=1+(1+Bin+Bin). This certainly is the same as 2+Bin+Bin – Irremediable

@SassaNF: μ is the fix point operation. But no, Bin is isomorphic to [Bool] - at each point you choose either One (True) or Zero (False) and eventually finish with LSB ([]). Maybe Bin is then just Maybe [Bool]. On the other hand, μX. 2 + 2X is a type of Bool list with two different end-of-lists; clearly, this is the same as having [Bool] and Bool telling you which of the original end-of-lists was used. There's no straightforward isomorphism between those two (even though you could probably find some rather complicated one). – Dieselelectric

@Dieselelectric you don't need a isomorphism, only a universal arrow. You already need this arrow, and you proposed to map Zero LSB into Nothing, which is the same as Inf. On the second thought, suc LSB = LSB, so maybe your LSB is already that Inf. – Irremediable

@SassaNF: By the "return Nothing" I meant preCorrect n = if isZero n then Nothing else Just (pre' n). Anyways, I don't see a point in continuing this debate (sorry); if one needs to implement correct version (Bin -> Maybe Bin), the change is small and very straightforward, I will not include it in the answer, because that would needlessly complicate it. – Dieselelectric

@Dieselelectric well, I don't care about correcting the answer; the construction needs to be algebraically correct, and I am trying to figure out what it must be. So the meaning of LSB must be understood. Will removeZeros reduce Zero LSB to LSB? But this means pre (One LSB) /= (Zero LSB), so you have broken suc . pre isomorphism for numbers greater than zero. – Irremediable

@Dieselelectric re: mu. Sorry, haven't seen that use. I've seen F(X)=1+X+X, then Bin=muF, so muF indicates a fix point of the functor; I haven't see mu applied to objects. – Irremediable

@SassaNF: In this representation, every number has infinitely many representations - just add arbitrary amount of Zeros. I'm working on the result of the previous answer. More correct representation would have extactly one representation for any given number; one such representation is data Bin = Zero | LeadingOne [Bool], where Zero represents 0 and LeadingOne represents bits after the most significant bit, for example: 10 == LeadingOne [False, True, False]. – Dieselelectric