[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Avoiding variable clashes
From: |
Andy Wingo |
Subject: |
Re: Avoiding variable clashes |
Date: |
Wed, 13 Apr 2011 17:27:45 +0200 |
User-agent: |
Gnus/5.13 (Gnus v5.13) Emacs/23.2 (gnu/linux) |
On Wed 13 Apr 2011 16:34, Hans Aberg <address@hidden> 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/
- Avoiding variable clashes, Hans Aberg, 2011/04/13
- Re: Avoiding variable clashes, Andy Wingo, 2011/04/13
- Re: Avoiding variable clashes, Hans Aberg, 2011/04/13
- Re: Avoiding variable clashes, Andy Wingo, 2011/04/13
- Re: Avoiding variable clashes, Hans Aberg, 2011/04/13
- Re: Avoiding variable clashes, Noah Lavine, 2011/04/13
- Re: Avoiding variable clashes, Andy Wingo, 2011/04/14
- Re: Avoiding variable clashes, Noah Lavine, 2011/04/14
- Re: Avoiding variable clashes, Andy Wingo, 2011/04/14
- Re: Avoiding variable clashes, Hans Aberg, 2011/04/14