It involves this paper. The more I read it the more it seems incredibly slick.

Here's the idea: (I believe this first bit is basically due to de Groot, but the authors of the present paper shifted it around a bit)

Define a notion of γ reduction that goes like

(λx.λy.M) P →

^{γ}(λy.(λx.M) P)

The key property of this is that if M →

^{γ}N and N is strongly normalising, then M is strongly normalising. That is, γ-reduction "reflects" (if I've got my terminology right --- I mean the converse of "preserves" in any event) the property of SN. Why is this? Well, consider how the thing on the left of the arrow might β-convert. It might do a little bit of work inside M, but righty could imitate that. It might do a little bit of work inside P, but righty could also simulate that. If lefty's top-level β-redex is taken, then we arrive at λy.[P/x]M, which is also immediately attainable from righty. Since we can actually get to that state by β-reducing righty, (rather than β-reducing and then γ-expanding as with the other two cases) it just

*is*SN without having to appeal to the induction hypothesis on the result of a substitution, which is always bad news.

So γ reflects SN. Now what? Well, it turns out that all terms have unique γ-canonical forms, and this isn't to tough to prove. We define another reduction relation, *-reduction, that goes like

If M has a β-redex (λx.N) P where x actually appears at least once in N (this is called a β

_{I}redex, in contrast to β

_{K}redexes, where the x doesn't appear) then we say M →

^{*}γ-nf([P/x]N).

Look what we've done: γ-reduction reflects SN, and in fact it's very easy to see that β

_{I}-reduction does too (not so for β

_{K}!) If M has

**any**reduction sequence to a *-normal form, and that *-normal form is SN, then M is SN. But wait! *-normal forms would have to have absolutely no β

_{I}redexes in them, by definition of *-reduction. In other words, a *-normal form's β-redexes are only of the kind β

_{K}. It's trivial to show such a term is SN. β

_{K}-redexes can only make the term smaller!

So we're left in a position where proving

*weak*normalization of *-reduction is sufficient to show

*strong*normalization of β-reduction. The paper does this by establishing an ω

^{ω}-order-type ordering on typed terms, but I think a hereditary substitution sort of trick could be pulled off here. I'm very excited.

Here's one more thing I noticed: the grammar of γ-normal forms can be expressed in a very similar form to the atomic-normal grammars I'm used to seeing:

R ::= R N | x | (λx.R) N

N ::= R | λx.N

The only addition to the usual grammar is the (λx.R) N: if you interpose an application between a couple of lambdas, then it's still γ-normal even if it's not β-normal.