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