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

[Laurent Regnier]

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