[PRL] Stooge sort - Wikipedia, the free encyclopedia

[J. Ian Johnson]

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)
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.
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