[Prev][Next][Index][Thread]
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.
Enjoy.
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
------------------------------------------------------------------------------