[plt-scheme] redex: syntactic equality
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
>>