[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.
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.
More information about the Types-list
mailing list