[Haskell-cafe] natural mergesort in Data.List

Joachim Breitner mail at joachim-breitner.de
Tue Sep 18 09:45:40 UTC 2018


Am Dienstag, den 18.09.2018, 10:21 +0200 schrieb Christian Sternagel:
> some years ago I formalized the mergesort implementation [1] from
> http://hackage.haskell.org/package/base-
> (as far as I can tell it didn't change since 2012) in the proof
> assistant Isabelle/HOL [2].
> More specifically, I proved its functional correctness (the result is
> sorted and contains all elements of the input with exactly the same
> multiplicities) and that it is a stable sorting algorithm.

just a shameless plug: As part of our hs-to-coq project, we
mechanically translated Data.List.sort to Coq, proved its termination
(for finite inputs, of course) and functional correctness;

> Very recently I also formalized a complexity result in Isabelle/HOL,
> namely that the number of comparisons is bounded from above by
>   n + n * ⌈log 2 n⌉
> for lists of length n.

Cool! That’s of course not easily possible with out shallow embedding
into Coq.

> For this proof I had to change the definition of "sequences",
> "ascending", and "descending" slightly.
> Now here is my question: Does anyone now of reasons why the current
> implementation of "sequences" is allowed to produce spurious empty lists
> in its result? The version I used in my formalization only differs in
> the following three spots:
It _could_ have been benchmarked and measured and determined that it is
actually faster to do less case analysis here. But I find that unlikely
(both the investigation and this output), and it is probably simply an
oversight, and I would expect that a patch to that effect would be
appreciated !


Joachim Breitner
  mail at joachim-breitner.de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: This is a digitally signed message part
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20180918/bb5564e8/attachment.sig>

More information about the Haskell-Cafe mailing list