[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>