Termination of system F-bounded

Announce of paper: Termination of System F-bounded (Note).

The possibility of writing non-terminating terms in typed lambda-calculi is 
strictly related to the possibility of solving ``recursive'' type equations 
such as T = T->U, or T <: T->U <: T, when subtyping is defined.

This raises the question of whether the addition of F-bounded 
quantification to system F-sub may allow non-terminating terms to be 
written. In this note we prove that this is note the case. Our proof is 
based on the computability method, and our approach is similar to the one 
used in [Mitchell 86], and, more closely, to the proof of termination of 
Fsub given in [Ghelli 90]. By the way, the proof in [Ghelli 90] is so full 
of typos, that this note may be a better read also for those which are just 
interested in Fsub termination.

One basic trick to make the proof go easy has been the choice of the set of 
rules for F-bounded. I would like to compare my formalization which someone 
else's preferred one, but I was not able to find out a complete 
formalization of F-bounded. Can somebody help me?

A postscript file F-bounded.ps.gz containing the note may be retrieved by 
anonymous ftp from site 'di.unipi.it', directory pub/ghelli. It is Mac-
produced, and I stripped font 'Times' out. If somebody will be able, or 
unable, to print it, I would like to know that.


Giorgio Ghelli.  

[Ghelli 90] G. Ghelli, "Proof Theoretic Studies about a Minimal Type System 
Integrating Inclusion and Parametric Polymorphism", PhD Thesis, TD-6/90, 
Dipartimento di Informatica dellUUniversit di Pisa, Italy, 1990.

[Mitchell 86] J.C. Mitchell, "A type-inference approach to reduction 
properties and semantics of polymorphic expressions (summary)", 11th ACM 
Conf. on Lisp and Functional Programming, 1986.

Giorgio Ghelli,    Universita' di Pisa, Dipartimento di Informatica,
                         Corso Italia 40, I-56125, Pisa, ITALY
E-mail: ghelli@di.unipi.it;  Phone: +39-50-510258;    Fax: +39-50-510226