%0 Conference Proceedings
%F here98
%A Henglein, Fritz
%A Rehof, Jakob
%T Constraint Automata and the Complexity of Recursive Subtype Entailment
%B ICALP
%P 616-627
%X 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
%U http://www.diku.dk/hjemmesider/ansatte/henglein/papers/henglein1998a.pdf
%8 July
%D 1998
%K rectype