A Diagrammatic Basis for Computer Programming

1. Problemstellung und Motivation

Das Papier adressiert die Herausforderung, imperative Programme und Programlogiken (wie Hoare-Logik) auf eine systematische, algebraische und diagrammatische Weise zu modellieren. Bisherige Ansätze basieren oft auf:

• Kategorischer Logik (Lawvere): Nutzt kartesische Kategorien für Gleichungslogik, scheitert jedoch bei relationalen Theorien, da das kartesische Produkt von Mengen im Kategorie der Relationen ($Rel$) nicht das kategorische Produkt ist.
• Relationalkalkül: Bietet algebraische Grundlagen, fehlt jedoch oft an einer einheitlichen Struktur, die sowohl Datenfluss als auch Kontrollfluss (Iteration, Verzweigung) elegant vereint.
• Kleene-Algebren mit Tests (KAT): Ein mächtiges Werkzeug für imperative Programme, das jedoch oft als „Blackbox" behandelt wird und die Interaktion zwischen Datenfluss und Kontrollfluss nicht visuell oder strukturell genug abbildet.

Das zentrale Problem ist die Suche nach einer einheitlichen algebraischen Struktur, die zwei unterschiedliche monoidale Produkte vereint:

1. Ein Produkt für Datenfluss (kartesisches Produkt, $\otimes$), das Kopieren und Verwerfen von Daten erlaubt.
2. Ein Produkt für Kontrollfluss (disjunkte Vereinigung, $\oplus$), das Iteration und Verzweigung modelliert.

2. Methodik und theoretischer Rahmen

Die Autoren entwickeln einen neuen kategorischen Rahmen, der auf Rig-Kategorien (Rig Categories) aufbaut, also Kategorien mit zwei monoidalen Strukturen ($\otimes$ und $\oplus$), wobei $\otimes$ über $\oplus$ distribuiert.

Kernkonzepte:

• Kleene-Bikategorien (Kleene Bicategories):

  • Dies sind Bikategorien, die auf dem Produkt $\oplus$ (disjunkte Vereinigung) basieren.
  • Sie sind poset-verfeinert (geordnet) und tragen eine Spur (Trace), die Iteration ($\cdot^*$) ermöglicht.
  • Das Produkt $\oplus$ ist ein Biprodukt (gleichzeitig Produkt und Koprodukt).
  • Die Struktur entspricht den Axiomen von Kozen's Typed Kleene Algebren.
  • Die Spur erfüllt eine posetale Uniformitätsbedingung, die entscheidend für die Ableitung von Induktionsprinzipien ist.

• Kartesische Bikategorien (Cartesian Bicategories):

  • Basierend auf dem Produkt $\otimes$ (kartesisches Produkt).
  • Modellieren Datenfluss mit Kopierern ($\Delta$) und Dischargern ($!$).
  • Entsprechen der regulären Logik (Fragment der Prädikatenlogik mit $\exists, \land, \top$).

• Kleene-Kartesische Rig-Kategorien (kc-rig Categories):

  • Die Synthese der beiden oben genannten Strukturen in einer Rig-Kategorie.
  • Hier interagieren die kartesischen (Datenfluss) und Kleene-Strukturen (Kontrollfluss) durch spezifische Kohärenzbedingungen.
  • Eine zentrale Bedingung ist die Interaktion der Spuren: $tr_S(f) \otimes id_Z = tr_{S \otimes Z}(f \otimes id_Z)$.

Diagrammatische Notation: Tape Diagrams

Um diese komplexen Strukturen visuell darzustellen, führen die Autoren Tape Diagrams ein.

• Idee: Tape Diagrams sind verschachtelte String-Diagramme.
• Inneres Diagramm: Modelliert den Datenfluss ($\otimes$) als String-Diagramm.
• Äußeres Diagramm: Modelliert den Kontrollfluss ($\oplus$) als String-Diagramm, das die inneren Diagramme umhüllt.
• Dies ermöglicht eine zweidimensionale Darstellung von Objekten, die eigentlich Polynome in den Sorten sind, und erlaubt es, Gesetze wie die Verteilung von $\otimes$ über $\oplus$ visuell zu verstehen.

3. Hauptbeiträge

1. Definition von Kleene-Kartesischen Rig-Kategorien:
   Die Autoren definieren formal die Klasse der $kc$-Rig-Kategorien und zeigen, dass die Kategorie der Mengen und Relationen ($Rel$) mit den üblichen Operationen ein Modell dafür ist.

2. Freie Erzeugung durch Tape Diagrams:
   Sie beweisen (Theorem 7.1), dass die Kategorie der Kleene-Kartesischen Tape Diagrams ($KCT_\Sigma$) die frei erzeugte $kc$-Rig-Kategorie über einem monoidalen Signatur $\Sigma$ ist. Dies bietet eine vollständige axiomatische Basis für die Diagramme.

3. Verbindung zu Programlogiken:

   • Hoare-Logik: Die Autoren zeigen, dass die Regeln der Hoare-Logik (für partielle Korrektheit) direkte Konsequenzen der Axiome von $kc$-Rig-Kategorien sind (Proposition 9.7).
   • Andere Logiken: Das Framework ist ausdrucksstark genug, um auch andere Logiken wie Incorrectness Logic, Sufficient Incorrectness Logic und Relational Hoare Logic (RHL) zu kodieren.
   • Peano-Arithmetik: Sie formulieren die Peano-Axiome für natürliche Zahlen als $kc$-Theorie und zeigen, dass Tape Diagrams Addition und Induktion korrekt modellieren.

4. Relationaler Hoare-Logik (RHL) und Produktprogramme:
   Ein bedeutender Vorteil des Ansatzes ist die natürliche Handhabung von relationalen Eigenschaften (z. B. Non-Interference, Sicherheitsvergleiche zwischen zwei Programmen). Durch das monoidale Produkt $\otimes$ können zwei Programme zu einem „Produktprogramm" kombiniert werden, was in traditionellen Ansätzen oft aufwendig ist.

4. Ergebnisse und Beweise

• Äquivalenz zu Kleene-Algebren: Es wird bewiesen, dass jede Kleene-Bikategorie eine (typisierte) Kleene-Algebra ist (Corollary 4.12).
• Vollständigkeit der Diagramme: Die Tape Diagrams bilden die freie Kategorie. Das bedeutet, dass zwei Diagramme genau dann gleich sind, wenn sie durch die Axiome der $kc$-Rig-Kategorien ineinander überführt werden können.
• Ableitung von Hoare-Regeln: Durch die Kodierung von Programmen als Tape Diagrams (Tabelle 9) und die Anwendung der kategorischen Gesetze (z. B. Adjunktionen, Naturgesetze für Kopierer) lassen sich die Regeln für skip, assignment, sequence, if-then-else und while-Schleifen herleiten.
  • Beispiel: Die Schleifenregel wird durch die Uniformität der Spur und das Induktionsprinzip abgeleitet.
• Beispiel Peano: Die Autoren demonstrieren, dass die Addition auf natürlichen Zahlen als Tape Diagramm kodiert werden kann und die üblichen rekursiven Gleichungen ($add(0, y) = y$, $add(s(x), y) = s(add(x, y))$) durch diagrammatische Umformungen bewiesen werden können.

5. Bedeutung und Ausblick

• Einheitliche Sprache: Das Papier bietet eine „Assembly-Sprache" für Programlogiken. Statt für jede Logik neue Inferenzregeln zu erfinden, folgen diese Regeln automatisch aus der algebraischen Struktur der zugrundeliegenden Kategorie.
• Visuelle Intuition: Tape Diagrams verbinden die intuitive Vorstellung von Datenfluss- und Kontrollflussgraphen in einer einzigen, kompositionellen Notation.
• Erweiterbarkeit: Der Ansatz ist nicht auf imperative Programme beschränkt, sondern kann prinzipiell auf andere Domänen (z. B. Quantencomputing, probabilistische Programme) erweitert werden, solange diese durch Rig-Kategorien beschreibbar sind.
• Forschungsrichtung: Die Autoren schlagen vor, dass komplexe Eigenschaften wie Non-Interference nun direkt durch die Gesetze von $kc$-Rig-Kategorien bewiesen werden können, was neue Wege für die formale Verifikation eröffnet.

Zusammenfassend etablieren die Autoren eine fundamentale algebraische Basis für die Programmierung, die die Lücke zwischen kategorischer Logik, Relationenkalkül und imperativer Programmierung schließt und dabei eine mächtige, visuelle Notation (Tape Diagrams) bereitstellt, die sowohl theoretisch fundiert als auch praktisch anwendbar ist.