The complexity of subtype entailment for simple types

A subtyping τ⩽τ´ is entailed by a set of subtyping constraints C, written C |=τ⩽τ´, if every valuation (mapping of type variables to ground types) that satisfies C also satisfies τ⩽τ´. We study the complexity of subtype entailment for simple types over lattices of base types. We show that: deciding C |=τ⩽τ´ is coNP-complete; deciding C |=α⩽β for consistent, atomic C and α, β atomic can be done in linear time. The structural lower (coNP-hardness) and upper (membership in coNP) bounds as well as the optimal algorithm for atomic entailment are new. The coNP-hardness result indicates that entailment is strictly harder than satisfiability, which is known to be in PTIME for lattices of base types. The proof of coNP-completeness gives an improved algorithm for deciding entailment and puts a precise complexity-theoretic marker on the intuitive “exponential explosion” in the algorithm. Central to our results is a novel characterization of C |=α⩽β for atomic, consistent C. This is the basis for correctness of the linear-time algorithm as well as a complete axiomatization of C |=α⩽β for atomic C by extending the usual proof rules for subtype inference. It also incorporates the fundamental insight for understanding the structural complexity bounds in the general case