Constraint Automata and the Complexity of Recursive Subtype Entailment

Abstract. We study entailment of structural and nonstructural recursive subtyping constraints. Constraints are formal inequalities between type expressions, interpreted over an 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 PSPACEhard, 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 these are the firs...

• Type: Conference
• Year: 1998
• Where: ICALP
• Authors: Fritz Henglein, Jakob Rehof
• Keywords: ICALP 1998, Nonstructural Subtype Entailment, Programming Languages, Recursive Subtyping Constraints, Subtype Entailment