Entailment of Non-Structural Subtype Constraints
Autor: Joachim Niehren and Tim Priesnitz
Herausgeber:
Entailment of subtype constraints was introduced for
constraint simplification in subtype inference systems.
Designing an efficient algorithm for subtype entailment
turned out to be surprisingly difficult. The situation was
clarified by Rehof and Henglein who proved entailment
of structural subtype constraints to be coNP-complete for
simple types and PSPACE-complete for recursive types. For
entailment of non-structural subtype constraints of both
simple and recursive types they proved PSPACE-hardness
and conjectured PSPACE-completeness
but failed in finding a complete algorithm. In this paper,
we investigate the source of complications and isolate a
natural subproblem of non-structural subtype entailment
that we prove PSPACE-complete. We conjecture (but this
is left open) that the presented approach can be
extended to the general case.
|