Charakterisierung nicht-struktureller Untertyp-Subsumption in der
Automaten-Theorie
Entscheidbarkeit von nicht-struktureller Untertyp-Subsumption (NSSE) ist
ein offenes Problem aus der theoretischen Informatik. Es wurde von Remy
und Pottier (ICFP96) im Kontext von Typinferenz für moderne
Programmiersprachen aufgeworfen, und seitdem vielfach untersucht
(Henglein, Rehof, Sue, Aiken, etc).
In diesem Vortrag charakterisiere ich NSSE erstmals durch reguläre
Ausdrücke und Wortgleichungen. Wortgleichungen sind bekannterweise
schwer zu lösen, da sie nicht-reguläre Sprachen beschreiben können. Die
neue Charakterisierung zeigt somit zum erstenmal, warum NSSE so schwer
ist: Es liegt an impliziten Wortgleichungen, die meine Charakterisierung
explizit macht. Ich hoffe, dass sich die Entscheidbarkeit von NSSE mit
Resultaten über Wortgleichungen zeigen lässt.
Spezielle Vorkenntnisse im Bereich der Unifikations- und Typ-Theorie
setze ich nicht voraus.
Alle InteressentInnen sind zu dem Vortrag herzlich eingeladen.