[TYPES] Permutation of beta-redexes in lambda-calculus

Laurent Regnier regnier at iml.univ-mrs.fr
Fri Nov 16 10:33:02 EST 2007


 >      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


More information about the Types-list mailing list