[PRL] Stooge sort - Wikipedia, the free encyclopedia
J. Ian Johnson
ianj at ccs.neu.edu
Wed Jun 22 12:48:28 EDT 2011
----- 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
>>
>> _______________________________________________
>> 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
>>
>
>
More information about the PRL
mailing list