Algebraic Structures and Fixed Point Operations in Computer Science

The semantics of recursion and iteration in computer science is usually captured by fixed points of functions, functors, or other constructors. We propose to study the equational properties of fixed point operations in semirings, semimodules, and more generally, in Lawvere theories, or cartesian categories. It has been shown that all reasonable cartesian fixed point models used in computer science satisfy exactly the identities of iteration theories. One of the questions of the proposed study aims at the simplification of the axioms of iteration theories, possibly in the presence of other operations, such as an additive structure, when the problem can be reduced to corresponding questions regarding iteration semirings and iteration semiring-semimodule pairs in which linear equations have canonical solutions. A second question concerns the application of of iteration theories and iteration semirings and semiring-semimodule pairs to axiomatization problems in computer science. Finding complete (first-order) axiomatizations has always been a major problem in many branches of theoretical computer science. There has been an enormous amount of effort devoted to finding appropriate axioms for the sequential and concurrent behavior of transition systems, flowchart, finitary and infinitary regular languages, tree languages, dynamic logic, action logics, and other structures and theories. Since all of these structures and and theories contain a fixed point operation, the proposed research would lead to simpler and better axioms for all of them. Most computer applications involve some form of specifications which in turn often involves recursive definitions. Computer science is to a large extent the art of specification and transformations of specifications at the same or between different levels of abstraction. The proposed research has the potential of developing efficient methods for transforming specifications into simpler equivalent specifications both in general and concrete settings.

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.