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



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 

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.