[Haskell-cafe] natural mergesort in Data.List

[Joachim Breitner]

Hi,

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-4.11.1.0/docs/src/Data.OldList.html#sort
> 
> (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;
https://github.com/antalsz/hs-to-coq/blob/master/examples/containers/theories/SortSorted.v


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

Cheers,
Joachim



-- 
Joachim Breitner
  mail at joachim-breitner.de
  http://www.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>