[This post is by Adam Procter.] Last week’s graduate seminar discussions focused on Peng (Frank) Fu’s proof of termination for the call-by-value simply-typed -calculus, which Aaron has written about previously. Frank’s proof is derived from that given for strong normalization with full -reduction in [Girard 1989]. (Later in the same book, Girard extends this proof to full System F.) The difference is that Frank’s proof is specific to the call-by-value calculus. This raises an obvious question: what need is there for a CBV-specific proof? Clearly, full -reduction subsumes CBV — and since full -reduction is strongly normalizing, why don’t we just point out that the set of transition sequences allowed under CBV is a subset of those allowed under full -reduction and call it a day? The answer is that if a CBV-specific proof for the pure -calculus reveals simplifications that can be made to the proof, these same simplifications might help us in constructing normalization proofs for richer languages under CBV reduction. I’ll say more about that below.
Let’s begin with a brief summary of the proof technique. Let’s say we define the set of -terms in the usual way (with or without constants), and define the set of types inductively as (say) a set of base types , and the set of function types . Then with each type we associate a so-called reducibility set, denoted . The reducibility sets are defined in such a way as to preserve the critical property that all terms in are normalizable. We then prove that for every type , all terms of type are in ; therefore every well-typed term is in some reducibility set, and since every term in a reducibility set is normalizable, it follows that all well-typed terms terminate.
All this may seem straightforward, but on close inspection there is an interesting wrinkle: to say that has type is not the same thing as saying that ! Indeed, the relationship of a type to its reducibility set is the trickiest part of this proof strategy. In order for the strategy to work, reducibility sets must be defined carefully in order to preserve the properties we are trying to prove! [Pierce 2002] explains:
If we want to prove some property of all closed terms of [base] type , we proceed by proving, by induction on types, that all terms of type possess property , all terms of type preserve property , all terms of type preserve the property of preserving property , and so on. We do this by defining a family of predicates indexed by types.
This technique, owing to [Tait 1967], is known as the logical relations technique. The “predicates” that Pierce refers to correspond to our reducibility sets.
Returning to Frank’s proof, we’ll define reducability sets for our purposes as follows:
- iff and is closed.
- iff for every , .
From these definitions (and again, assuming a call-by-value evaluation strategy), we can prove four critical properties:
- (CR 1) If , then and is closed.
- (CR 2) If and , then .
- (CR 3) If is a closed term, and , then .
- (CR 4) is a non-empty set.
The final step of the proof shows that every well-typed term is in some reducibility set (specifically that associated with its type). This is shown by induction on the structure of typing derivations. From this result, along with CR 1, it follows that all well-typed terms terminate.
At the beginning of this post, I alluded to the possibility of a CBV-specific proof being simpler than a proof for full -reduction. First it is worth noting that unlike Girard’s proof, Frank’s proof does not require to be of type in order to be in .
Second, let’s compare CR 3 to its counterpart from Girard’s proof:
- (CR 3) [Fu] If is a closed term, and , then .
- (CR 3′) [Girard] If is neutral, and whenever we convert a redex of we obtain a term , then .
Wait… “neutral”? What does that mean? Well, as it turns out, it means that the term is not an abstraction, i.e. it is of either of the forms or . It turns out that this stipulation is needed because under full -reduction, we can perform -reduction inside an abstraction; CBV does not allow this. So we have to reason with extra care about abstraction terms — they simply are not “covered” by CR 3′. (In Girard’s proof, this extra step takes the form of a lemma stating that if for all reducible of type , is reducible, then so is .) In Frank’s proof, by contrast, this extra step is not required (though the inductive step for proving CR 1 on function types is somewhat similar), as CR 3 applies to all closed terms.
A final (and perhaps slightly tangential) point, courtesy of Chris Casinghino in a comment on Frank’s original writeup: [Pierce 2002] also gives a proof of normalization for CBV. However, Pierce’s definition of the reducibility set takes a different form. Paraphrasing to keep things in line with our notation:
- iff halts.
- iff halts and for every , .
In other words, the inductive step for application insists that the function term be terminating. Frank’s proof does not contain this side condition. This may not seem like a big deal, but Chris points out that the addition of the side condition makes it trickier to use in a framework of logical relations like that given in [Mitchell 1996]. Chris is working on a formalization of just such a framework that disallows such side conditions, so the absence of the side condition may be very helpful.
In a future post, and as an exercise for my own amusement/education, I hope to adapt Frank’s proof to call-by-name evaluation. It’ll be interesting to see how much this change complicates things, if at all. My hunch is that the CBN proof should be similar in structure, since CBN evaluation is deterministic (like CBV but unlike full -reduction). Stay tuned!
- Girard, J., Taylor, P., and Lafont, Y. 1989. Proofs and Types. Cambridge University Press.
- Mitchell, J. C. 1996. Foundatioins for Programming Languages. MIT Press.
- Pierce, B. C. 2002. Types and Programming Languages. MIT Press.
- Tait, W. W. 1967. Intensional interpretation of functionals of finite type I. Journal of Symbolic Logic 32, 198-212.