<div dir="auto">It may. Or it may not. The performance impact of such small changes can be hard to predict.</div><br><div class="gmail_quote"><div dir="ltr">On Tue, Sep 18, 2018, 10:38 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 David,<br>
<br>
thanks for the pointer.<br>
<br>
Btw: I was able to modify my complexity proof so that "sequences" is no<br>
longer required to only contain non-empty lists. Sorry for the noise.<br>
<br>
But maybe such a "sequences" is not entirely useless: Did I understand<br>
correctly that what you are saying is that knowing that all elements in<br>
"sequences" are non-empty lists might have some impact on performance<br>
due to being able to use "NonEmpty a"?<br>
<br>
cheers<br>
<br>
chris<br>
<br>
On 09/18/2018 03:18 PM, David Feuer wrote:<br>
> data NonEmpty a = a :| [a]<br>
> <br>
> It's a nonempty list, defined in Data.List.NonEmpty.<br>
> <br>
> On Tue, Sep 18, 2018, 9:14 AM Christian Sternagel <<a href="mailto:c.sternagel@gmail.com" target="_blank" rel="noreferrer">c.sternagel@gmail.com</a><br>
> <mailto:<a href="mailto:c.sternagel@gmail.com" target="_blank" rel="noreferrer">c.sternagel@gmail.com</a>>> wrote:<br>
> <br>
> Dear David,<br>
> <br>
> I am guaranteeing (since I proved it in Isabelle/HOL) that the following<br>
> version of "sequences" does not contain empty lists in its result (I am<br>
> copying from my Isabelle formalization, in order to avoid typos) ;)<br>
> <br>
> fun sequences :: "'a list ⇒ 'a list list"<br>
> and asc :: "'a ⇒ ('a list ⇒ 'a list) ⇒ 'a list ⇒ 'a list list"<br>
> and desc :: "'a ⇒ 'a list ⇒ 'a list ⇒ 'a list list"<br>
> where<br>
> "sequences (a # b # xs) =<br>
> (if key a > key b then desc b [a] xs else asc b ((#) a) xs)"<br>
> | "sequences [x] = [[x]]"<br>
> | "sequences [] = []"<br>
> | "asc a as (b # bs) =<br>
> (if ¬ key a > key b then asc b (λys. as (a # ys)) bs<br>
> else as [a] # sequences (b # bs))"<br>
> | "asc a as [] = [as [a]]"<br>
> | "desc a as (b # bs) =<br>
> (if key a > key b then desc b (a # as) bs<br>
> else (a # as) # sequences (b # bs))"<br>
> | "desc a as [] = [a # as]"<br>
> <br>
> The "key" function is an implicit first parameter for each of<br>
> "sequences", "asc", and "desc" above. The fact that I am using a "key"<br>
> function instead of a comparator is due to Isabelle/HOL's standard<br>
> library. Also, there are no pattern guards in Isabelle/HOL. Anyway, it<br>
> should be relatively straight-forward to translate these functions into<br>
> Haskell.<br>
> <br>
> Another thing: I just realized that "merge_pairs" in my formalization<br>
> also differs from "mergePairs", since with the changed "sequences" it<br>
> might actually get an empty list as input, in which case the current<br>
> "mergePairs" wouldn't terminate at all.<br>
> <br>
> So for those who are interested, the full definition of mergesort can be<br>
> found here<br>
> <br>
> <br>
> <a href="https://devel.isa-afp.org/browser_info/current/AFP/Efficient-Mergesort/Efficient_Mergesort.html" rel="noreferrer noreferrer" target="_blank">https://devel.isa-afp.org/browser_info/current/AFP/Efficient-Mergesort/Efficient_Mergesort.html</a><br>
> <br>
> where mergesort is called "msort_key".<br>
> <br>
> cheers<br>
> <br>
> chris<br>
> <br>
> Btw: What is "NonEmpty x"?<br>
> <br>
> On 09/18/2018 11:55 AM, David Feuer wrote:<br>
> > If you're guaranteeing that the result won't contain empty lists, it<br>
> > would be worth benchmarking the effect of using NonEmpty x instead of<br>
> > [x] in that spot.<br>
> ><br>
> > On Tue, Sep 18, 2018, 4:21 AM Christian Sternagel<br>
> <<a href="mailto:c.sternagel@gmail.com" target="_blank" rel="noreferrer">c.sternagel@gmail.com</a> <mailto:<a href="mailto:c.sternagel@gmail.com" target="_blank" rel="noreferrer">c.sternagel@gmail.com</a>><br>
> > <mailto:<a href="mailto:c.sternagel@gmail.com" target="_blank" rel="noreferrer">c.sternagel@gmail.com</a> <mailto:<a href="mailto:c.sternagel@gmail.com" target="_blank" rel="noreferrer">c.sternagel@gmail.com</a>>>> wrote:<br>
> ><br>
> > Dear Cafe,<br>
> ><br>
> > some years ago I formalized the mergesort implementation [1] from<br>
> ><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<br>
> result is<br>
> > sorted and contains all elements of the input with exactly the<br>
> same<br>
> > multiplicities) and that it is a stable sorting algorithm.<br>
> ><br>
> > Very recently I also formalized a complexity result in<br>
> 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<br>
> current<br>
> > implementation of "sequences" is allowed to produce spurious<br>
> empty lists<br>
> > in its result? The version I used in my formalization only<br>
> differs in<br>
> > the following three spots:<br>
> ><br>
> > sequences [x] = [[x]] -- this is the only important change,<br>
> since<br>
> > sequences [] = [] -- then the result does not contain<br>
> 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.<br>
> ><br>
> <br>
</blockquote></div>