@MastersThesis{Priesnitz:2000,
AUTHOR = {Priesnitz, Tim},
TITLE = {Entailment von nicht-strukturellen Teiltyp-Constraints},
YEAR = {2000},
ADDRESS = {Saarbrücken},
SCHOOL = {Universität des Saarlandes, Fachbereich Informatik},
URL = {ftp://ftp.ps.uni-sb.de/pub/papers/ProgrammingSysLab/Priesnitz-2000.ps.gz},
ABSTRACT = {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, dass 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.},
ANNOTE = {COLIURL : Priesnitz:2000:EST.pdf Priesnitz:2000:EST.ps}
}
|
