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 <address@hidden> 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
>
>
>
>