Re: Permutation of beta-redexes in lambda-calculus

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

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.

   http://www.era.lib.ed.ac.uk/handle/1842/778

Sam