language: en

The Undecidability of Mitchell's Subtyping Relationship

J. B. Wells
jbw@cs.bu.edu
Dept. of Computer Science Boston University
Boston, MA 02215, U.S.A.
December 10, 1995

Abstract Mitchell defined and axiomatized a subtyping relationship (also known as containment, coercibility, or subsumption) over the types of System F (with "!" and "8"). This subtyping relationship is quite simple and does not involve bounded quantification. Tiuryn and Urzyczyn quite recently proved this subtyping relationship to be undecidable. This paper supplies a new undecidability proof for this subtyping relationship. First, a new syntax-directed axiomatization of the subtyping relationship is defined. Then, this axiomatization is used to prove a reduction from the undecidable problem of semi-unification to subtyping. The undecidability of subtyping implies the undecidability of type checking for System F extended with Mitchell's subtyping, also known as "F plus eta".

1 Introduction