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