Subtype satisfiability and entailment

Abstract

Subtype constraints were introduced in advanced programming language research for designing subtype systems and program analysis algorithms. Two logical problems arise in this context: subtype satisfiability and subtype entailment. Subtype satisfiability underlies subtype inference; subtype entailment is for simplifying subtyping constraints in the same application. In this thesis, we investigate both problems systematically for a number of dialects of subtyping constraint languages that may vary in the following dimensions: types may be simple (finite) or recursive (infinite), type constants may be ordered in lattices or in general partially ordered sets, subtyping can be structural or non-structural, depending on whether least and greatest types are permitted. We use and develop new formal reasoning techniques based on automata, unification, and modal logic. Subtype satisfiability is well understood for all dialects with constants ordered in a lattice. Although cubic time algorithms are given by Palsberg and O'Keefe (1995), Pottier (1996), and Palsberg, Wand, and O'Keefe (1997), little is known about dialects where constants belong to arbitrary partially ordered sets. We present a uniform treatment to determine the complexities of all these classes. As a consequence, we settle a problem left open by Tiuryn and Wand in 1993 and also subsume complexity bounds given by Wand and Tiuryn (1993), Tiuryn (1992), and Frey (2002). Our results are based on a new connection between modal logic and subtype constraints that we present. Subtype entailment is known to be hard even for simple subtype constraint languages. Rehof and Henglein determined the complexity of structural subtype entailment with type constants ordered in a lattice. They proved coNP-completeness for simple types (1997) and PSPACE-completeness for recursive types (1998). Furthermore, they showed that non-structural subtype entailment is PSPACE-hard and is conjectured PSPACE-complete for the case with only two type constants for the least and greatest types respectively (1998). Yet the problem still remains open today. We argue that the difficulty occurs due to e ects linked to non-regular word languages. In order to do so, we precisely characterize subtype entailment by finite word automata with word equations. This characterization induces new results on non-structural subtype entailment, constituting a promising starting point for future investigation on decidability.

Diese Arbeit untersucht zwei logische Probleme der programmiersprachlichen Typinferenz: Erfüllbarkeit und Subsumption von Teiltyp-Constraints. Wir untersuchen diese Probleme systematisch für eine Reihe von Constraintsprachen. Dabei greifen wir auf Methoden der computationalen Logik, Unifikations- und Automatentheorie zurück. Teiltyp-Erfüllbarkeit ist für den Fall wohl verstanden, dass die Typkonstanten in einem Verband angeordnet sind (Palsberg und O'Keefe (1995), Pottier (1996), Palsberg, Wand und O'Keefe (1997)). Der allgemeinere Fall mit beliebig angeordneten Konstanten wurde bislang weniger untersucht. Wir stellen einen ersten universellen Ansatz vor, indem wir erstmals einen Zusammenhang zwischen Teiltyp-Constraints und Modallogik aufzeigen. Dadurch lösen wir unter Anderem ein seit 1993 offenes Komplexitätsproblem von Wand und Tiuryn. Teiltyp-Subsumption ist selbst für einfachste Constraintsprachen von hoher Komplexität. Rehof und Henglein zeigten dies für den strukturellen Verbandsfall (mit zwei Typkonstanten 1997, 1998), ließen jedoch den nicht-strukturellen Fall offen. In dieser Arbeit betrachten wir den einfachsten nicht-strukturellen Fall. Hier zeigen wir, dass versteckte Wortgleichungen neue Schwierigkeiten verursachen. Hierzu charakterisieren wir Teiltyp-Subsumption durch spezielle endliche Automaten mit Wortgleichungen. Unsere Charakterisierung liefert partielle Entscheidbarkeitsresulte zur nichtstrukturellen Teiltyp-Subsumption und kann als Grundlage für künftige Untersuchungen dienen.