[Haskell-cafe] natural mergesort in Data.List

[David Feuer]

If you're guaranteeing that the result won't contain empty lists, it would
be worth benchmarking the effect of using NonEmpty x instead of [x] in that
spot.

On Tue, Sep 18, 2018, 4:21 AM Christian Sternagel <c.sternagel at gmail.com>
wrote:

> Dear Cafe,
>
> 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.
>
> 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.
>
> 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:
>
>   sequences [x] = [[x]] -- this is the only important change, since
>   sequences [] = []     -- then the result does not contain empty lists
>
> instead of
>
>   sequences xs = [xs]
>
> and
>
>   ascending a as [] = let !x = as [a] in [x]
>
> instead of
>
>   ascending a as bs = let !x = as [a] in x : sequences bs
>
> and
>
>   descending a as []  = [a:as]
>
> instead of
>
>   descending a as bs = (a:as) : sequences bs
>
> [1] https://www.isa-afp.org/entries/Efficient-Mergesort.html
> [2] http://isabelle.in.tum.de/
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20180918/c6aca18f/attachment.html>