Peano induction for binary numbers (bis)

August 7th, 2007 by Conor

This is a story from the early days of designing Epigram. It’s a case study of equipping a data structure with a funny induction principle. I want to show that a binary representation of positive numbers satisfies a unary induction principle. I think I got the problem from Nicolas Magaud a while back, but Hugo Herbelin reminded me of it at CHIT/CHAT, so I dug it out of my bottom drawer. I’ll be informal, tending to Agda, notationally.

Positive binary numbers are snoc-lists of bits with a 1 at the front.


> data Bit  = 0 | 1
> data Bin  = 1 | Bin;Bit

We can easily write their successor operation by structural recursion.


> bsuc : Bin -> Bin
> bsuc 1        = 1 ; 0
> bsuc (b ; 0)  = b ; 1
> bsuc (b ; 1)  = bsuc b ; 0

Now the task is to give


%format forall = “\forall”

> binPeano :  (P : Bin -> *) ->
>             P 1 ->
>             ((i : Bin) -> P i -> P (bsuc i)) ->
>             (b : Bin) -> P b

I’ll give a broken attempt, followed by my proof, and then James McKinna’s proof.

Let’s try fixing P and its closure properties, then proceeding by structural recursion on b.


> binPeano P p1 ps b = p b where
>   p 1        = p1
>   p (b ; 0)  = {P (b ; 0)}
>   p (b ; 1)  = {P (b ; 1)}

Now what? In the ‘even’ case, we can get our hands on p b : P b, but we need to show P (b ; 0), so we need to do a successor step b times. If only we knew how to iterate b times…but that’s what we’re trying to achieve in the first place. Arse!

So let’s try again, except that instead of trying to prove P, let’s try to establish ability to iterate. I’ll move b to the front, and keep P inside the induction.


%format forall = “\forall”

> binPeano :  (b : Bin) ->
>             (P : Bin -> *) ->
>             P 1 ->
>             ((i : Bin) -> P i -> P (bsuc i)) ->
>             P b
>
> binPeano 1        P p1 ps = p1
> binPeano (b ; 0)  P p1 ps = binPeano b (\b -> P (b ; 0))
>   {P (1 ; 0)}
>   {(i : Bin) -> P (i ; 0) -> P (bsuc i ; 0)}
> binPeano (b ; 1)  P p1 ps = binPeano b (\b -> P (b ; 1))
>   {P (1 ; 1)}
>   {(i : Bin) -> P (i ; 1) -> P (bsuc i ; 1)}

What has happened here? By keeping P inside the induction, we’ve turned it into what ripplers would call a ‘sink’ capable of absorbing the differences between the induction hypothesis and the induction conclusion. And that’s how we use it: to prove P of twice b, prove (P of twice) b! The remaining holes are pretty easy to fill, for (bsuc i ; 0) is exactly bsuc (bsuc (i ; 0)), and so on. To finish the job, we need to establish the base cases, then do a double step. That is, to iterate (twice b) times, do a double step b times.


%format forall = “\forall”

> binPeano :  (b : Bin) ->
>             (P : Bin -> *) ->
>             P 1 ->
>             ((i : Bin) -> P i -> P (bsuc i)) ->
>             P b
>
> binPeano 1        P p1 ps = p1
> binPeano (b ; 0)  P p1 ps = binPeano b (\b -> P (b ; 0))
>   (ps p1)
>   (\i -> ps (i ; 1) . ps (i ; 0))
> binPeano (b ; 1)  P p1 ps = binPeano b (\b -> P (b ; 1))
>   (ps (ps p1))
>   (\i -> ps (bsuc i ; 0) . ps (i ; 1))

So that’s that, except that it’s a bit tricky and a bit higher-order and, worst of all, quite expensive in the size of the inductions involved. If we’re being scrupulous about universe levels, we have to be careful about quantifying over arbitrary P : Bin -> Set_i. To be allowed such a thing, we need to use our structural induction principle at Set_(i+1). Pricey! But with universe polymorphism (if only we had it) ok.

Then along comes James McKinna and shows us how to keep it first-order and small, all the way along. Instead of working with arbitrary predicates closed under 1 and bsuc, work with the smallest such predicate, as it implies the others. What’s the smallest? Why, the inductively defined predicate!


> data Peano : Bin -> * where
>   p1    : Peano 1
>   psuc  : Peano i -> Peano (bsuc i)

Now, the weak rule induction principle for Peano is exactly the induction principle we want, except that it imposes the precondition that Peano should actually hold, of course. Our mission is now to show that it does.


> peano : (b : Bin) -> Peano b
> peano 1        = p1
> peano (b ; 0)  = double (peano b)
> peano (b ; 1)  = psuc (double (peano b))
>
> double : Peano b -> Peano (b ; 0)
> double p1        = psuc p1
> double (psuc p)  = psuc (psuc (double p))

And we’re done. James and I liked this trick so much, we designed a programming language to exploit it. That’d be Epigram.

Recent FP lunches, as well as conversations with James McKinna, Randy Pollack, Lucas Dixon, Roy McCasland, Alan Bundy and J Strother Moore have me thinking again about this stuff. Watch this space…

5 Responses to “Peano induction for binary numbers (bis)”

  1. Russell O'Connor Says:

    Epigram 2 won’t have inductively defined families, so the family Peano cannot be defined as such. How will this work in Epigram 2?

  2. jag Says:

    Shouldn’t it be

    bsuc (b; 1) = bsuc b; 0

    ?

  3. Conor Says:

    I don’t know why the rss feed only just kicked in. Sorry for the appallingly slow response.

    jag, you’re absolutely right; I’ve fixed it.

    Russell, Epigram 2′s core theory has the restricted kind of inductive families you get in Agda 1, where constructors must target the full range of indices. You’re right, with that alone you can’t define Peano. However, unlike Agda 1, we also have a propositional equality, and that allows us to simulate full inductive families in a uniform way by adding “Ford equations”. So, in this example, we won’t say “p1 returns Peano 1″, but we will say “p1 returns Peano b for any b you like as long as it’s equal to 1″. In the source language, we’ll sugar away the explicit equation mangling (much as we currently do), so it looks pretty much the way it does now.

  4. Russell O'Connor Says:

    > worst of all, quite expensive in the size of the inductions involved.

    Can you elaborate on this? What is expensive, and how are you measuring the size of inductions?

    I find it a little unfair that peano got a helper function, but binPeano has to do all the work itself. More fair would be to say

    binPeano (b;1) P p1 ps := ps (binPeano (b;0) P p1 ps)

    Of course the body of binPeano (b;0) would have to be given it’s own name (binDouble) to make this properly structurally recursive.

  5. Conor Says:

    I tried to reply to this a few days ago and something went wrong. Here goes again.

    By size, I mean the universe inhabited by the motive of the induction. binPeano quantifies over the motive inside the induction, so elimination over Set(n+1) is required to justify elimination over Set(n). Meanwhile, the Peano family is just an ordinary Set, and it does for all.

    I guess I’d also observe that binPeano is a higher-order function full of continuation-passing voodoo, whilst peano and its little friend are first order. Some people love that higher-order stuff, and finality in general, because you can do anything, but I love initiality, because it enables me to see everything.

Leave a Reply