[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.