[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
## Re: Avoiding variable clashes

**From**: |
Hans Aberg |

**Subject**: |
Re: Avoiding variable clashes |

**Date**: |
Wed, 13 Apr 2011 18:53:26 +0200 |

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

**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**, *Hans Aberg*, `2011/04/13`
**Re: Avoiding variable clashes**, *Andy Wingo*, `2011/04/13`
**Re: Avoiding variable clashes**,
*Hans Aberg* **<=**
**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`