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.


Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: