-Original Message-
From: gsst...@gmail.com [mailto:gsst...@gmail.com] On Behalf Of Greg Stark
Sent: Saturday, March 09, 2013 5:16 PM
To: Dann Corbit
Cc: Bruce Momjian; Peter Geoghegan; Robert Haas; Tom Lane; PG Hackers
Subject: Re: Why do we still perform a check for pre-sorted input within
Yes, you are right. I knew of a median of medians technique for pivot
selection and I mistook that for the median of medians median selection
algorithm (which it definitely isn't).
I was not aware of a true linear time selection of the median algorithm {which
is what median of medians accomplis
"A Machine-Checked Proof of the Average-Case Complexity of Quicksort in Coq"
By Eelis van der Weegen and James McKinna
Institute for Computing and Information Sciences
Radboud University Nijmegen
Heijendaalseweg 135, 6525 AJ Nijmegen, The Netherlands
Contains a formal proof, validated by machine
-Original Message-
From: gsst...@gmail.com [mailto:gsst...@gmail.com] On Behalf Of Greg Stark
Sent: Saturday, March 09, 2013 11:39 AM
To: Dann Corbit
Cc: Bruce Momjian; Peter Geoghegan; Robert Haas; Tom Lane; PG Hackers
Subject: Re: Why do we still perform a check for pre-sorted input withi
Original Message-
>From: gsst...@gmail.com [mailto:gsst...@gmail.com] On Behalf Of Greg Stark
>Sent: Friday, March 08, 2013 4:59 PM
>To: Dann Corbit
>Cc: Bruce Momjian; Peter Geoghegan; Robert Haas; Tom Lane; PG Hackers
>Subject: Re: Why do we still perform a check for pre-sorted input with