Avoiding variable clashes

Avoiding variable clashes

[Hans Aberg]

What method is Guile using to avoid substitution variable clashes (de Bruijn numbers, combinators, etc.)?

Hans

Re: Avoiding variable clashes

[Andy Wingo]

On Wed 13 Apr 2011 14:57, Hans Aberg <haberg-1@telia.com> writes:

> What method is Guile using to avoid substitution variable clashes (de
> Bruijn numbers, combinators, etc.)?

Each lexical variable is given a fresh name (a gensym) when it is
introduced.  The expander keeps an environment as to what name maps to
what gensym, and residualizes the gensym in the lexical reference or
assignment.

See "The Scheme Compiler" in the manual, for more.

Andy
-- 
http://wingolog.org/

Re: Avoiding variable clashes

[Hans Aberg]

On 13 Apr 2011, at 16:19, Andy Wingo wrote:

>> What method is Guile using to avoid substitution variable clashes (de
>> Bruijn numbers, combinators, etc.)?
> 
> Each lexical variable is given a fresh name (a gensym) when it is
> introduced.  The expander keeps an environment as to what name maps to
> what gensym, and residualizes the gensym in the lexical reference or
> assignment.
> 
> See "The Scheme Compiler" in the manual, for more.

I am thinking about it in the context of other types of binders, that satisfies the alpha-rule, but not the beta, useful in math (like theorem provers). Has that been discussed?

Hans

Re: Avoiding variable clashes

[Andy Wingo]

On Wed 13 Apr 2011 16:34, Hans Aberg <haberg-1@telia.com> writes:

> On 13 Apr 2011, at 16:19, Andy Wingo wrote:
>
>>> What method is Guile using to avoid substitution variable clashes (de
>>> Bruijn numbers, combinators, etc.)?
>> 
>> Each lexical variable is given a fresh name (a gensym) when it is
>> introduced.  The expander keeps an environment as to what name maps to
>> what gensym, and residualizes the gensym in the lexical reference or
>> assignment.
>> 
>> See "The Scheme Compiler" in the manual, for more.
>
> I am thinking about it in the context of other types of binders, that
> satisfies the alpha-rule, but not the beta, useful in math (like theorem
> provers). Has that been discussed?

Sorry, I don't know what you mean.  References?

Andy
-- 
http://wingolog.org/

Re: Avoiding variable clashes

[Hans Aberg]

On 13 Apr 2011, at 17:27, Andy Wingo wrote:

>>>> What method is Guile using to avoid substitution variable clashes (de
>>>> Bruijn numbers, combinators, etc.)?
>>> 
>>> Each lexical variable is given a fresh name (a gensym) when it is
>>> introduced.  The expander keeps an environment as to what name maps to
>>> what gensym, and residualizes the gensym in the lexical reference or
>>> assignment.
>>> 
>>> See "The Scheme Compiler" in the manual, for more.
>> 
>> I am thinking about it in the context of other types of binders, that
>> satisfies the alpha-rule, but not the beta, useful in math (like theorem
>> provers). Has that been discussed?
> 
> Sorry, I don't know what you mean.  References?

There is an article here:
  http://en.wikipedia.org/wiki/Variable_binding_operator

Hans

Re: Avoiding variable clashes

[Noah Lavine]

I think that mechanism is all that Guile uses at present. However, it
should be general enough to resolve all situations where variables of
the same name refer to different entities, assuming you set up the
environments correctly.

Are you planning on implementing a theorem prover for Guile? That would be cool.

On Wed, Apr 13, 2011 at 11:46 AM, Hans Aberg <haberg-1@telia.com> wrote:
> On 13 Apr 2011, at 17:27, Andy Wingo wrote:
>
>>>>> What method is Guile using to avoid substitution variable clashes (de
>>>>> Bruijn numbers, combinators, etc.)?
>>>>
>>>> Each lexical variable is given a fresh name (a gensym) when it is
>>>> introduced.  The expander keeps an environment as to what name maps to
>>>> what gensym, and residualizes the gensym in the lexical reference or
>>>> assignment.
>>>>
>>>> See "The Scheme Compiler" in the manual, for more.
>>>
>>> I am thinking about it in the context of other types of binders, that
>>> satisfies the alpha-rule, but not the beta, useful in math (like theorem
>>> provers). Has that been discussed?
>>
>> Sorry, I don't know what you mean.  References?
>
> There is an article here:
>  http://en.wikipedia.org/wiki/Variable_binding_operator
>
> Hans
>
>
>
>

Re: Avoiding variable clashes

[Hans Aberg]

On 13 Apr 2011, at 18:25, Noah Lavine wrote:

> I think that mechanism is all that Guile uses at present. However, it
> should be general enough to resolve all situations where variables of
> the same name refer to different entities, assuming you set up the
> environments correctly.
> 
> Are you planning on implementing a theorem prover for Guile? That would be cool.

Or at least having something to experiment with. From Andy's description, it seems one may merely have to disable the beta-rule.

I wrote on a theorem prover that pushed comparison of clauses into the unification, admitting unification branching, and doing breadth-first search.

The hard part was resolving variable clashes in substitution.

Hans

Re: Avoiding variable clashes

[Andy Wingo]

On Wed 13 Apr 2011 17:46, Hans Aberg <haberg-1@telia.com> writes:

>> Sorry, I don't know what you mean.  References?
>
> There is an article here:
>   http://en.wikipedia.org/wiki/Variable_binding_operator

I still don't understand.  What are you trying to do?

Andy
-- 
http://wingolog.org/

Re: Avoiding variable clashes

[Hans Aberg]

On 13 Apr 2011, at 18:25, Andy Wingo wrote:

>>> Sorry, I don't know what you mean.  References?
>> 
>> There is an article here:
>> http://en.wikipedia.org/wiki/Variable_binding_operator
> 
> I still don't understand.  What are you trying to do?

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.

Hans

Re: Avoiding variable clashes

[Noah Lavine]

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

Re: Avoiding variable clashes

[Andy Wingo]

On Thu 14 Apr 2011 03:08, Noah Lavine <noah.b.lavine@gmail.com> writes:

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

What are you referring to here?

Andy
-- 
http://wingolog.org/

Re: Avoiding variable clashes

[Noah Lavine]

>> 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.)
>
> What are you referring to here?

It's just part of my mental image of how variables work. I think of
the key idea as there being different "variable objects", or perhaps
"slots", even for variables referenced by the same symbol. We
implement that by assigning a unique gensym to each variable object, I
think, but you could assign a unique anything to each variable object
and it would work just as well. Is that an accurate picture of how
Guile works?

When I said I might like to change that, I was thinking of a thread a
while ago about how to handle top-level variables defined in macros.
It seems to me that instead of having a gensym object for each
separate variable, you might want a pair of (symbol . macro), where
symbol is the name of the variable and macro is the macro expansion it
came from. Then you could print stack traces or error messages with
information like "variable x (from the third expansion of (while)
...".

I haven't really thought through the idea much though. As I said, it's
not high on my to-do list.

Re: Avoiding variable clashes

[Andy Wingo]

On Thu 14 Apr 2011 15:13, Noah Lavine <noah.b.lavine@gmail.com> writes:

> We [assign] a unique gensym to each variable object, I think, but you
> could assign a unique anything to each variable object and it would
> work just as well. Is that an accurate picture of how Guile works?

Yes, for lexical variables.

> When I said I might like to change that, I was thinking of a thread a
> while ago about how to handle top-level variables defined in macros.

Top-level variables are different :)

Andy
-- 
http://wingolog.org/

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