here97

Fritz Henglein, Jakob Rehof. The Complexity of Subtype Entailment for Simple Type. TOPPS Report D-319 Department of Computer Science, University of Copenhagen (DIKU), January 1997.

Copyright notice:This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.

Abstract

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

Fritz Henglein
Jakob Rehof

BibTex Reference

@TechReport{here97,
Author = {Henglein, Fritz and Rehof, Jakob},
Title = {The Complexity of Subtype Entailment for Simple Type},
Institution = {Department of Computer Science, University of Copenhagen (DIKU)},
Address = {Universitetsparken 1, DK-2100 Copenhagen, Denmark},
Month = {January},
Year = {1997}
}

EndNote Reference [help]

Get EndNote Reference (.ref)