> The beta rule is in denotational semantics something like > ((lambda x . E_1) E_2) => [E_2/x]E_1, E_2 free for x in in E_1 > where [E_2/x]E_1 means substituting all free occurrences of x with E_2. > > In addition, one has the alpha rule > (lambda x . E) => (lambda y . [y/x]E), y free for x in E > > Now, if one would want to implement say a quantifier 'forall', one would > still need the alpha rule, and substitution, but instead of the beta rule have > (forall x . E) => [t/x]E, t free for x in E > where t is any term. One would have to write additional stuff to manipulate > it. But the alpha rule is tricky to implement. > > The generalization would be to admit defining operators b satisfying the > alpha rule > (b x . E) => (b y . [y/x]E), y free for x in E > where one can add additional evaluation rules.
I believe you can implement all of that with the mechanisms of environments and gensyms. However, let me give a slightly different perspective on it, which is how I have come to think of these things: First, the alpha rule: the expressions (lambda (x) (+ x 1)) and (lambda (y) (+ y 1)) are equivalent by the alpha rule, because we have merely changed the name of a thing. The environment perspective is that you shouldn't think of 'x and 'y as variables at all. Instead, think that in the first expression the symbol 'x refers to some ideal "variable" object, which represents one "slot" where a value can exist. In the second expression, 'y refers to the same sort of object. Every different slot that can be referred to has a different one of these variable objects, so substituting one for another is pointless - there will never be a name conflict. For instance, the following expression has two "variable" objects, even though there is only one symbol naming them: (lambda (x) (lambda (x) (+ x 1))) We use environments to essentially replace symbols by the appropriate "variable" objects as soon as we see the symbols, so the rest of the compiler code never has to worry about one symbol naming two different things, or other weird cases like that. The fact that we represent different variables as gensyms is an implementation detail, and unimportant. (In fact, I might like to change that detail at some point to get better error messages, but it's not high on my to-do list.) Does this make sense to you? Noah
