[plt-scheme] redex: syntactic equality

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?

Thanks!

-- Éric


On Oct 11, 2009, at 11:50 PM, Jay McCarthy wrote:

> I don't believe there is, because Redex would have no way of knowing
> which terms of yours are binders and are available for alpha-renaming.
> Not to mention rules like let* and letrec.
>
> Jay
>
> On Sun, Oct 11, 2009 at 8:50 PM, Eric Tanter <etanter at dcc.uchile.cl>  
> wrote:
>> Hi,
>>
>> Is there a way to compare two terms for equality (modulo alpha  
>> renaming)
>> out-of-the-box?
>> or do I have to define my own metafunction for that?
>>
>> Thanks,
>>
>> -- Éric
>>
>>
>> _________________________________________________
>>  For list-related administrative tasks:
>>  http://list.cs.brown.edu/mailman/listinfo/plt-scheme
>>
>
>
>
> -- 
> Jay McCarthy <jay at cs.byu.edu>
> Assistant Professor / Brigham Young University
> http://teammccarthy.org/jay
>
> "The glory of God is Intelligence" - D&C 93