# No, I did not. Let me be absolutely clear, I did not do that. Except, yes, I did that.

I have a secret plan to fight inflation prove strong normalization of the simply-typed lambda calculus in twelf.

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.
Tags:
• #### (no subject)

Something that's bugged me for a long time is this: How many paths, starting at the origin, taking N steps either up, down, left or right, end up at…

• #### (no subject)

Still sad that SAC seems to end up being as complicated as it is. Surely there's some deeper duality between…

• #### (no subject)

I had already been meaning to dig into JaneSt's "Incremental" library, which bills itself as a practical implementation (in ocaml) of the ideas in…

• Post a new comment

#### Error

Anonymous comments are disabled in this journal

default userpic

• #### (no subject)

Something that's bugged me for a long time is this: How many paths, starting at the origin, taking N steps either up, down, left or right, end up at…

• #### (no subject)

Still sad that SAC seems to end up being as complicated as it is. Surely there's some deeper duality between…

• #### (no subject)

I had already been meaning to dig into JaneSt's "Incremental" library, which bills itself as a practical implementation (in ocaml) of the ideas in…