[TYPES] Permutation of beta-redexes in lambda-calculus
Laurent Regnier
regnier at iml.univ-mrs.fr
Fri Nov 16 10:33:02 EST 2007
Hello,
> This [notion of redex permutation] has been developed by
> Laurent Regnier in 1990 [1]. He calls it \sigma reduction and is
> formulated as follows:
>
> ((\x.U) V) W --> (\x.(U W)) V (x\notin W)
> (\x.\y.U) V --> \y.(\x.U) V (y\notin V)
Thanks to Eduardo for mentioning this work. I should say that other
people had already some work on it, eg it is used (and maybe defined
for the first time) in an 87 de Vrijer paper (Exactly estimating
functionals and strong normalization).
On the other hand I have never heard of the CBV version that Stéphane
proposes.
Bests,
Laurent
More information about the Types-list
mailing list