[plt-scheme] redex: syntactic equality

Another thing you might try is systematically renaming your terms (the
first variable gets the name "x1", the second "x2", etc) and then use
equal? to compare them. That amount to implementing your own alpha
comparison, of course, but if you've gone as far as tagging lambdas,
maybe you're not that far from that function.

Robby

2009/10/12 Casey Klein <clklein at eecs.northwestern.edu>:
> 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.
>
> http://docs.plt-scheme.org/redex/Patterns.html#%28idx._%28gentag._11._%28lib._redex/redex..scrbl%29%29%29
>
> 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))
> _________________________________________________
>  For list-related administrative tasks:
>  http://list.cs.brown.edu/mailman/listinfo/plt-scheme
>