Höhere mathematische operationale Semantik

Die Beweise für Kompositionalität in höheren Sprachen sind notorious kompliziert, und allgemeine semantische Rahmenbedingungen, die Kompositionalität garantieren, sind schwer zu finden. Insbesondere das bialgebraische abstrakte GSOS-Rahmenwerk von Turi und Plotkin, das sofort einsetzbare Kompositionalitätsresultate für erste Stufen-Sprachen bereitstellt, findet bisher keine Anwendung auf höhere Sprachen. In der vorliegenden Arbeit entwickeln wir eine Theorie abstrakter GSOS-Spezifikationen für höhere Sprachen, die im Wesentlichen die Kernprinzipien von Turis und Plotkins Rahmenwerk auf eine höhere Ebene übertragen. In unserer Theorie wird die operationale Semantik höherer Sprachen durch bestimmte dinaturale Transformationen dargestellt, die wir (punktierte) GSOS-Gesetze höherer Ordnung nennen. Wir geben ein allgemeines Kompositionalitätsresultat, das für alle Systeme gilt, die auf diese Weise spezifiziert sind, und diskutieren, wie die Kompositionalität der kombinatorischen Logiken und des -Calculus in Bezug auf eine starke Variante von Abramskys anwendungsbezogener Bisimilarität als Instanzen gewonnen wird.