The undecidability of Mitchell's subtyping relationship
OA Version
Citation
Wells, J.B.. "The Undecidability of Mitchell's Subtyping Relationship“, Technical Report BUCS-1995-019, Computer Science Department, Boston University, December 10, 1995. [Available from: http://hdl.handle.net/2144/1578]
Abstract
Mitchell defined and axiomatized a subtyping relationship (also known as containment, coercibility, or subsumption) over the types of System F (with "→" and "∀"). 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".