On 13 Apr 2011, at 18:25, Andy Wingo wrote: >>> Sorry, I don't know what you mean. References? >> >> There is an article here: >> http://en.wikipedia.org/wiki/Variable_binding_operator > > I still don't understand. What are you trying to do?
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. Hans
