Paper: The complexity of subtype entailment for simple types (at LICS 1997)
Authors: Fritz Henglein Jakob RehofAbstract
A subtyping /spl tau//spl les//spl tau/' is entailed by a set of subtyping constraints C, written C |=/spl tau//spl les//spl tau/', if every valuation (mapping of type variables to ground types) that satisfies C also satisfies /spl tau//spl les//spl tau/'. We study the complexity of subtype entailment for simple types over lattices of base types. We show that: deciding C |=/spl tau//spl les//spl tau/' is coNP-complete; deciding C |=/spl alpha//spl les//spl beta/ for consistent, atomic C and /spl alpha/, /spl beta/ 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 |=/spl alpha//spl les//spl beta/ for atomic, consistent C. This is the basis for correctness of the linear-time algorithm as well as a complete axiomatization of C |=/spl alpha//spl les//spl beta/ 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.
BibTeX
@InProceedings{HengleinRehof-Thecomplexityofsubt, author = {Fritz Henglein and Jakob Rehof}, title = {The complexity of subtype entailment for simple types}, booktitle = {Proceedings of the Twelfth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1997}, year = 1997, editor = {Glynn Winskel}, month = {June}, pages = {352--361}, location = {Warsaw, Poland}, publisher = {IEEE Computer Society Press} }