Publication details

Saarland University Computer Science

Entailment von nicht-strukturellen Teiltyp-Constraints

Tim Priesnitz

Master's Thesis, Diplomarbeit. Fachbereich Informatik, Universität des Saarlandes, February 2000

Teiltyp-Entailment ist die Frage, ob eine Implikation zwischen Teiltyp-Constraints $t_1sm t_2$ gilt. Algorithmen, die diese Frage lösen, sind für die Vereinfachung von Teiltyp-Constraints relevant. Die Vereinfachung von Teiltyp-Constraints ist hingegen in contraintbasierten Typ-Sytemen dringend erforderlich. Die Komplexität von Teiltyp-Entailment hängt von der gewählten Typsprache ab; schon für ausdrucksschwache Typsprachen ist es überraschend schwierig, einen Algorithmus für Teiltyp-Entailment zu entwerfen. So ist Teiltyp-Entailment für einfache Typen coNP-vollständig und wird durch die Hinzunahme von rekursiven Typen PSPACE-vollständig. Entailment wird durch die Erweiterung um einen kleinsten und größten Typ nicht-strukturell. Henglein und Rehof haben bewiesen, daß nicht-strukturelles Teiltyp-Entailment, sowohl im einfachen wie auch im rekursiven Fall, PSPACE-schwer ist; einen vollständigen Algorithmus konnten sie allerdings nicht angeben. Es ist eine bekannte offene Frage, ob nicht-strukturelles Teiltyp-Entailment überhaupt entscheidbar ist.
Ausgehend von dieser Situation untersucht diese Arbeit, worin die Schwierigkeiten liegen. Wir isolieren ein Teilproblem von nicht-strukturellem Teiltyp-Entailment, von dem wir zeigen, daß es PSPACE-vollständig ist. Damit zeigen wir zum ersten Mal Entscheidbarkeit für ein nicht-triviales Fragment von nicht-strukturellem Entailment. Wir charakterisieren Teiltyp-Entailment in der Automaten-Theorie; dazu erweitern wir das Konzept der endlichen Automaten zu sogenannten P-Automaten, deren Eigenschaften wir systematisch analysieren. Im nächsten Schritt reduzieren wir nun Teiltyp-Entailment auf das Universalitätsproblem von eingeschränkten P-Automaten. Für unser ausgezeichnetes Fragment können wir uns in der Tat auf endliche Automaten zurückziehen, deren Universalitätsproblem PSPACE-vollständig ist.

Download PDF        Show BibTeX               


Login to edit


Legal notice, Privacy policy