%O Report 
%F here97
%A Henglein, Fritz
%A Rehof, Jakob
%T The Complexity of Subtype Entailment for Simple Type
%I Department of Computer Science, University of Copenhagen (DIKU)
%C Universitetsparken 1, DK-2100 Copenhagen, Denmark
%X We study the complexity of subtype entailment for simple types over lattices of base types. We show that: \begin{itemize} \item deciding \( C \models \tau \leq \tau' \) is coNP-complete. \item deciding \( C \models \alpha \leq \beta \) for consistent, atomic $C$ and $\alpha, \beta$ atomic can be done in linear time. \end{itemize} 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 shows that entailment is strictly harder than satisfiability (in contrast to for example propositional logic), which is known to be in PTIME for lattices of base types. The proof of coNP-completeness, on the other hand, 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 \models \alpha \le \beta \) for atomic, consistent $C$. This is the basis for correctness of the linear-time algorithm, and it shows how to axiomatize completely \( C \models \alpha \le \beta \) by extending the usual proof rules for subtype inference
%U http://www.diku.dk/hjemmesider/ansatte/henglein/papers/henglein1997a.pdf
%8 January
%D 1997