[TYPES] Permutation of beta-redexes in lambda-calculus
"Stéphane Lengrand (Work)"
Lengrand at LIX.Polytechnique.fr
Thu Nov 15 15:38:52 EST 2007
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
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...
lengrand at lix.polytechnique.fr
More information about the Types-list