23 July, 2010

branching on the left vs branching on the right (agda bubble sort part 3)

I gave a definition of onepass, the inner loop of my Agda bubblesort implementation, in an earlier post.

That wasn't the first implementation that I tried.

Instead, first I wrote it like this, in a way that uses with expressions. The difference is that the version I wrote uses an if construct that is manually defined. Agda seems to prefer doing case analysis / branching using with, which makes it seem as if you're getting a new parameter to pattern match on - in the below example, the results of y ≤? y which is either yes _ or no _.

onepass : {n : ℕ}→ Vec ℕ n → Vec ℕ n
  onepass {zero} [] = []
  onepass {suc zero} (y :: []) = y :: []
  onepass {suc (suc n)} (y :: (y' :: y0)) with y ≤? y'
  ... | yes _ = y :: (onepass {suc n} (y' :: y0))
  ... | no _ = y' :: (onepass {suc n} (y :: y0))

For comparison, here's the definition in my first post:

onepass {suc (suc n)} (y :: (y' :: y0)) = if y ≤? y' then        
                                        y :: (onepass {suc n} (y' :: y0))     
                                   else y' :: (onepass {suc n} (y :: y0))  

The two implementations do the same thing at runtime - they swap the first two elements of the list and recurse. But their compile-time behaviour is different.

The with-based version doesn't pass the termination checker. The if-based one does.

The with-based version with with the proofs that I gave in part 2. The if based version doesn't.

So I pretty much am forced to choose: I can use the with-based definition, and turn off the termination checker in the Agda compiler. Or not. Either way seems pretty lame. In order to proof all this stuff, I have to turn off the termination checker which is a key part of checking the proofs that I'm writing.

I don't really understand what is going on inside Agda to make the first version not work. But that's what I actually use in practice (with termination checking turned off) - perhaps I can investigate a bit more later. But for now, I want to continue working on a proof (albeit not termination checked) that bubblesort actually sorts...


  1. Anonymous24/7/10 02:00

    Here's an idea:
    Theorem: After k passes of bubblesort (from beginning to end), the last k elements of your list are in ascending order and the (n-k+1)th element is larger-or-equal than all of the first (n-k) elements in the list.

    Proof: Use induction on the number of passes of bubblesort.

    By the way, on the k-th pass, you only need to consider the first (n-k+1) elements of your list; this number decreases when k increases, so you get a proof of termination as well.

  2. anonymous: yep, that's basically the structure of my attempts at a sortedness proof. Hopefully I'll manage to get it to work soon - it seems to be taking me longer than I expected...

  3. btw, I *have* a termination proof - the variable {n} gets smaller on every recursive call. Agda can see that (if I phrase the program the if-based way)