[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