The Complexity of Subtype Entailment for Simple Types

A subtyping 0 is entailed by a set of subtyping constraints C, written C j= 0, if every valuation (mapping of type variables to ground types) that satisfies C also satisfies 0. We study the complexity of subtype entailment for simple types over lattices of base types. We show that: deciding C j= 0 is coNP-complete. deciding C j= 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 complexitytheoretic marker on the intuitive “exponential explosion” in the algorithm. Central to our results is a novel characterization of C j= for atomic, consistent C. This is the basis for correctness ...

• Type: Conference
• Year: 1997
• Where: LICS
• Authors: Fritz Henglein, Jakob Rehof
• Keywords: Automated Reasoning, Base Types, Entailment, LICS 1997, Subtype Entailment