Was macht die Denotationssemantik aus?

In einem anderen Thread definierte Andrej Bauer die Denotationssemantik als:

Die Bedeutung eines Programms hängt von der Bedeutung seiner Teile ab.

Was mich an dieser Definition stört, ist, dass sie scheinbar nicht das heraushebt, was gemeinhin als Denotationssemantik von dem, was gemeinhin als Nicht-Denotationssemantik angesehen wird, nämlich strukturelle Operationssemantik .

Genauer gesagt ist der Schlüsselbestandteil hier die Modularität oder Kompositionalität der Semantik oder anders ausgedrückt die Tatsache, dass sie gemäß der abstrakten Struktur des Programms definiert sind.

Da die meisten (alle?) Formalen Semantiken heutzutage eher strukturell sind, ist dies die erforderliche Definition?

Meine Frage lautet also: Was ist Denotationssemantik?

Die Unterscheidung, die ich persönlich zwischen denotationaler und operationeller Semantik mache, ist ungefähr so:

• Denotationssemantik ist mathematisch und gleich. Die Details der Reduktion sind weniger wichtig als das Endergebnis, was in manchen mathematischen Bereichen ein zeitloser Wert ist.
• Die operationale Semantik ist algorithmisch. Es entfaltet sich in einzelnen Zeitschritten. Der Prozess ist Teil der Bedeutung, und das Endergebnis ist nur ein besonderer Schritt in diesem Prozess.

Der Unterschied kann manchmal ziemlich subtil sein und es kann schwierig sein zu sagen, ob es sich nur um einen Unterschied in Stil oder Substanz handelt.

Wir können jedoch sehen, wie die Kompositionsdefinition von Andrej natürlicher aus der Denotationsdefinition folgt, und wir können uns auch leicht eine nicht-konfluente, nicht-kompositorische Semantik vorstellen, die immer noch der operationellen Definition entspricht.

Wenn ich mir vorstellen würde, was Dana Scott sagen würde, würde er wahrscheinlich sagen, dass die Denotationssemantik kompositorisch ist (wie von mir behauptet) und dass die Bedeutung eines Programms ein echtes mathematisches Objekt sein muss, keine syntaktische oder formalistische Einheit. Natürlich muss man in einer solchen Sichtweise zwischen formaler Manipulation der Syntax und "wahrer" Mathematik unterscheiden. Dies ist notwendigerweise eine nicht mathematische Unterscheidung.

Nachträglich möchte man vermutlich, dass die Bedeutung in dem Sinne angemessen ist, dass zwei beobachtend unterschiedliche Programme nicht die gleiche Bedeutung erhalten. Eine solche Angemessenheit hängt natürlich davon ab, was man als "Beobachtung" bezeichnet.

Aus dieser Sicht könnte argumentiert werden, dass strukturelle operative Semantik keine denotationale Semantik ist, da sie die Bedeutung einer syntaktischen Entität mit einer anderen syntaktischen Entität (einem Wert oder einer Reduktionssequenz) gleichsetzt.

Ich stimme zu, dass A. Bauers Identifikation der Denotationssemantik mit der Kompositionalität (in Büchern zur Programmiersprachensemantik ) das, was traditionell mit Denotationssemantik gemeint war, nicht wirklich gut charakterisiert, da sowohl die operationale Semantik als auch die Programmlogik (Axiomatik-Semantik) kompositionell sind .

Ich würde vorschlagen, dass der Begriff am besten soziohistorisch verstanden wird, da er sich lose auf eine bestimmte theoretische Tradition bezieht (die ernsthaft begann, als Scott ein gittertheoretisches Modell des untypisierten Lambda-Kalküls erstellte), mit bestimmten bevorzugten Werkzeugen (Ordnungstheorie, Fixpunktsätze) , Topologie, Kategorietheorie) und bevorzugte Zielsprachen (rein funktional und sequentiell). Ich stelle mir vor, dass - abgesehen von reinem intellektuellen Interesse - die Denotationssemantik hauptsächlich erfunden wurde, weil:

1. Früher war es schwierig, über die operationale Semantik nachzudenken.

2. Früher war es schwierig, nicht-trivialen Sprachen eine axiomantische Semantik zu geben.

$\pi$

Zusammenfassend würde ich also argumentieren, dass der Begriff "Denotationssemantik" ungenauer und damit weniger nützlich geworden ist. Es könnte für die Semantik-Community hilfreich sein, sich einer besseren Terminologie anzunähern.

Ich bin mit der Antwort von Adrej zufrieden, aber ich würde gerne noch näher darauf eingehen.

So starten Sie mit, denotational Semantik will etwas sagen wie „die Bedeutung dieser Notation ist , dass“. Ein echter Semantiker möchte sich vorstellen, dass die Bedeutungen das sind, was in unserem Geist existiert und die Notationen nur eine Möglichkeit sind, diese Bedeutungen auszudrücken. Daraus folgt die Anforderung, dass die Denotationssemantik kompositionell sein muss. Wenn die Bedeutungen primär und die Notationen sekundär sind, haben wir keine andere Wahl, als die Bedeutungen größerer Notationen als Funktionen der Bedeutungen ihrer Bestandteile zu definieren.

Wenn wir diesen Standpunkt akzeptieren, muss eine gute Denotationssemantik die Bedeutungen erfassen, von denen wir annehmen, dass sie wir im Kopf haben. Jede kompositorische Semantik würde nicht unbedingt in die Rechnung passen. Wenn ich eine semantische Definition für eine Komposition vorstelle und niemand zustimmt, dass darin eine Bedeutung angegeben ist, die er in seinem Kopf hat, dann nützt das wenig. Die Spielesemantik ist derzeit in dieser Situation. Es ist eine kompositorische Definition und technisch ziemlich stark, aber nur sehr wenige Menschen sind sich einig, dass es etwas mit den Bedeutungen zu tun hat, die sie im Kopf haben.

Allerdings hat jede Zusammensetzungsdefinition verschiedene technische Vorteile. Wir können es verwenden, um Äquivalenzen oder andere Eigenschaften durch Induktion auf die Syntax von Begriffen zu überprüfen. Wir können es verwenden, um die Richtigkeit von Beweissystemen zu überprüfen, indem wir wiederum die Syntax von Begriffen einführen. Wir können die Korrektheit von Compilern oder Programmanalysetechniken überprüfen (die ihrer Natur nach durch Induktion der Syntax definiert sind). Eine vollständig abstrakte semantische Definition bietet noch mehr technische Vorteile. Sie können damit zeigen, dass zwei Programme nicht gleichwertig sind, was man mit keiner beliebigen Kompositionssemantik machen kann. Eine vollständig definierbare semantische Definition ist noch besser. Hier haben die semantischen Domänen genau das, was Sie in der Programmiersprache ausdrücken können (mit einigen Vorbehalten). Sie können also die Werte in den Domänen auflisten, um zu sehen, welche Werte vorhanden sind. Dies ist mit syntaktischen Notationen nur schwer möglich. Aus all diesen Gründen punktet die Spielesemantik hervorragend.

Die Definitionen der Kompositionssemantik haben jedoch im Laufe der Jahre an Bedeutung verloren. Robin Milner und Andy Pitts haben eine Reihe von " Operational Reasoning " -Techniken entwickelt, die ausschließlich auf der Syntax basieren, aber die operationale Semantik verwenden, wo immer dies für die Erörterung des Verhaltens erforderlich ist. Diese betrieblichen Argumentationstechniken sind Low-Tech. Keine ausgefallene Mathematik. Keine unendlichen Objekte. Wir können sie Studenten beibringen und jeder kann sie benutzen. Viele Leute fragen sich, warum wir überhaupt eine Denotationssemantik brauchen. (Martin Berger ist wahrscheinlich in diesem Lager.)

Persönlich habe ich kein Problem damit, viele Werkzeuge in meinem Werkzeugkasten zu haben. Denotationstechniken können bei einigen Problemen besser und Operationstechniken bei anderen besser abschneiden. Die Forscher, die die Theorie entwickeln, könnten besser auf den einen oder anderen Ansatz abgestimmt sein. Ziemlich oft können wir die Erkenntnisse in einem Ansatz entwickeln und diese Erkenntnisse auf den anderen Ansatz übertragen. (Viele Arbeiten von Andy Pitts sind von dieser Art. Die relationale Parametrizität wurde in der denotationalen Umgebung entwickelt, aber er kann herausfinden, wie man sie als operationale Argumentation wiedergibt. Wenn ich sie mir anschaue, sage ich: "Wow, hätte ich nie dachte, das wäre möglich. "Separation Logic geht auch in diese Richtung. Steve Brookes gab einen 60-seitigen Zuverlässigkeitsnachweis für Concurrent Separation Logic unter Verwendung der Denotationssemantik.

Operative Ansätze punkten auch dann, wenn die Programmiersprachen sehr ausgefallen sind und alle Arten von Loop-Typen höherer Ordnung zur Verfügung stehen. Wir haben vielleicht keine Ahnung, wie man solche Dinge mathematisch modelliert. Oder die mathematischen Standardmodelle könnten sich unter dem Stress der Irritation als inkonsistent herausstellen. (Siehe beispielsweise "Polymorphismus ist keine Mengenlehre" von Reynolds.) Operative Ansätze, die ausschließlich auf der Syntax beruhen, können all diese mathematischen Probleme übersehen.

Ein weiterer Ansatz, der zwischen operationellen und denotationalen Ansätzen liegt, ist die Realisierbarkeit . Anstatt wie bei operativen Ansätzen mit syntaktischen Begriffen zu arbeiten, verwenden wir zum Teil eine andere Form von mathematischen Repräsentanten. Diese Repräsentanten können möglicherweise nicht als echte denotationale "Bedeutungen" bezeichnet werden, aber sie wären zumindest etwas abstrakter als syntaktische Ausdrücke. Zum Beispiel können wir für die polymorphe Lambda-Rechnung zunächst untypisierten Begriffen eine Bedeutung geben (in einigen Modellen der untypisierten Lambda-Rechnung) und sie dann als Repräsentanten ("Realisierer") verwenden, um eine Art von "operativem Denken" in kleinen Schritten durchzuführen abstraktere Ebene.

Lassen Sie es also einen gesunden Wettbewerb zwischen den Ansätzen von Denotation, Operation und Realisierbarkeit geben. Es ist kein Schaden.

Andererseits könnte es auch zu einem "ungesunden" Wettbewerb zwischen den verschiedenen Ansätzen kommen. Menschen, die mit einem Ansatz arbeiten, sind möglicherweise so eng mit diesem verbunden, dass sie den Sinn der anderen Ansätze möglicherweise nicht erkennen. Im Idealfall sollten wir alle die Stärken und Schwächen der verschiedenen Ansätze kennen und eine wissenschaftliche Einstellung zu ihnen entwickeln, auch wenn sie nicht unsere individuellen Favoriten sind.

[Noch eine Antwort. Es ist wahrscheinlich unsinnig, mehrere Antworten zusammenzutragen. Aber hey, das ist ein tiefes Problem.]

Ich habe gesagt, dass ich Andrejs Antwort zustimme, aber es scheint, dass ich nicht ganz zustimme. Da ist ein Unterschied.

Ich sagte, dass eine Denotationssemantik sagen muss: "Die Bedeutung dieser Notation ist die". Was ich damit gemeint habe, ist, dass Notationen Bedeutungen zugewiesen werden müssen, die irgendeine Form von konzeptuellen Entitäten sind, keine anderen Notationen. Im Gegensatz dazu verlangte Andrej, um Scott zu umschreiben, dass die Bedeutungen "mathematische" Objekte sein müssen. Ich glaube nicht, dass der mathematische Teil notwendig ist.

Zum Beispiel wäre es aus meiner Sicht vollkommen in Ordnung, wenn die Bedeutungen von Notationen physikalische Prozesse wären. Nachdem alle Computerprogramme Ihr Auto gebremst haben, fliegen Sie Flugzeuge, werfen Bomben ab und was nicht. Dies sind physikalische Prozesse, keine Elemente in einem mathematischen Raum. Sie können keine Bombe abwerfen, um zu sehen, ob sie jemanden tötet, und sie zurücknehmen, wenn dies nicht der Fall ist. Computerprogramme können das nicht. Aber mathematische Funktionen können. (Sie werden "Snapback" -Operationen genannt.) Es ist also keineswegs klar, dass mathematische Funktionen für Computerprogramme eine gute Bedeutung haben.

Auf der anderen Seite wissen wir noch nicht, wie wir über physikalische Prozesse abstrakt sprechen sollen. Wir könnten also tatsächlich eine mathematische Beschreibung von Prozessen verwenden, um unsere Ideen zu artikulieren. Aber diese mathematischen Beschreibungen wären genau das, "Beschreibungen". Sie sind keine Bedeutungen. Die wirklichen Bedeutungen wären nur die physikalischen Prozesse, die wir uns konzeptionell vorstellen.

In seiner Dankesrede für den SIGPLAN-Preis (der bald auf Youtube erscheinen sollte) sagte Hoare, dass ACP einen "algebraischen Ansatz", CSP einen "denotationalen Ansatz" und CCS einen "operativen Ansatz" zur Beschreibung von Prozessen verwendet. Ohad und ich saßen in der Sitzung zusammen, sahen uns an und sagten "das ist wirklich interessant". Hier wird also viel konzeptioneller Raum erkundet. Ich denke, dass eine Menge von Scotts späteren Arbeiten über Nachbarschaftssysteme und Informationssysteme usw. in der Tat der Versuch war, Funktionen als "Prozesse" irgendeiner Form zu erklären. Girards Geometrie der Interaktion und die spätere Spielesemantik sind auch Bestrebungen, Funktionen als Prozesse zu erklären. Ich würde sagen, dass die Entwicklung einer soliden Prozesstheorie der große Beitrag der Informatik zur Mathematik des 21. Jahrhunderts sein könnte. Ich würde nicht glauben, dass die Mathematik alle Antworten hat, und wir sollten versuchen, Rechenphänomene auf mathematische Konzepte zu reduzieren, um sie zu verstehen.

Was mich erstaunt, ist, wie schön das Verstecken von Informationen in Zustandsberechnungen funktioniert (Imperative Programmierung sowie Prozesskalküle), während es in mathematisch / funktionalen Formalismen umständlich und kompliziert ist. Ja, wir haben relationale Parametrizität, und es ermöglicht uns, die Grenzen mathematischer Formalismen sehr gut zu umgehen. Aber es entspricht nicht der Einfachheit und Eleganz der imperativen Programmierung. Daher glaube ich nicht, dass die mathematischen Formalismen die richtige Antwort sind, obwohl ich zugeben würde, dass sie die beste Antwort sind, die wir derzeit haben. Aber wir sollten weiter suchen. Es gibt eine schöne Theorie von Prozessen, die die traditionelle Mathematik zweifellos schlagen wird.

[Hoffentlich ist dies meine letzte Antwort auf diese Frage!]

Ohads ursprüngliche Frage war, wie sich die Denotationssemantik von der strukturellen Operationssemantik unterscheidet. Er dachte, dass beide kompositorisch waren. Eigentlich ist das falsch. Die strukturelle Betriebssemantik wird als Abfolge von Schritten angegeben. Jeder Schritt wird kompositorisch ausgedrückt (und es ist bemerkenswert, dass Plotkin die Entdeckung macht, dass dies möglich ist!), Aber das gesamte Verhalten ist nicht kompositorisch definiert. Folgendes sagt Plotkin in seiner Einleitung zum SOS-Artikel [Hervorhebung hinzugefügt]:

In der Denotationssemantik folgt man einem Ideal der Kompositionalität, bei dem die Bedeutung einer zusammengesetzten Phrase in Abhängigkeit von der Bedeutung ihrer Teile angegeben wird. Bei der operationellen Semantik wird das Verhalten einer Programmphrase betrachtet, also nur die Sammlung der Übergänge, die sie ausführen kann. Dieses Verhalten ist jedoch nicht kompositorisch, wenn es als Funktion von Programmphrasen betrachtet wird. Die Regeln geben es jedoch strukturell, dh primitiv rekursiv, in der Syntax vor; ...

Die Tatsache, dass jeder Schritt kompositorisch ausgedrückt wird, bedeutet nicht, dass das gesamte Verhalten kompositorisch ausgedrückt wird.

Es gibt einen schönen Artikel von Carl Gunter mit dem Titel Formen der semantischen Spezifikation , in dem die verschiedenen Methoden zur Spezifikation der Semantik verglichen und gegenübergestellt werden. Ein Großteil dieses Materials ist auch im ersten Kapitel seines Textes "Semantik der Programmiersprachen" wiedergegeben. Dies sollte hoffentlich das Bild klarer machen.

Noch ein Wort zur "operativen Semantik". In den Anfängen bezeichnete der Begriff "operationell" jede semantische Definition, die sich auf detaillierte Bewertungsschritte bezog. Sowohl die denotationalen Semantiker als auch die axiomatischen Befürworter sahen die "operationale" Semantik als niedrig und maschinenorientiert an. Ich denke, das beruhte wirklich auf ihrer Überzeugung, dass Beschreibungen auf höherer Ebene möglich waren. Diese Überzeugungen wurden erschüttert, sobald sie die Parallelität betrachteten. de Bakkers und Zuckers Prozesse und die Denotationssemantik der Nebenläufigkeit haben diese interessanten Passagen:

Wir werden die Methodik der Denotationssemantik anwenden. "Denotational" sollte hier mit "operational" kontrastiert werden: Die Schlüsselidee des ersteren Ansatzes besteht darin, dass Ausdrücke in einer Programmiersprache Werte in mathematischen Bereichen bezeichnen, die mit einer geeigneten Struktur ausgestattet sind, während in letzteren die Operationen die von den Sprachkonstrukten vorgeschriebenen sind modelliert durch Schritte, die von einer geeigneten abstrakten Maschine ausgeführt werden ....

Das mathematische Modell enthält verschiedene Begriffe, die, obwohl sie denotationalen Stil haben, im Geiste operativ sind [Hervorhebung hinzugefügt]. Dazu gehören das "Verlaufsmerkmal" des Begriffs "Prozess" selbst und die Verwendung sogenannter stiller Bewegungen im Umgang mit Synchronisation und Rekursion.

Hier sehen wir, wie die Autoren mit den beiden Begriffen "operativ" zu kämpfen haben, von denen einer der technische Begriff - Verhalten, das durch syntaktische Manipulationen ausgedrückt wird, und der andere der begriffliche Begriff - niedrig und detailliert ist. Plotkin und Milner ist es zu verdanken, dass sie die "operative" Semantik rehabilitiert haben, sie so hoch wie möglich gehalten haben und gezeigt haben, dass sie elegant und aufschlussreich sein kann.

Trotz alledem unterscheidet sich der operationelle Begriff des Prozesses immer noch erheblich von dem Begriff des Prozesses, den de Bakker und Hoare zusammen mit ihren Teams entwickelt haben. Und ich denke, es gibt viel Geheimnisvolles und Wunderschönes an dem Begriff des Denotationsprozesses, das noch zu verstehen ist.

Diese zusätzliche Antwort soll den Punkt verdeutlichen, dass denotationale semantische Modelle entworfen wurden, um Rechenphänomene zu "erklären". Ich werde eine Reihe von Beispielen aus der Semantik imperativer Programmiersprachen (auch "Algol-ähnliche" Sprachen genannt) geben.

Zuerst gab es das von Scott und Strachey formulierte semantische Modell. (Vgl. Gordon: Bezeichnung der Programmiersprachen - mein absoluter Favorit oder Winskels Buch.) Dieses Modell geht davon aus, dass es einen globalen Status gibt , der sich aus dem Status aller von einem Programm zugewiesenen Speicherorte zusammensetzt. Jeder Befehl wird als eine Art Funktion von globalen Zuständen zu globalen Zuständen interpretiert.

Reynolds sagte, dass es nicht die Stapeldisziplin der lokalen Variablen modelliert. Wenn ein lokaler Bereich eingegeben wird, werden seine Variablen zugewiesen und beim Verlassen des Bereichs freigegeben. Grundsätzlich stellt sich die Frage: Inwiefern sind lokale Variablen lokal? Wie erfasst die Semantik die Lokalität? Um dies zu erklären, erfand er ein Modell der Funktorkategorie. (Vgl. Reynolds: Die Essenz von Algol und Tennent: Semantik der Programmiersprachen).

Tennent wollte die in Reynolds ' Specification Logic (einer Erweiterung von Hoare Logic für Verfahren höherer Ordnung) formulierten Argumentationsprinzipien modellieren . Die Logik hat Ideen wie ausdrucksähnliche (schreibgeschützte) Berechnungen, Nichteinmischung zwischen befehlsähnlichen und ausdrucksähnlichen Berechnungen und einige Prinzipien der Datenabstraktions-Argumentation. Er verfeinerte Reynolds 'Modell der Funktorkategorie, um ein neues zu finden. Dies nennt man das "SASL" -Modell, das auch in Tennents Buch behandelt wird.

Meyer und Sieber sowie O'Hearn und Tennent stellten fest, dass keines dieser Modelle die Lokalität lokaler Variablen noch vollständig erfasst . Wenn sich zwei Implementierungen eines abstrakten Datentyps oder einer Klasse in ihren lokalen Variablen unterscheiden, sie jedoch in einer Weise manipulieren, die von außen betrachtet dasselbe Verhalten aufweist, sind sie beobachtungsgleich. Die Denotationssemantik sollte sie gleichsetzen. Um dies zu modellieren, fügten O'Hearn und Tennent einer Variante des Funktionskategoriemodells von Reynolds relationale Parametrizität hinzu.

Als ich mir das Problem gleichzeitig ansah, glaubte ich nicht an den Ansatz der Funktorkategorie. Ich fand es auch zu technisch und glaubte, dass es ein einfacheres Modell geben muss. Dies veranlasste mich, das Modell "Globaler Zustand als unnötig" zu erfinden, das eher einem CSP-Ablaufverfolgungsmodell gleicht, jedoch für eine Sprache höherer Ordnung. Als zusätzlichen Bonus erfasste dieses Modell auch die Irreversibilität der Zustandsänderung, die in den früheren Modellen nicht vorhanden war.

Mein Modell funktionierte nur für eine wohlerzogene Subsprache von Algol, genannt Syntactic Control of Interference . Abramsky und McCusker haben mein Modell um semantische Spielideen erweitert, damit es mit vollem Algol funktionieren kann. Ihr Modell erklärt also die gleichen Phänomene wie meins, nur für die größere Sprache.

In jedem Fall können wir nachweisen, dass die neuen Modelle Beobachtungsäquivalenzen (oder andere Formen logischer Formeln) erfassen, die die genannten Rechenphänomene aufweisen, die von den früheren Modellen nicht validiert wurden. Es gibt also einen sehr genauen Sinn, in dem diese Modelle Rechenphänomene "erklären".

[Alle Arbeiten, die ich hier erwähnte, sind in den Bänden "Algol-like Languages" zu finden: link and link ]