[PRL] Stooge sort - Wikipedia, the free encyclopedia

[Carl Eastlund]

Here's how I'd implement stooge-sort for easy termination checking in
ACL2.  [Typed off-the-cuff, may be riddled with bugs.]

(defun take-last (n l)
  (let* ((k (len l)))
    (if (> n k)
      l
      (nthcdr (- k n) l))))

(defun stooge-sort (as)
  (cond
    ((endp as) as)
    ((endp (rest as)) as)
    (t (let* ((n (len as))
              (n*2/3 (ceiling (* n 2/3)))
              (n*1/3 (- n n*2/3))
              (bs1 (stooge-sort (take n*2/3 as)))
              (bs2 (take-last n*1/3 as))
              (bs (append bs1 bs2))
              (cs1 (take n*1/3 bs))
              (cs2 (stooge-sort (take-last n*2/3 bs)))
              (cs (append cs1 cs2))
              (ds1 (stooge-sort (take n*2/3 cs)))
              (ds2 (take-last n*1/3 cs))
              (ds (append ds1 ds2)))
         ds))))

Carl Eastlund

On Wed, Jun 22, 2011 at 12:48 PM, J. Ian Johnson <ianj at ccs.neu.edu> wrote:
>
> ----- Original Message -----
> From: "Carl Eastlund" <cce at ccs.neu.edu>
> To: "J. Ian Johnson" <ianj at ccs.neu.edu>
> Cc: "Paul A. Steckler" <steck at stecksoft.com>, "Dan Friedman" <dfried00 at gmail.com>, "PRL" <prl at lists.ccs.neu.edu>
> Sent: Wednesday, June 22, 2011 12:25:31 PM GMT -05:00 US/Canada Eastern
> Subject: Re: [PRL] Stooge sort - Wikipedia, the free encyclopedia
>
> 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.
>
> And that assumption comes in the form of my if statement. How else would you do this?
> -Ian
>
>>
>>>> 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