[plt-scheme] redex: syntactic equality

From: Eric Tanter (etanter at dcc.uchile.cl)
Date: Mon Oct 12 09:16:28 EDT 2009

ok, will try that next time ;)

(for now I'm fine with the tag solution)

-- Éric

On Oct 12, 2009, at 7:14 AM, Robby Findler wrote:

> 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

Posted on the users mailing list.