Re: Avoiding variable clashes

[Hans Aberg]

On 14 Apr 2011, at 03:08, Noah Lavine wrote:

>> 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?

Sure. A mental image I have is thinking of it as an expression where the bound 
variable occurrences have a special type of arrow pointing back towards the 
operator that binds it. In this picture, the variable name is irrelevant. This 
is what essentially what the alpha rule says.

The problem is that it is hard to find a good implementation. Some 
implementation methods may integrate the beta rule in a way that it becomes 
hard generalize. (Combinators, for example.)

But the Guile method of merely renaming at need should not have such a problem.

Hans