1: We consider the following rule in $\l$-calculus: 

2: $$\sigm\quad {(\l x.M)\ ((\l y.N)\ P)}\Rew{}{(\l y.(\l x.M)\ N)\ P)}$$

3: 

4: We want to prove

5: \begin{proposition}\label{prop:goal}

6: $\SN{\beta}{}\subseteq\SN{{\sigm\beta}}$.

7: \end{proposition}

8: 

9: \begin{lemma}\label{lem:sigmterm}

10: $\Rew{\sigm}$ is terminating in $\l$-calculus. 

11: \end{lemma}

12: \begin{proof}

13: Each application of the rule decreases by one the number of pairs of $\l$

14: that are not nested. 

15: \end{proof}

16: 

17: To prove Proposition~\ref{prop:goal} above, it would thus be sufficient to prove

18: that $\Rew{\sigm}$ could be adjourned with respect to $\Rew{\b}$, in

19: other words that $\co{\Rew{\sigm}}{\Rew{\b}}\subseteq

20: \co{\Rew{\b}}{\Rewn{\sigm\b}}$ (the adjournment technique leads

21: directly to the desired strong normalisation result).

22: When trying to prove the property by induction and case analysis on the

23: $\b$-reduction following the $\sigm$-reduction to be adjourned, all

24: cases allow the adjournment but one, namely:

25: $${(\l x.M)\ ((\l y.N)\ P)}\Rew{\sigm}{(\l y.(\l x.M)\ N)\ P}

26: \Rew{\b}{(\l y.\subst M x N)\ P}$$

27: 

28: Hence, we shall assume without loss of generality that the

29: $\beta$-reduction is not of the above kind. For that we need to

30: identify a sub-relation of $\b$-reduction $\gred$ such that

31: \begin{itemize}

32: \item

33: $\Rew{\sigm}$ can now be adjourned with respect to $\gred$

34: \item

35: we can justify that there is no loss of generality.

36: \end{itemize}

37: For this we give ourselves the possibility of marking $\l$-redexes and

38: forbid reductions under their (marked) bindings, so that, if in the

39: $\sigm$-reduction above we make sure that $(\l y.(\l x.M)\ N)\ P)$ is

40: marked, the problematic $\b$-reduction is forbidden.

41: 

42: Hence we use the usual notation for a marked redex $(\overline \l y.Q)\

43: P$, but we can also see it as the construct $\mlet y Q P$ of

44: \lC~\cite{Moggi:edinburgh1988} and other works on call-by-value

45: $\l$-calculus.

46: We start with a reminder about marked redexes.

47: 

48: \begin{definition}

49: The syntax of the $\l$-calculus is extended as follows:

50: $$

51: M,N::= x\sep \l x.M\sep M\ N\sep \ml x M N

52: $$

53: Reduction is given by the following system $\betiii$:

54: $$

55: \begin{array}{lll}

56: \beti&(\l x.M)\ N&\Rew{}\subst N x M\\

57: \betii&\ml x M N&\Rew{}\subst N x M

58: \end{array}

59: $$

60: 

61: The forgetful projection onto $\l$-calculus is straightforward:

62: $$

63: \begin{array}{lll}

64: \fgt{x}&\eqdef x\\

65: \fgt{\l x.M}&\eqdef \l x.\fgt{M}\\

66: \fgt{M\ N}&\eqdef \fgt M\ \fgt N\\

67: \fgt{\ml x M N}&\eqdef (\l x.\fgt M)\ \fgt N

68: \end{array}

69: $$

70: \end{definition}

71: 

72: \begin{remark}\label{rem:fgtss}

73: Clearly, $\Rew{\betiii}$ strongly simulates $\Rew{\beta}$ through $\fgtname^{-1}$ and 

74: $\Rew{\beta}$ strongly simulates $\Rew{\betiii}$ through $\fgtname$.

75: \end{remark}