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
