[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Avoiding variable clashes

From: Noah Lavine
Subject: Re: Avoiding variable clashes
Date: Wed, 13 Apr 2011 12:25:16 -0400

I think that mechanism is all that Guile uses at present. However, it
should be general enough to resolve all situations where variables of
the same name refer to different entities, assuming you set up the
environments correctly.

Are you planning on implementing a theorem prover for Guile? That would be cool.

On Wed, Apr 13, 2011 at 11:46 AM, Hans Aberg <address@hidden> wrote:
> 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:
> Hans

reply via email to

[Prev in Thread] Current Thread [Next in Thread]