[Prev][Next][Index][Thread]
Bounded Quantification is Undecidable
Date: Tue, 23 Jul 91 15:51:04 -0400
F< (or F-sub) is a typed lambda-calculus with subtyping and bounded
second-order polymorphism. First introduced by Cardelli and Wegner,
it has been widely studied as a core calculus for type systems with
subtyping.
Curien and Ghelli proved the partial correctness of a well-known
recursive procedure for computing minimal types of F< terms and showed
that the termination of this procedure is equivalent to the
termination of its major component, a procedure for checking the
subtype relation between F< types. This procedure was also thought to
terminate on all inputs, but the discovery of a subtle bug in his
proof of this claim led Ghelli to observe, earlier this year, that
there are inputs on which the subtyping procedure diverges. This
reopened the question of the decidability of subtyping (and hence of
typechecking) for F<.
Much to my surprise, I recently settled this question in the negative by
finding a reduction from two-counter Turing machines to F< subtyping
statements such that a given two-counter machine halts iff its
encoding into F< is derivable from the rules defining the subtype
relation.
The reduction is presented in detail in a new technical report,
numbered CMU-CS-91-161, which is available from me upon request or by
anonymous FTP from any internet host as follows:
ftp proof.ergo.cs.cmu.edu [or 128.2.222.187]
login: anonymous
password: <your mail address>
binary
cd /usr/bcp/pub
get fsub.dvi.Z [or fsub.ps.Z]
-- Benjamin Pierce