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

eduardo@sol.lifia.info.unlp.edu.ar eduardo at sol.lifia.info.unlp.edu.ar
Thu Nov 15 18:48:23 EST 2007

Hi Stéphane,

Although not exactly what you are looking for and at the risk
that you may very well have heard of it already, I thought I might
mention a "mirror image" notion of permutation to the one you suggest.

@
/ \
@
/ \

you permute this other one

@
/ \
@
/ \

This 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)

He proves that all \sigma-equivalent terms have the same longest
(beta) reduction to normal form. As a consequence \sigma-reduction is
perpetual. Also, you get a result corresponding to your theorem as a
corollary.

Regards,
E.

[1] Regnier, 1990, Une équivalence sur les lambda-termes, paru dans
TCS 126 (1994).

Quoting "Stéphane Lengrand (Work)" <Lengrand at lix.polytechnique.fr>:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> Dear all,
>
> I have recently found it necessary to prove the following theorem (by a
> series of adjournment properties), and was wondering if it rings a bell
> to anyone.
>
> Definition: Let gamma be a new reduction rule of lambda-calculus defined as
> (lambda x.M) ((lambda y.N) P) ---> (lambda y.(lambda x.M) N) P
> (avoiding capture of y in M, obviously)
>
> Theorem: If M is SN for beta, then M is SN for beta+gamma.
>
> The rule comes up in my framework for a call-by-value evaluation similar
> to Moggi's lambdaC.
> I'm sure that its termination (together with beta-reduction) must have
> already come up in someone else's work...
>
> Stephane Lengrand
> lengrand at lix.polytechnique.fr
>

----------------------------------------------------------------
Este mensaje ha sido enviado utilizando IMP desde LIFIA.