Was macht die Denotationssemantik aus?

45

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?

Ohad Kammar
quelle
4
Die Bedeutung kann in vielen Formen gegeben werden: Vor-Nach-Bedingungen, Betrieb einer abstrakten Maschine, einer mathematischen Einheit, einer Spielstrategie. In allen modernen Ansätzen werden diese Bedeutungen in Abhängigkeit von der Bedeutung der Teile angegeben.
Ohad Kammar
1
Die Frage nach der Existenz von leitete das Studium der Domänentheorie ein. Es ist aus dem Denotationsansatz hervorgegangen, definiert ihn aber nicht (zum Beispiel hat die betreffende Sprache möglicherweise nicht einmal Funktionsräume). Was die Modularität betrifft, so hat im Grunde genommen jeder moderne Ansatz zur Semantik Kompositionalität in einem geeigneten Sinne. [DD]D
Ohad Kammar
10
Ok, bitte hören Sie auf, die falsche Meinung zu verbreiten, dass die Domänentheorie initiiert oder motiviert hat, weil dies nicht der Fall war. Dana Scott wollte, dass die Domänentheorie eine mathematische Theorie ist, die für den typisierten λ- Kalkulus geeignet ist . Die Tatsache, dass es auch ein Modell des untypisierten λ- Kalküls gab, war ein Unfall . Ich weiß, er hat es mir gesagt. [DD]=D λλ
Andrej Bauer
2
[DD]=DλD[DD]D
1
Ich bin mir nicht sicher, ob das hilft, aber die Art und Weise, wie ich "aktuelle" Denotationssemantik-Arbeit sehe, ist "Zusammenstellung der Sprache in eine Kategorie" - tatsächlich könnte man Semantik in Begriffen bekannter mathematischer Objekte schreiben, ohne auf der Kategoriestruktur zu bestehen, aber das ist es eine faire Charakterisierung der spezifischen Beispiele, die ich angetroffen habe.
Gasche

Antworten:

30

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.

Marc Hamann
quelle
Ein gutes Beispiel für den Unterschied zwischen Algorithmus und Mathematik ist die Behandlung von Nichtbeendigung. Die Bezeichnung einer Schleife ist bottom, aber aufgrund des Halteproblems ist es nicht zu entscheiden, ob die Bezeichnung eines beliebigen Programms bottom ist. In der Kleinschritt-Semantik können Sie stattdessen Reduktionsschritte beobachten, aber die Theorie hat keinen "unteren" Wert. Unentscheidbarkeit und Nichtbeendigung rücken in die Metatheorie: Unentscheidbar ist, ob eine Folge von Reduktionen endet. Ebenso ist es in der Großschritt-Semantik nicht zu entscheiden, ob es eine Ableitung gibt.
Blaisorblade
23

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.

Andrej Bauer
quelle
3
Von Zeit zu Zeit wird mir gesagt, dass Übergangssysteme nicht so mathematisch sind wie Domänen, Gitter oder Ordnungen. Ich finde diese Ansicht verwirrend. Alle können in der ZFC-Mengen-Theorie ausgedrückt werden.
Martin Berger
1
Die Frage, wie genau eine bestimmte Semantik ein Computerphänomen modellieren kann, ist interessanter und hängt entscheidend vom gewählten Begriff der Beobachtung ab. Einer der Hauptvorteile der operativen Semantik (z. B. Prozesstheorie) besteht gerade darin, dass natürliche Beobachtungsbegriffe im Vergleich zur ordnungstheoretischen Semantik viel einfacher zu definieren sind.
Martin Berger
3
@Marc: Ich stimme Ihnen zu, dass Operationsmethoden die Berechnung nicht als Funktion modellieren. Aber ich verstehe nicht, warum das ordnungstheoretische Ansätze "mathematischer" macht. Von der Physik beeinflusste Mathematik wie Differentialgleichungen modellieren die Bewertungen bestimmter Systeme über die Zeit. Der Input-Output-Ansatz selbst verwendet eine rudimentäre zeitliche Struktur, nämlich dass der Output vor dem Input nicht verfügbar ist.
Martin Berger
2
@Martin: Mathematiker beklagen sich oft darüber, dass das, was Physiker tun, auch keine echte Mathematik ist. ;-) Die Physik ist zu diesem Zeitpunkt nur eine bequemer etablierte Wissenschaft. TCS ist immer noch relativ jung. Ich denke, TCS sollte sich nicht darum kümmern, Menschen in einer anderen Disziplin glücklich zu machen (egal wie sehr wir es persönlich mögen). Wir haben unser eigenes Mojo unterwegs (genau wie die Physiker).
Marc Hamann
2
@Marc: Beliebiger Müll kann in ZFC ausgedrückt werden, das ist also kein besonders verlässliches Kriterium. Semantik, in der "Funktionen" in einer Programmiersprache als Funktionen im mathematischen Sinne interpretiert werden, hat mindestens zwei Vorteile. Erstens passt es gut dazu, wie die Leute Funktionen in einer Programmiersprache sehen. Zweitens sind Funktionen vertraute mathematische Objekte, so dass es eine Menge Maschinen gibt, die man benutzen kann. Natürlich haben auch Übergangssysteme ihre Verwendung.
Andrej Bauer
19

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.

π

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.

Martin Berger
quelle
1
Um meinen letzten Beitrag zusammenzufassen, muss eine "Denotationssemantik" sagen: "Die Bedeutung dieser Notation ist die". "Operative" Semantik und "axiomatische" Semantik sind keine solchen semantischen Definitionen. Es ist irreführend, sie so erscheinen zu lassen. Beachten Sie auch, dass das, was als "operativer Ansatz" bezeichnet wird, ein Ansatz ist, um über Programme zu argumentieren. Es ist keine operationale Semantik. Der operationale Ansatz und der axiomatische Ansatz können die technischen Anwendungen der denotationalen Semantik ersetzen. Aber sie werden nicht zu denotationalen Semantiken.
Uday Reddy
LπL
1
@Martin. Warum das kompositorische Zuweisen von Prozessen nicht konkret ist. Es könnte sein, wenn Sie uns alle davon überzeugen, dass Prozesse eine fundamentale Theorie sind, genau wie Mengenlehre, und man sollte nicht nach ihrer Semantik fragen. Ich sympathisiere mit der Ansicht, dass es eine grundlegende Sprache geben könnte, die Zustandsberechnungen modelliert. Vielleicht wird irgendwann eine Art Prozesskalkül als solche Grundlage akzeptiert. Aber ich glaube nicht, dass wir schon da sind.
Uday Reddy
1
@MartinBerger Das ist das einzige, was ich jemals gelernt habe, aber es fällt mir schwer, sofort eine gute Referenz zu liefern. Zum Beispiel verwendet "Endlich taglos, teilweise bewertet" ( citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.99.9287 ) "fold", "compositional" und "primitive recursive" im Intro als offensichtliche Synonyme (Aber das wird in der Zeitung nicht viel besprochen, es ist selbstverständlich). Umgekehrt scheint dies ein Diskussionspunkt in der Philosophie zu sein, wenn man Wikipedia hier anvertrauen
möchte
1
@Blaisorblade Als ich ein Doktorand war, knüpfte ich Kontakte zu denotationalen Semantikern, weil ich eigentlich an denotationalen Semantiken arbeiten sollte. Ich habe sie immer gefragt, was Denotationssemantik sei, wenn sie mir eine abstrakte Definition geben könnten, aber ich habe nur ausweichende oder vage Antworten wie "Denotationssemantik ist mathematische Semantik" erhalten, siehe auch A. Bauers Erklärung. Ich denke nicht, dass das Konzept gut definiert ist. Ich verstehe auch nicht, warum die Forderung nach primitiver Rekursivität einschränkend genug ist, da die Macht der primitiven Rekursion davon abhängt, was noch verfügbar ist: (Fortsetzung)
Martin Berger,
16

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.

Uday Reddy
quelle
Ein konstruktiver Ansatz zur Lösung dieses Problems könnte darin bestehen, Übersetzungen zwischen den verschiedenen Ansätzen zu finden.
Martin Berger
1
Beachten Sie, dass ich keine Probleme mit der herkömmlichen Denotationssemantik als Werkzeug in der Toolbox habe. Ich finde nur die impliziten oder expliziten Vorschläge, dass sie irgendwie problematischer sind und keine kohärente Begründung haben.
Martin Berger
Ich würde die von Peter O'Hearn und Bob Tennent herausgegebenen Bände "Algollike Languages" ( eecs.qmul.ac.uk/~ohearn/Algol/algol.html ) als Musterbeispiel für bewährte Verfahren aufstellen . Dazu gehören Arbeiten zur "konventionellen Denotationssemantik" (Strachey, Reynolds, Tennent, Meyer et al.) Sowie zur "unkonventionellen" Denotationssemantik (Mine, Abramsky & McCusker, Brookes) und zu operationellen Ansätzen (Andy Pitts, Felleisen). Übrigens waren zwei Arbeiten von Reynolds in den Bänden (Specification Logic und Syntactic Control of Interference) "axiomatisch", als sie geschrieben wurden!
Uday Reddy
1
In Bezug auf den gesunden Wettbewerb besteht ein Hauptproblem darin, dass es so viele Ansätze, Formalismen, Forscher und Papiere gibt, dass es schwierig ist, mit der Entwicklung Schritt zu halten. Es könnte sich für uns als Forschungsgemeinschaft lohnen, die bestehenden Ansätze nachhaltig zu synthetisieren und zu vereinheitlichen.
Martin Berger
2
@MartinBerger, ein Ausgangspunkt, den ich kenne, ist Patrick Cousots Arbeit "Constructive Design of a Hierarchy of Semantics", die zeigt, dass ein sehr breites Spektrum von semantischen Modellen, einschließlich Übergangssystemen, axiomatischer Semantik und Denotationsmodellen, mithilfe von Zusätzen in Beziehung gesetzt werden kann. daher als unterschiedliche Abstraktionen angesehen.
Vijay D
12

[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.

Uday Reddy
quelle
10

[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.

Uday Reddy
quelle
Es tut uns leid, dass Sie nicht auf die Chat-Anfrage geantwortet haben. Ich bin sehr beschäftigt für die nächsten zwei Wochen. Vielen Dank für das Schreiben! Es ist die erste technische Antwort auf der Seite, die ich verstehe.
Vijay D
Ich könnte diese Gelegenheit nutzen, um einen Stecker für unsere Midlands Graduate School in Theoretical Computer Science einzustecken, die all diese Probleme angehen soll. Es steht allen Doktoranden weltweit offen.
Uday Reddy
9

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 ]

Uday Reddy
quelle