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