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

Sam Lindley Sam.Lindley at ed.ac.uk
Fri Dec 7 12:27:22 EST 2007

Stéphane Lengrand (Work) wrote:
> 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...

I considered this problem in Section 3.2 of my thesis.



More information about the Types-list mailing list