Fritz Henglein, Jakob Rehof. Constraint Automata and the Complexity of Recursive Subtype Entailment. In ICALP, Pages 616-627, July 1998.
Download paper:
Adobe portable document (pdf)
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.
We study entailment of structural and nonstructural recursive subtyping constraints. Constraints are formal inequalities between type expressions, interpreted over and ordered set of possibly infinite labeled trees. The nonstructural ordering on trees is the one introduced by Amadio and Cardelli for subtyping with recursive types. The structural ordering compares only trees with common shape. A constraint set entails an inequality if every assignment of meanings (trees) to type expressions that satisfies all the constraints also satisfies the inequality. In this paper we prove that nonstructural subtype entailment is PSPACE-hard, both for finite trees (simple types) and infinite trees (recursive types). For the structural ordering we prove that subtype entailment over infinite trees is PSPACE-complete when the order on trees is generated from a lattice of type constants. Since structural subtype entailment over finite trees has been shown to be coNP-complete, assuming coNP $\neq$ PSPACE these are the first complexity-theoretic separation results that show that, informally, nonstructural subtype entailment is harder than structural entailment, and recursive entailment is harder than nonrecursive entailment
[ icalp98 ]
[ Rectype ]
@InProceedings{here98,
Author = {Henglein, Fritz and Rehof, Jakob},
Title = {Constraint Automata and the Complexity of Recursive Subtype Entailment},
BookTitle = {ICALP},
Pages = {616--627},
Month = {July},
Year = {1998}
}
Get EndNote Reference (.ref)