[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Avoiding variable clashes

From: Noah Lavine
Subject: Re: Avoiding variable clashes
Date: Wed, 13 Apr 2011 21:08:21 -0400

> The beta rule is in denotational semantics something like
>  ((lambda x . E_1) E_2) => [E_2/x]E_1, E_2 free for x in in E_1
> where [E_2/x]E_1 means substituting all free occurrences of x with E_2.
> In addition, one has the alpha rule
>  (lambda x . E) => (lambda y . [y/x]E), y free for x in E
> Now, if one would want to implement say a quantifier 'forall', one would 
> still need the alpha rule, and substitution, but instead of the beta rule have
>  (forall x . E) => [t/x]E, t free for x in E
> where t is any term. One would have to write additional stuff to manipulate 
> it. But the alpha rule is tricky to implement.
> The generalization would be to admit defining operators b satisfying the 
> alpha rule
>  (b x . E) => (b y . [y/x]E), y free for x in E
> where one can add additional evaluation rules.

I believe you can implement all of that with the mechanisms of
environments and gensyms. However, let me give a slightly different
perspective on it, which is how I have come to think of these things:

First, the alpha rule: the expressions (lambda (x) (+ x 1)) and
(lambda (y) (+ y 1)) are equivalent by the alpha rule, because we have
merely changed the name of a thing.

The environment perspective is that you shouldn't think of 'x and 'y
as variables at all. Instead, think that in the first expression the
symbol 'x refers to some ideal "variable" object, which represents one
"slot" where a value can exist. In the second expression, 'y refers to
the same sort of object. Every different slot that can be referred to
has a different one of these variable objects, so substituting one for
another is pointless - there will never be a name conflict.

For instance, the following expression has two "variable" objects,
even though there is only one symbol naming them:
(lambda (x) (lambda (x) (+ x 1)))

We use environments to essentially replace symbols by the appropriate
"variable" objects as soon as we see the symbols, so the rest of the
compiler code never has to worry about one symbol naming two different
things, or other weird cases like that.

The fact that we represent different variables as gensyms is an
implementation detail, and unimportant. (In fact, I might like to
change that detail at some point to get better error messages, but
it's not high on my to-do list.)

Does this make sense to you?

reply via email to

[Prev in Thread] Current Thread [Next in Thread]