2007/11/13

QSort in Agda, Round 4

This round we externally prove that qsort returns an increasingly-sorted list. The logic is quite the same, so I'll simply post the code without explanation. A "philosophical" argument follows the code.

partition-bdd : (p : Nat)(xs : List Nat) -> {m n : Nat} ->
                  (bddAbove m ⋯ bddBelow n) xs ->
                  ((\pair -> (bddAbove p ⋯ bddBelow n) (fst pair)) ⋯
                   (\pair -> (bddAbove m ⋯ bddBelow p) (snd pair)))
                  (partition p xs)
partition-bdd p [] {m}{n} _ = (bdd-above-base {p} ‖ bdd-below-base {n}) ‖
                              (bdd-above-base {m} ‖ bdd-below-base {p})
partition-bdd p (x :: xs) {m}{n}
  (bdd-above-step xs-bddabv x≼m ‖ bdd-below-step xs-bddblw n≼x)
  with partition p xs
     | partition-bdd p xs {m}{n} (xs-bddabv ‖ xs-bddblw)
     | cmp x p
... | < ys , zs > | (ys-bddabv ‖ ys-bddblw) ‖ zs-bddpfs | \/-IL x≼p =
  (bdd-above-step ys-bddabv x≼p ‖ bdd-below-step ys-bddblw n≼x) ‖ zs-bddpfs
... | < ys , zs > | ys-bddpfs ‖ (zs-bddabv ‖ zs-bddblw) | \/-IR p≼x =
  ys-bddpfs ‖ (bdd-above-step zs-bddabv x≼m ‖ bdd-below-step zs-bddblw p≼x)

qsort-inc-sorted : ∀ (\xs -> {m n : Nat} ->(bddAbove m ⋯ bddBelow n) xs ->
                     (IncSorted ⋯ bddAbove m ⋯ bddBelow n) (qsort xs))
qsort-inc-sorted [] bddpf = inc-sorted-base ‖ bddpf
qsort-inc-sorted (x :: xs) {m}{n}
  (bdd-above-step xs-bddabv x≼m ‖ bdd-below-step xs-bddblw n≼x)
  with partition x xs | partition-bdd x xs (xs-bddabv ‖ xs-bddblw)
... | < ys , zs > | ys-bdd ‖ zs-bdd
  with qsort-inc-sorted ys ys-bdd | qsort-inc-sorted zs zs-bdd
qsort-inc-sorted (x :: xs) {m}{n}
  (bdd-above-step xs-bddabv x≼m ‖ bdd-below-step xs-bddblw n≼x)
  | < ys , zs > | ys-bdd ‖ zs-bdd | ys'-sorted ‖ ys'-bddabv ‖ ys'-bddblw
                                  | zs'-sorted ‖ zs'-bddabv ‖ zs'-bddblw =
  inc-sorted-concat
    ys'-sorted
    (inc-sorted-step zs'-sorted zs'-bddblw (≼-refl {x}))
    ys'-bddabv
    (bdd-below-step zs'-bddblw (≼-refl {x})) ‖
  bdd-above-concat (relaxUpperBound ys'-bddabv x≼m)
                   (bdd-above-step zs'-bddabv x≼m) ‖
  bdd-below-concat ys'-bddblw
    (relaxLowerBound (bdd-below-step zs'-bddblw (≼-refl {x})) n≼x)

I think it is appropriate to name this kind of proof style externalism, while the intrusive approach taken in round 1 and 2 may be named internalism. The two terms are borrowed from Epistemology, where internalism requires one to provide justification for his/her (true) belief in order to claim that belief is knowledge, while externalism doesn't impose such a requirement but instead allows a justification to be provided externally by someone else.

So far my experience shows that externalism naturally leads to modularized proofs and (at least) won't take more effort than internalism, since Agda supports externalism reasonably well (e.g., magic with), while internalist proofs are coupled with algorithms or data structures and thus hard to combine or reuse. Besides, if one really needs an internalist version, he/she can simply write something like

qsort''′ : List Nat -> List Nat ∣ IncSorted
qsort''′ xs with lemma3 xs
qsort''′ xs | ∃-I _ (xs' ⋮ xs≡xs' ‖ xs'-bdd)
  with qsort-inc-sorted xs' xs'-bdd
qsort''′ xs | ∃-I _ (xs' ⋮ xs≡xs' ‖ xs'-bdd) | xs''-sorted ‖ _ =
  qsort xs ⋮ subst (\ys -> IncSorted (qsort ys)) xs≡xs' xs''-sorted

So currently I think externalism has the advantage over internalism. (Just contrary to the position I take toward epistemic internalism and externalism!)

--
The next (and, very likely, the final) round would be proving the ultimate correctness of qsort!


I think I'm going to stop here since I just can't prove that the relation IsPermutation xs ys is transitive... Anyway, the primary aim of this series of exercises has been achieved, and that's good. XD

Labels: ,

Anonymous scm11/14/2007 6:47 am 說:

辛苦了!That was an amazing amount of interesting work.

Now it appears to me that there are at least three ways to do proofs in a language with dependent type.

1. The first approach I learnt was to use "indexed types", such as List A Nat with its length encoded in the type. You may also define the type of sorted lists or the lists that is a permutation of a particular list, etc.

2. To avoid having to define a new datatype for every property we'd like to prove, I thought about using dependent pairs. Perhaps we can call this "control internalism" and the previous approach "data internalism"?

3. Then I was told that we can always prove all properties separately from the programs, as in your "externalism". This is actually an older approach which, apart from being machine-verifiable, is not too different from how we used to prove programs by hand.

So, if it turns out that 3. is the most modular, I have to think again why people invented 1. There ought to be some advantages, but what is it?

 

<< 回到主頁