Domain Theory in semantics and in the theory of C*-algebras
Mathematics
Final Report Abstract
Im Zentrum des Projektes stand die mit G. D. Plotkin durchgeführte Aufgabe, semantische Modelle für Programmiersprachen im Sinne der denotationellen Semantik von D S. Scott bereitzustellen, welche das gemischte Auftreten von probabilistischem als auch gewöhnlichem Nichtdeterminismus modellieren. Wesentlicher Gesichtspunkt war es, neben einer Beschreibung der input-output Beziehung (state transformer semantics), eine äquivalente Semantik anzugeben, welche für Eigenschaften des Outputs die schwächste Vorbedingung für den Input beschreibt, welche die gewünschte Output-Eigenschaft garantiert (predicate transformer semantics). Da die Modelle gleichzeitig zufällige Auswahl nach gewissen Wahrscheinlichkeiten als auch rein nichtdeterministische Auswahl modellieren sollen, stellen sie Anforderungen, die beträchtlichen mathematischen Aufwand erforderten. Methoden der Wahrscheinlichkeitstheorie und Funktionalanalysis mußten für die Verwendung über den Scott’schen Bereichen mit ihren nicht Hausdorffschen Topologien in modifizierter Gestalt entwickelt werden. Die Arbeit an dieser Aufgabe ist nunmehr in zufriedenstellender Weise abgeschlossen. Im Rahmen des Projektes wurden auch mehrere Fragen untersucht, die in inhaltlichem Zusammenhang mit der eben genannten Arbeit stehen und einzelne Gesichtspunkte grundsätzlicher untersuchen als für den speziellen Zweck erforderlich. Auch wurde die Beziehung zu verwandten Ansätzen untersucht. Für eine einfache imperative Sprache und diskrete Zustandsräume wurden die beiden Semantiken und ihre Äquivalenz explizit ausgearbeitet. Als nicht beabsichtigter Nebeneffekt ergaben sich enge Zusammenhange der Scott’schen Bereichstheorie mit Entwicklungen in der Theorie der C*-Algebren: Die von G. A. Elliott im Jahr 2008 eingeführte topologische Anreicherung der klassischen Cuntz-Halbgruppe ist bereichstheoretischer Natur. Diese Entwicklung eröffnet neue Perspektiven.
Publications
- Mixed powerdomains for probability and nondeterminism. Logical Methods in Computer Science
Klaus Keimel, G. D. Plotkin
(See online at https://doi.org/10.23638/LMCS-13(1:2)2017) - The Cuntz semigroup and domain theory
Klaus Keimel
- Relating direct and predicate transformer partial correctness semantics for an imperative probabilisticnondeterministic language. Theoretical Computer Science 412 (2011), 2701–2713
Klaus Keimel, A. Ph. Rosenbusch and Th. Streicher
(See online at https://doi.org/10.1016/j.tcs.2010.12.029) - Locally convex cones and the Schr¨der-Simpson Theorem. Quaestiones Mathematicae 35 (2012), 353–390
Klaus Keimel
(See online at https://doi.org/10.2989/16073606.2012.725274) - On the equivalence of state transformer semantics and predicate transformer semantics. Proceedings of the Workshop Informatics and Information Technologies in Education: Theory, Practice, Didactics, Novosibirsk, vol. 1 (2012), 78–104
Klaus Keimel
- Quasicontinuous domains and the Smyth powerdomain. Electronic Notes in Theoretical Computer Science 298 (2013), 215–232
Klaus Keimel, R. Heckmann
(See online at https://doi.org/10.1016/j.entcs.2013.09.015) - Continuous lattices and completely distributive lattices. Chapter 1 (pages 5–53) in: G. Grätzer and F. Wehrung (Eds.) ’Lattice Theory: Special Topics and a Applications’ vol. I, Birkhäuser Verlag, 2014
Klaus Keimel, J. D. Lawson
(See online at https://doi.org/10.1007/978-3-319-06413-0_1) - Observationally-induced algebras in Domain Theory. Logical Methods in Computer Science 10(3:18) (2014), 1–26
Klaus Keimel, I. Battenfeld and Th. Streicher
(See online at https://doi.org/10.2168/LMCS-10(3:18)2014) - Weak topologies and compactness in asymmetric functional analysis. Topology and its Applications 185/186 (2015), 1–22
Klaus Keimel
(See online at https://doi.org/10.1016/j.topol.2015.01.015) - Weak upper topologies and duality for cones. Logical Methods in Computer Science, 11(3:21) (2015), 1–14
Klaus Keimel
(See online at https://doi.org/10.2168/LMCS-11(3:21)2015)
