Rekursion in der koalgebraischen Semantik
Zusammenfassung der Projektergebnisse
Eine Programmspezifikation hat oft die Form eines rekursiven Programmschemas, d. h. eines Gleichungssystems, in dem einfachere Programme als Funktionsvariablen vorkommen. In der formalen Semantik wird die Bedeutung von Programmschemata in einer gegebenen Algebra (in der einfachere Programme schon als Funktionen interpretiert worden sind) dargestellt. Man spricht hier von einer interpretierten Semantik. Dieses Thema wurde schon in den 1970er Jahren mit algebraischen Methoden behandelt. Unser Projekt hatte als Hauptziel einen vollständig neuen, konzeptuell klaren Zugang zur Semantik von rekursiven Programmschemata. Das Projekt hat auf Vorarbeiten aufgebaut, in denen algebraische und koalgebraische Methoden erfolgreich kombiniert wurden, um die interpretierte Semantik von Programmschemata (die auf einer Klasse von Algebren als Interpretationen basiert) sowie die uninterpretierte Semantik (als unendliche Formeln) zu klären und in Zusammenhang zu bringen. Die Ergebnisse sind in den beigelegten Arbeiten formuliert. Insbesondere haben wir den von Bloom und Ésik eingeführten Begriff der Iterationstheorie von der Basiskategorie der Signaturen verallgemeinert zum Begriff der Elgot’schen Theorien. Diese liefern eine einfachere Axiomatisierung des kleinsten Fixpunktoperators in der Domaintheorie. Im Bereich von Berechnungseffekten, die durch Distributivgesetze dargestellt werden, haben wir Distributivgesetze zwischen analytischen Funktoren und kommutativen Monaden konstruiert und auf iterative Algebren angewendet. Außerdem wurden Algebren einer Base eingehend studiert. Unter anderem haben wir eine koalgebraische Konstruktion freier iterativer Algebren einer Base gefunden. Auch im Hinblick auf logische Kalküle für koalgebraische Spezifikation und für die Äquivalenz von Programmschemata wurden Fortschritte erzielt.
Projektbezogene Publikationen (Auswahl)
- Analytic functors and weak pullbacks Theory and Applications of Categories 21 (2008), 191-209
J. Adámek, J. Velebil
- Bases for parametrized iterativity Information and Computation 206 (2008), 966-1002
J. Adámek, S. Milius, J. Velebil
- Coequational logic for finitary functors Proceedings Coalgebraic Methods in Computer Science (CMCS 2008) Electronic Notes in Theoretical Computer Science 203 (2008),243-262
D. Schwencke
- A description of iterative reflections of monads Proceedings Foundations of Software Science and Computational Structures FOSSACS 2009 Lecture Notes in Theoretical Computer Science 5504 (2009), 152-166
J. Adámek, S. Milius, J. Velebil
- Elgot theories: a new perspective of iteration theories Proceedings Mathematical Foundations of Program Semantics (MFPS 2009) Electronic Notes in Theoretical Computer Science 249 (2009), 407-427
J. Adámek, S. Milius, J. Velebil
- Equational properties of recursive program scheme solutions Cahiers Topologie Gèom. Diff. Catèg. 50 (2009), 23-66
S. Milius, L. S. Moss
- Semantics of higher-order recursion schemes Proceedings Coalgebraic Methods in Computer Science (CALCO 2009) Lecture Notes in Theoretical Computer Science (2009) 5728, 34-48
J. Adámek, S. Milius, J. Velebil
- Iterative reflections of monads, in Mathematical Structures in Computer Science, published online by Cambridge University Press, February 2010
J. Adámek, S. Milius, J. Velebil
(Siehe online unter https://doi.org/10.1017/S0960129509990326)
