Compositional and Effectful Recursive Specification Formats : Distributive Laws and the Semantics of Recursion

Schwencke, Daniel

Recursive specifications are a powerful tool mainly used in mathematics and computer science. In the last decade, it was observed that many of them form coalgebras for a functor. A category theoretic approach to these specifications was developed. Our thesis carries this line of research further in two different directions by combining it with distributive laws. First, we consider distributive laws of algebra functors over coalgebra functors. As shown by Bartels (based on results by Turi and Plotkin), these define algebraic operations on the final coalgebra. We present several formats of recursive specifications (both recursive equations and recursive program schemes) which make use of operations defined that way. Following the category theoretic approach to recursive specifications, we obtain compositionality results for our specification formats. We demonstrate our results on five important special cases and show e.g. that Milner's solution theorem for his calculus of communicating systems (CCS) follows from our work. We also obtain a proof that Rutten's behavioral differential equations for the specification of operations on streams can be used in a step-by-step manner. Second, we consider distributive laws of algebra functors over certain monads. The monads model computational effects in the sense of Moggi's work, e.g. nondeterminism, and the distributive laws extend algebraic operations to cope with computational effects. Adapting Milius' completely iterative algebras to our setting, we introduce two notions of algebras with effects in which systems of recursive equations have unique solutions. Looking at three particular effects, we characterize partial, nondeterministic and composite such algebras. Finally we introduce the notion of a recursive program scheme with effects for five concrete effects and prove that all the guarded schemes have a unique or at least a canonical uninterpreted solution. For nonempty nondeterministic schemes, we compare our category theoretic approach with the classical one by Arnold and Nivat.

Rekursive Spezifikationen sind ein leistungsstarkes Werkzeug, das vor allem in der Mathematik und Informatik genutzt wird. Im Laufe der letzten etwa zehn Jahre wurde entdeckt, dass viele von ihnen Koalgebren für einen Funktor darstellen. Ein kategorientheoretischer Ansatz für solche Spezifikationen wurde entwickelt. Die vorliegende Arbeit erweitert diese Forschung in zwei verschiedene Richtungen, indem sie sie mit Distributivgesetzen kombiniert. Erstens werden Distributivgesetze eines Algebra-Funktors über einem Koalgebra-Funktor betrachtet. Bartels zeigte (aufbauend auf Ergebnisse von Turi und Plotkin), dass solche Distributivgesetze algebraische Operationen auf finalen Koalgebren definieren. In der vorliegenden Arbeit werden verschiedene Formate rekursiver Spezifikationen (sowohl rekursive Gleichungen als auch rekursive Programmschemata) präsentiert, in denen Operationen verwendet werden, die auf diese Weise definiert wurden. Indem der kategorientheoretische Ansatz für rekursive Spezifikationen verwendet wird, kann gezeigt werden, dass die Spezifikationsformate die Eigenschaft der Kompositionalität besitzen. Die Ergebnisse werden anhand von fünf wichtigen Spezialfällen illustriert. Beispielsweise wird gezeigt, dass Milners Lösungssatz für sein Prozess-Kalkül CCS aus den Ergebnissen folgt. Als weiteres Beispiel wird bewiesen, dass Ruttens behavioral differential equations auch schrittweise für die Spezifikation von Operationen auf Streams verwendet werden können. Zweitens werden Distributivgesetze von Algebra-Funktoren über verschiedenen Monaden betrachtet. Die Monaden modellieren Berechnungseffekte im Sinne der Arbeiten von Moggi, z.B. Nichtdeterminismus, und die Distributivgesetze erweitern algebraische Operationen so, dass sie Berechnungseffekte verarbeiten können. Milius' vollständig iterative Algebren werden für die Arbeit mit Berechnungseffekten adaptiert und zwei Arten von Algebren mit Berechnungseffekten eingeführt, in denen Systeme rekursiver Gleichungen eindeutige Lösungen haben. Es werden drei konkrete Effekte betrachtet und partielle, nichtdeterministische und zusammengesetzte solche Algebren charakterisiert. Schließlich wird der Begriff eines rekursiven Programmschemas mit Effekten für fünf verschiedene Effekte eingeführt und bewiesen, dass all diese Schemata, falls sie die Guardedness-Eigenschaft haben, eine eindeutige oder zumindest eine kanonische uninterpretierte Lösung besitzen. Für nichtleere nichtdeterministische Schemata wird der gewählte kategorientheoretische Ansatz mit dem klassischen Ansatz von Arnold und Nivat verglichen.

Citation style:

Total: