[PRL] Stooge sort - Wikipedia, the free encyclopedia
wand at ccs.neu.edu
Thu Jun 16 21:46:01 EDT 2011
Anybody want to formalize this in Coq/ACL2/whatever ?
On Thu, Jun 16, 2011 at 5:32 PM, John Clements <clements at brinckerhoff.org>wrote:
> On Jun 16, 2011, at 1:36 PM, Mitchell Wand wrote:
> > Anybody want to give a proof that this works? --Mitch
> > Link: http://en.wikipedia.org/wiki/Stooge_sort (sent via Shareaholic)
> A real proof, or just a proof sketch?
> 1) It works for lists of size 1 & 2.
> 2) Assume it works for lists of size n. Then prove that it works for lists
> of size 1.5 * n, as follows:
> Given an unsorted list of size 1.5n, consider the elements that belong in
> the upper third (there are 0.5n of these); they're scattered all over.
> After sorting the lower 2/3, though, the elements from this set that
> occurred in the lower 2/3 must now all be in the upper half of that set, and
> thus contained in the middle third of the range. Then, sorting the upper
> 2/3, they're all in the top half of the upper 2/3, and hence in their
> correct spots. By a similar logic, the elements that belong in the lower
> third are moved into the middle or lower third by the first two sorts, and
> the third sort moves them into their proper locations. By a counting
> argument, the elements belonging in the middle third will be in the lower
> 2/3 after the first two sorts, and in their correct locations after the
> There's still some detail to fill in w.r.t. which way to round the division
> between thirds; everything could fall apart in there, I suppose.
-------------- next part --------------
HTML attachment scrubbed and removed
More information about the PRL