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
