On Wed 13 Apr 2011 16:34, Hans Aberg <haber...@telia.com> writes: > 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?
Sorry, I don't know what you mean. References? Andy -- http://wingolog.org/
