[PRL] Stooge sort - Wikipedia, the free encyclopedia

[Carl Eastlund]

On Wed, Jun 22, 2011 at 11:31 AM, J. Ian Johnson <ianj at ccs.neu.edu> wrote:
> I've been spending a little time on this in the mornings, and I can tell you that a formal proof is no simple matter.
> In ACL2, the straightforward implementation is formally impossible to prove terminating since you must know that the output is a list of the same size as the input before admitting the function. Thus, you must add "no-ops" like (if (= (length output) (length input)) [... rest of program ...] 'impossible)

Why do you need this?  You should be able to compute N = 2/3 the size
of the input list once, and any time you recur, do it by taking the
first or last N elements of some intermediate list.  That should make
the size of the input to each recursion N, and proving totality should
be straightforward.

> Once you do that, proving that taking the different thirds of the list for input longer than 2 also requires multiple lemmas about floor, ceiling, take and nthcdr.

Now this, I agree with.  Reasoning about fractions of list lengths in
ACL2 is where I would expect the difficulty to arise.

> I'll respond with more as the proof develops.
> -Ian
> ----- Original Message -----
> From: "Paul A. Steckler" <steck at stecksoft.com>
> To: "Mitchell Wand" <wand at ccs.neu.edu>
> Cc: "Dan Friedman" <dfried00 at gmail.com>, "PRL" <prl at lists.ccs.neu.edu>
> Sent: Friday, June 17, 2011 12:33:41 AM GMT -05:00 US/Canada Eastern
> Subject: Re: [PRL] Stooge sort - Wikipedia, the free encyclopedia
>
> On Fri, Jun 17, 2011 at 11:46 AM, Mitchell Wand <wand at ccs.neu.edu> wrote:
>> Anybody want to formalize this in Coq/ACL2/whatever ?
>
> In Sydney, we're organizing a CoqFight, where contestants will be
> given problems
> to formalize in a competitive setting. This problem might be useful in
> that context (if
> in no other).
>
> -- Paul
>
> _______________________________________________
> PRL mailing list
> PRL at lists.ccs.neu.edu
> https://lists.ccs.neu.edu/bin/listinfo/prl
>
> _______________________________________________
> PRL mailing list
> PRL at lists.ccs.neu.edu
> https://lists.ccs.neu.edu/bin/listinfo/prl
>