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

[Joe Wells]

"Stéphane Lengrand (Work)" <Lengrand at LIX.Polytechnique.fr> writes:

> 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.

Dear Stéphane,

A extremely similar theorem is proven in:

  A. J. Kfoury, J. B. Wells.
  New Notions of Reduction and Non-Semantic Proofs of β-Strong Normalization in Typed λ-Calculi.
  LICS 1995.

For discussion of and pointers to related work (the original
“reduction with memory” method from Klop's 1980 Ph.D. thesis, de
Groote's similar method, Regnier's work, etc.), see also this
technical report:

  A. J. Kfoury, J. B. Wells.
  Addendum to “New Notions of Reduction and Non-Semantic Proofs of β-Strong Normalization in Typed λ-Calculi”.
  Computer Science Department, Boston University, Technical Report 95-007, 1995.

See also the general result in the following paper:

  F. D. Kamareddine.
  Postponement, Conservation and Preservation of Strong Normalisation for Generalised Reduction.
  Journal of Logic and Computation, 10(5), pp. 721-738, 2000.

I hope these pointers are helpful.

-- 
Joe Wells