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