[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.
http://www.era.lib.ed.ac.uk/handle/1842/778
Sam
More information about the Types-list
mailing list