[plt-scheme] redex is great
Ok. I have two checks, nf1? and nf2?. If the definition of N can be trusted only nf2? is needed.
(define-metafunction bλ nf1? : T -> any
((nf1? ((L (V) T) T)) #f)
((nf1? (L (V) T)) (nf? T))
((nf1? (T_1 T_2)) ,(and (not (term (abstr? T_1))) (term (nf? T_1)) (term (nf? T_2)))))
(define-metafunction bλ nf2? : T -> any
((nf2? N) #t)
((nf2? T) #f))
(write
(time
(redex-check cλ T
(lambda (t)
(case (length (apply-reduction-relation reductor t))
((1) #t)
((0) (and (term (nf1? t)) (term (nf2? t))))
(else #f)))
#:attempts 10000
#:source reductor
#:retries 100)))
cpu time: 46375 real time: 47094 gc time: 4196
#<void>
Thanks, 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 4:13 PM
Subject: Re: [plt-scheme] redex is great
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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20090222/bbb04c2f/attachment.html>