[plt-scheme] redex is great

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20090222/5a52fa9c/attachment.html>