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