[PRL] Stooge sort - Wikipedia, the free encyclopedia

[Mitchell Wand]

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
> third.
>
> 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.
>
> John
>
>
-------------- next part --------------
HTML attachment scrubbed and removed