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

[eduardo@sol.lifia.info.unlp.edu.ar]

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.  
Instead of permuting this configuration

         @
        / \
           @
          / \

     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.