`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...

Here's an idea:

ReplyDeleteTheorem: 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.

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...

ReplyDeletebtw, 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)

ReplyDelete