My student Peng (Frank) Fu has recently written up a short note (3 pages) with a reducibility proof for call-by-value (CBV) simply typed lambda calculus (STLC).   This may be useful for those interested in how one shows termination of STLC by the reducibility method.  Note that simpler methods exist for showing certainly at least (weak) normalization of STLC, but reducibility is a very useful tool for analyzing stronger systems.  Peng’s note is based on a short note (4 pages) I wrote up for one of my classes, showing strong normalization for STLC with full beta-reduction.  The restriction to CBV simplifies the proof, although it requires ensuring explicitly that terms are closed (have no free variables).  For the CBV case, a similar proof is given in Chapter 12 of Benjamin Pierce’s Types and Programming Languages book.  The main differences between Frank’s proof and the one in Chapter 12 of Pierce are that: (1) reducible terms are not assumed to be typable, and (2) an inductive definition is given for the substitutions which replace variables by reducible terms (simplifying the notation somewhat).

1. I like the way RED is defined in this proof. In particular, another difference from Pierce’s proof is that you drop his side condition that t halts from the arrow case. So, your definition of RED is more obviously a logical relation.

The cost is that we have to do a lot more work to prove (CR 1). In Pierce, this is immediate from the definition, but this proof needs two inductions. It also requires a new assumption: the beginning of the inductive case of (CR 1) assumes that RED_T is inhabited for every T.

Of course, this extra hypothesis is easy to verify here. It might be more troubling in a more complicated language. For example, imagine a proof of strong normalization for System F. Is RED_{\forall a b . a -> b} inhabited? What if we’re working in a formalization where the grammar of terms admits only well-typed terms (say by using type-indices in coq/agda/haskell)?

Of course, by proving (CR 1), you’ve really shown that adding the side condition (as in Pierce) doesn’t change the admitted terms. So, Pierce’s version is a logical relation too (in the technical sense described, for example, in John Mitchell’s book). So, was it worth doing all this extra work?

It’s hard to say. I’m working on a formalization where we syntactically rule out definitions like Pierce’s (otherwise I suppose I’d have to be able to show the side conditions don’t actually change the relation). It would go a long way, in this formalization, to find a version of the proof which doesn’t demand each RED_T is inhabited.

2. Hi, Chris.

You raise a really great point about the fact that Frank’s proof assumes that Red_T is inhabited in the inductive case for (CR 1). We missed that (I did, at least). This is actually a nontrivial assumption here, because unlike in the case of the proof from Girard that I have reworked in my note on reducibility for STLC with full beta-reduction — well, there we have all variables in Red_T for every T. But here we do not have that luxury: the members of Red_T are closed for every T.

Now what might save this from being a serious restriction is that the terms in Red_T need not have type T (in the empty context). But there is still something to prove even then: namely that Red_T is non-empty for every T.

So thanks again for your comment, and keep us updated on your formalization!

Aaron

3. Chris,

Thank you for those useful comments. Below are my opinion(May not 100% correct though)
1, I think dropping the side condition(that is, t halts) in RED_T1->T2 has nothing to do with showing the inhabited property of RED_T. If
we don’t drop this condition, we still need to assure ourselves RED_T is non-empty. Because whenever we define a method of construction, we need to make sure this method should not construct an empty set.

2. I am also recently thinking about what different would it makes when we choose drop the condition or not. I do think not dropping the condition may be a good strategy in other more complex language especially using logical relation to prove other properties. I just want to show that we “can” actually drop that condition in proving of termination in the setting of simply type. But I strongly agree with you that in other complex language, dropping a condition like that will not even work.

Again, thank you very much for your useful comments. I will make necessarily changes in my notes.

Frank