Algebraische Strukturen und Fixpunktoperationen in der Informatik

Die Semantiken der Rekursion und der Iteration werden in der Informatik üblicherweise durch Fixpunkte von Funktionen, Funktoren oder anderen Konstruktoren beschrieben. Wir haben vor, Eigenschaften, die durch Gleichungen definiert werden können, mittels Fixpunktoperationen in Halbringen, Halbmodulen und allgemeiner, in Lawvere oder cartesianischen Theorien zu untersuchen. Es wurde gezeigt, daß alle vernünftigen cartesianischen Fixpunktmodelle der Informatik genau die Identitäten der Iterationstheorien erfüllen. Wir wollen klären, ob sich die Axiome der Iterationstheorien vereinfachen lassen; vielleicht unter Zuhilfenahme anderer Operationen, die etwa zu additiven Strukturen führen. So könnte das Problem auf entsprechende Fragen in Iterationshalbringen und Iterationshalbring halbmodulpaaren, in welchen lineare Gleichungen kanonische Lösungen besitzen, führen. Eine weitere Frage betrifft die Anwendung der Iterationstheorien, der Iterationshalbringe und der Halbring Halbmodulpaare auf Axiomatisierungsprobleme in der Informatik. In vielen Gebieten der Theoretischen Informatik ist das Auffinden vollständiger Axiomatisierungen (erster Ordnung) ein äußerst wichtiges Problem. Für das Auffinden geeigneter Axiome für das sequentielle und parallele Verhalten von Transitionssystemen, Flußdiagrammen, regulären Sprachen über endlichen und unendlichen Wörtern, Baumsprachen, dynamischer Logik, "action logic" und weiteren Strukturen und Theorien ist ein gewaltiger Aufwand getrieben worden. Da alle diese Strukturen und Theorien Fixpunktoperationen enthalten, würde das vorgeschlagene Projekt zu einfacheren und besseren Axiomen für diese führen. Viele Anwendungen der Informatik gründen auf Spezifikationen, welche wiederum auf rekursive Definitionen führen. In weiten Teilen der Informatik ist man damit beschäftigt, Spezifikationen oder Transformationen von Spezifikationen auf gleichen oder verschiedenen Abstraktionsniveaus zu finden. Das vorgeschlagene Projekt würde es ermöglichen, effiziente Methoden zu entwickeln, um Spezifikationen in einfachere äquivalente Spezifikationen unter allgemeinen und speziellen Rahmenbedingungen zu transformieren.

Wie bei algebraischen Strukturen nicht anders zu erwarten wurden hauptsächlich einerseits algebraische Systeme und omega - algebraische Systeme und andrerseits Kellerautomaten und omega -- Kellerautomaten betrachtet. In der Arbeit "Weighted simple reset pushdown automata" werden die namensgebenden Kellerautomaten eingeführt. Sie verfügen über keine epsilon -- Transitionen und haben für die Veränderung des Kellers in einem Schritt nur folgende Möglichkeiten: 1. Lesen und gleichzeitig Löschen des obersten Kellersymbols. 2. In den Keller ein Symbol als oberstes Kellersymbol hineinschreiben. 3. Den Keller unverändert lassen. Das Hauptresultat dieser Arbeit ist, daß jede algebraische Potenzreihe als Verhalten eines solchen Kellerautomaten dargestellt werden kann. In der Arbeit "Greibach Normal Form for omega-Algebraic Systems and Weighted Simple omega-Pushdown Automata" wird dieses Resultat auf omega-algebraische Potenzreihen und omega-Kellerautomaten verallgemeinert. In der Theorie der Formalen Sprachen und Automaten ist die Triple Construction" wohlbekannt und wird in jeder einschlägigen Vorlesung behandelt. Es handelt sich dabei um die Konstruktion einer äquivalenten kontext -- freien Grammatik aus einem gegebenen Kellerautomaten. In der Monographie Semirings, Automata, Languages" von Arto Salomaa und Werner Kuich wird diese Konstruktion auf algebraische Potenzreihen und gewichtete Kellerautomaten verallgemeinert. Mit Hilfe des dort entwickelten Apparates und weiterer Überlegungen wird die "Triple Construction" in der Arbeit "The Triple-Pair Construction for Weighted omega-Pushdown Automata" in eine andere Richtung durch die "Triple Pair Construction" verallgemeinert. Dabei handelt es sich um die Konstruktion einer äquivalenten gemischten kontext -- freien Grammatik aus einem gegebenen omega -- Kellerautomaten, wobei eine kontextfreie Grammatik durch endlichen Ableitungen wie üblich endliche Wörter erzeugt und durch unendliche Ableitungen unendliche Wörter erzeugt.