[PRL] Stooge sort - Wikipedia, the free encyclopedia

[Carl Eastlund]

On Wed, Jun 22, 2011 at 11:54 AM, J. Ian Johnson <ianj at ccs.neu.edu> wrote:
> 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.
>
> (defun stsort (x)
>  (cond ((endp x) nil)
>        (t (let ((l (if (< (last x) (first x))
>                           (swap-ends x)
>                         x)))
>                (if (< (length l) 3)
>                    l
>                  (let* ((l (append (stsort (lower2/3 l))
>                                    (upper1/3 l)))
>                         (l (append (lower1/3 l)
>                                    (stsort (upper2/3 l)))) ;; oh bugger
>                         (l (append (stsort (lower2/3 l))
>                                    (upper1/3 l))))
>                    l))))))
> The intermediate lists depend on the output of the function. We need to know that the length of the first (and second) append is equal to the length of x.

Only because you wrote it that way.  Instead of writing lower1/3,
upper2/3, and so forth, I would simply compute i = len(x), j = 2/3 i,
and then use take or drop of j or i-j in each instance.  Rather than
needing to know that the length of each append is equal to i, I would
simply assume it.  Totality would then be easy.  Proving correctness,
on the other hand, would require proving these lengths to be the same
-- but with all involved functions proved total, this should be much
easier.

>
>>> 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.
>
> The lemmas you need aren't too bad, but trying to prove
> (implies (and (posp n) (integerp x))
>         (equal (+ (floor x n) (ceiling x (- 1 (/ 1 n))))
>                x))
> [or something like it, that lemma is on my home computer]
> then with arithmetic-5, you get a rewriting loop. Automated math is hard.
>
> -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
>>
>
>