Skip navigation

[This post is by Frank Fu.] I have recently written up a note with a reducibility proof for call-by-value (CBV) System F.
You can get one from my website: http://www.cs.uiowa.edu/~pfu/

This may be useful for those interested in how one shows termination of System F by the reducibility method.

My note is based on Girard’s proof, showing strong normalization for System F with full beta-reduction. Here are the differences between this version of proof and Girard’s proof:

0. Restrict on CBV closed terms.

1. Eleminate the types at the term level, so the interpretation of the universal abstract type reflects a notion of ’intersection type’.

2. Reducible terms are not assumed to be typable.

3. Add a constant to the term to construct inactive terms, which makes the reducibility set to be non-empty.

4. Comments from Prof. Stump: The interpretation of every type is required to be non-empty is not flexible enough for some of the type theories we are interested in, since certain types really are expected to have empty interpretations (for example, equality types
like 0 = 1). Still, I think it was an excellent exercise to explore
this approach, and to discover what it can handle and what it cannot.

Advertisements

### 2 Comments

1. I was also thinking about this lately. This is the version that I came up with:

CR1 : if t in R, then t normalizes to a value.
CR2 : if t ~> t’, then (t in R iff t’ in R).

And then define RED by

t in RED phi X ==
t in phi(X)
t in RED phi (T1 -> T2) ==
t normalizes and
forall t’ in RED phi T1,
(t t’) in RED phi T2
t in RED phi (Forall X. T) ==
forall R in CR,
t in RED (phi, R/X) T

In other words, the difference to your relation is that in the arrow case I explicitly postulate that the term normalizes (like Pierce’s proof in TaPL).

This also seems to work, and avoids having to force all the RED-sets to be nonempty.

2. Vilhelm,
Thanks for sharing your thoughts. I agree
with you that your version should also be working as well and without showing the non-empty.

And just as Prof. Stump said, in some cases, we really need to let the reducibility set to be empty–[|0=1|]. Thus your version has the ability to analyze this sort of system, which is really good.

And to be honest, I still not sure what we really gain to have a nonempty interpretation for every types.