%
% GENERATED FROM https://www.coli.uni-saarland.de
%    by   : anonymous
%    IP   : coli2006.lst.uni-saarland.de
%    at   : Mon, 05 Feb 2024 15:43:18 +0100 GMT
%    
% Selection : Author: Tim_Priesnitz
%




@TechReport{Niehren_Priesnitz:1999,
      AUTHOR = {Niehren, Joachim and Priesnitz, Tim},
      TITLE = {Characterizing Subtype Entailment in Automata Theory},
      YEAR = {1999},
      ADDRESS = {Saarbrücken},
      TYPE = {Technical Report},
      INSTITUTION = {Universität des Saarlandes},
      URL = {http://www.ps.uni-sb.de/Papers/abstracts/pauto.html ftp://ftp.ps.uni-sb.de/pub/papers/ProgrammingSysLab/pauto.ps.gz},
      ABSTRACT = {Subtype entailment is the entailment problem of subtype constraints for some type language. Understanding the algorithmic properties of subtype entailment is relevant to several subtype inference systems. For simple types, subtype entailment is coNP complete; when extended with recursive types it becomes PSPACE complete. Adding the least and greatest type renders subtyping non-structural. Whether non-structural subtype entailment is decidable is a prominent open problem. We characterize subtype entailment in automata theory. This yields a uniform proof method by which all known complexity results on subtype entailment in the literature can be derived. The main contribution of the paper is an equivalent characterization of non-structural subtype entailment in automata theory (by so called P-automata). On the one hand side, our characterization implies that several variants of non-structural subtype entailment are polynomial time equivalent (with or without contravariant function types or recursive types). This robustness result is new and nontrivial. On the other hand side, we believe that our characterization contributes an important and necessary step towards answering the open question on decidability of non-structural subtype entailment.},
      ANNOTE = {COLIURL : Niehren:1999:CSE.pdf Niehren:1999:CSE.ps}
}

@InProceedings{Niehren_Priesnitz:1999_1,
      AUTHOR = {Niehren, Joachim and Priesnitz, Tim},
      TITLE = {Entailment of Non-Structural Subtype Constraints},
      YEAR = {1999},
      BOOKTITLE = {Asian Computing Science Conference, December 10-12},
      NUMBER = {1742},
      PAGES = {251-265},
      SERIES = {Lecture Notes in Computer Science},
      ADDRESS = {Phuket, Thailand},
      PUBLISHER = {Springer},
      URL = {ftp://ftp.ps.uni-sb.de/pub/papers/ProgrammingSysLab/SubTypeEntailment:99.ps.gz},
      ABSTRACT = {Entailment of subtype constraints was introduced for constraint simplification in subtype inference systems. Designing an efficient algorithm for subtype entailment turned out to be surprisingly difficult. The situation was clarified by Rehof and Henglein who proved entailment of structural subtype constraints to be coNP-complete for simple types and PSPACE-complete for recursive types. For entailment of non-structural subtype constraints of both simple and recursive types they proved PSPACE-hardness and conjectured PSPACE-completeness but failed in finding a complete algorithm. In this paper, we investigate the source of complications and isolate a natural subproblem of non-structural subtype entailment that we prove PSPACE-complete. We conjecture (but this is left open) that the presented approach can be extended to the general case.},
      ANNOTE = {COLIURL : Niehren:1999:ENS.pdf Niehren:1999:ENS.ps}
}

@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}
}