# [plt-scheme] redex is great

But don't provide a #:source argument when checking the property's
other half. Doing so guarantees that redex-check won't find a
counterexample, since by definition, the ones it will try do reduce.
On Sun, Feb 22, 2009 at 9:13 AM, Robby Findler
<robby at eecs.northwestern.edu> wrote:
>* 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
*>* _________________________________________________
*>* For list-related administrative tasks:
*>* http://list.cs.brown.edu/mailman/listinfo/plt-scheme
*>*
*>*
*