[Prev][Next][Index][Thread]
Subtyping for second-order types is undecidable
[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]
Dear All,
We would like to announce the availability of the following paper:
``The Subtyping Problem for Second-Order Types is Undecidable''
by Jerzy Tiuryn and Pawel Urzyczyn
Institute of Informatics, Warsaw University, Poland
-------------------------------
The paper is available by anonymous ftp from: ftp.mimuw.edu.pl
directory: /pub/users/urzy
file: sub-undec.ps.Z
or from the www page http://zls.mimuw.edu.pl/~urzy/ftp.html
Jerzy Tiuryn and Pawel Urzyczyn
==============================================================================
Abstract:
The subtyping relation for second-order polymorphic types is defined
(after Mitchell [1]) as the least quasi-order <= on polymorphic types
satisfying the following conditions (where A stands for the universal
quantifier):
1) s <= s;
2) Aa s <= s(t/a);
3) s <= Aa.s, provided a is not free in s;
4) Aa(s->t) <= Aa s -> Aa t;
5) s' <= s and t <= t' implies t->s <= t'->s';
6) s <= t implies Aa s <= Aa t;
7) s <= t and t <= u implies s <= u.
The subtyping problem is to determine for given s and t, whether
s <= t holds. We show that this problem is undecidable by a reduction
of the halting problem for two-counter automata. It follows that the
type-checking problem:
"given E, M, and t, determine whether E |- M:t holds"
is undecidable for the polymorphic (Curry-style) lambda-calculus
extended by the subsumption rule:
E |- M:t, t <= s
----------------
E |- M:s
or equivalently, by the eta-rule:
E |- M:t, M -->_eta N
---------------------
E |- N:s
[1] J.C. Mitchell, ``Polymorphic type inference and containment'',
Information and Computation, 76(2-3), 1988, 211--249.
====================================================================