[plt-scheme] redex is great

From: Robby Findler (robby at eecs.northwestern.edu)
Date: Sun Feb 22 10:13:26 EST 2009

That's half of the property but I expect it to be the interesting half
(that doesn't check that all non-reducing forms are normal forms).

Robby


On 2/22/09, Jos Koot <jos.koot at telefonica.net> wrote:
> You mean this?
>
> (write
>  (time
>   (redex-check cλ T
>    (lambda (t) (< (length (apply-reduction-relation reductor t)) 2))
>    #:attempts 10000
>    #:source reductor
>    #:retries 100)))
>
> cpu time: 46250 real time: 49094 gc time: 3810
> #<void>
>
> Jos
>
> ----- Original Message -----
> From: "Robby Findler" <robby at eecs.northwestern.edu>
> To: "Jos Koot" <jos.koot at telefonica.net>
> Cc: <plt-scheme at list.cs.brown.edu>
> Sent: Sunday, February 22, 2009 2:44 PM
> Subject: Re: [plt-scheme] redex is great
>
>
> On Sun, Feb 22, 2009 at 7:05 AM, Jos Koot <jos.koot at telefonica.net> wrote:
>> Hi Robby,
>> This does the job. Now
>> (term(curry((((λ(z)(z z))(λ(x y)(x(x y))))a)z)))
>> is reduced to (a(a(a(a z))) without any bifurcation.
>> May be the code should be simplified, but in this form it exposes my way
>> of
>> thinking.
>> I thought you might like to see the results of your appreciated help.
>> Thanks
>> very much.
>
> Nice.
>
> Now the thing to try to to formulate a property of this semantics and
> use redex-check to try to falsify it. I expect you'd want the property
> to be something like "each term is either a normal form or reduces to
> exactly one thing".
>
> Robby


Posted on the users mailing list.