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.