<div dir="auto">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.</div><br><div class="gmail_quote"><div dir="ltr">On Tue, Sep 18, 2018, 4:21 AM Christian Sternagel <<a href="mailto:c.sternagel@gmail.com">c.sternagel@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Dear Cafe,<br>
<br>
some years ago I formalized the mergesort implementation [1] from<br>
<br>
<br>
<a href="http://hackage.haskell.org/package/base-4.11.1.0/docs/src/Data.OldList.html#sort" rel="noreferrer noreferrer" target="_blank">http://hackage.haskell.org/package/base-4.11.1.0/docs/src/Data.OldList.html#sort</a><br>
<br>
(as far as I can tell it didn't change since 2012) in the proof<br>
assistant Isabelle/HOL [2].<br>
<br>
More specifically, I proved its functional correctness (the result is<br>
sorted and contains all elements of the input with exactly the same<br>
multiplicities) and that it is a stable sorting algorithm.<br>
<br>
Very recently I also formalized a complexity result in Isabelle/HOL,<br>
namely that the number of comparisons is bounded from above by<br>
<br>
  n + n * ⌈log 2 n⌉<br>
<br>
for lists of length n.<br>
<br>
For this proof I had to change the definition of "sequences",<br>
"ascending", and "descending" slightly.<br>
<br>
Now here is my question: Does anyone now of reasons why the current<br>
implementation of "sequences" is allowed to produce spurious empty lists<br>
in its result? The version I used in my formalization only differs in<br>
the following three spots:<br>
<br>
  sequences [x] = [[x]] -- this is the only important change, since<br>
  sequences [] = []     -- then the result does not contain empty lists<br>
<br>
instead of<br>
<br>
  sequences xs = [xs]<br>
<br>
and<br>
<br>
  ascending a as [] = let !x = as [a] in [x]<br>
<br>
instead of<br>
<br>
  ascending a as bs = let !x = as [a] in x : sequences bs<br>
<br>
and<br>
<br>
  descending a as []  = [a:as]<br>
<br>
instead of<br>
<br>
  descending a as bs = (a:as) : sequences bs<br>
<br>
[1] <a href="https://www.isa-afp.org/entries/Efficient-Mergesort.html" rel="noreferrer noreferrer" target="_blank">https://www.isa-afp.org/entries/Efficient-Mergesort.html</a><br>
[2] <a href="http://isabelle.in.tum.de/" rel="noreferrer noreferrer" target="_blank">http://isabelle.in.tum.de/</a><br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
To (un)subscribe, modify options or view archives go to:<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
Only members subscribed via the mailman list are allowed to post.</blockquote></div>