[plt-scheme] redex: syntactic equality

From: Casey Klein (clklein at eecs.northwestern.edu)
Date: Mon Oct 12 06:15:46 EDT 2009

On Sun, Oct 11, 2009 at 11:09 PM, Eric Tanter <etanter at dcc.uchile.cl> wrote:
> You're right, in the general case there is no way for redex to know what my
> language is doing...
> Actually, what I need is comparison of lambda terms:
> I want (let ((f (lambda (x) x)) (eq? f f)) to be true in my language
> So I'm going another way that consists in tagging lambda values with a
> unique identifier, and then having comparison check this:
> eg. (lambda (x) x) --> (lambda r1234 (x) x)
> The identifier is obtained with (gensym "r").
> This is working fine, except that I realize that I don't know how to write a
> test-->> for that, because when a lambda value ends up in the store, I have
> no way to know which r__ it has.
> Is there a way to do so?

No, you can't check this with test-->>.

Try formulating the expected result as a Redex pattern and comparing
the actual result to that pattern using redex-match. Use _!_ patterns
to force tags to be distinct.


For example, if the expected result is the pair produced by λx.x and
λx.1, use this pattern:

   ((λ r_!_1 (x) x) (λ r_!_1 (x) 1))

Posted on the users mailing list.