Wie werden Nebenwirkungen in der Semantik behandelt?

In Anthony Aabys Abschnitt "Einführung in Programmiersprachen" über Semantik macht er folgende Bemerkung:

Ein Großteil der Arbeit in der Semantik von Programmiersprachen ist durch die Probleme motiviert, die beim Versuch auftreten, imperative Programme zu konstruieren und zu verstehen - Programme mit Zuweisungsbefehlen. Da der Zuweisungsbefehl den Variablen Werte neu zuordnet, kann die Zuweisung unerwartete Auswirkungen auf entfernte Teile des Programms haben.

Dies erscheint mir als bemerkenswertes Eingeständnis, dass das Zulassen von Nebenwirkungen einen Großteil der Arbeit in der Semantik motivieren würde.

Wie wirkt sich das Vorhandensein von Nebenwirkungen in einer Programmiersprache auf die Fähigkeit aus, ein Programm einem Rechenmodell zuzuordnen? Gibt es Ansätze zur Bewältigung des Zustands, die diesen Prozess verbessern und gleichzeitig Nebenwirkungen zulassen können?

Aufbauend auf Charles 'Antwort besteht die Hauptschwierigkeit in der Theorie der Programmiersprachen darin, dass der natürliche Begriff der Äquivalenz von Programmen weder in der einfachsten mathematischen Semantik, die Sie geben können, noch im zugrunde liegenden Maschinenmodell eine strikte Gleichheit darstellt. Betrachten Sie beispielsweise das folgende Stück Java-ähnlichen Codes:

Object x = new Object();
Object y = new Object();
... some more code ...

Also erstellt dieses Programm ein Objekt und benennt es mit x, erstellt dann ein zweites Objekt mit dem Namen y und führt dann weiteren Code aus. Angenommen, ein Programmierer beschließt, die Zuordnungsreihenfolge dieser beiden Objekte umzudrehen:

Object y = new Object();
Object x = new Object();
... some more code ...

Stellen Sie nun die Frage: Ändert dieses Refactoring das Verhalten des Programms? Zum einen werden auf der zugrunde liegenden Maschine x und y in den beiden Programmläufen an unterschiedlichen Stellen zugeordnet. In diesem Sinne verhält sich das Programm also anders.

In einer Java-ähnlichen Sprache können Sie Referenzen jedoch nur auf Gleichheit und nicht auf Ordnung testen. Dies ist also ein Unterschied, den der "etwas mehr Code" nicht feststellen kann . Infolgedessen erwarten die meisten Programmierer, dass die Umkehrung der Reihenfolge keinen Einfluss auf die endgültige Antwort hat, und die meisten Compiler-Autoren erwarten, dass sie auf dieser Basis Nachbestellungen und Optimierungen vornehmen können. (Auf der anderen Seite, in einem C-ähnlicher Sprache, Sie können Zeiger für die Bestellung vergleichen, indem man sich auf ganze Zahlen zuerst Gießen und so diese Neuanordnung tut nicht unbedingt beobachtbares Verhalten erhalten.)

Eine der zentralen Fragen der Semantik ist die Beantwortung der Frage, wann zwei Programme beobachtbar gleichwertig sind. Da unser Begriff der Beobachtung von den Merkmalen der Programmiersprache abhängt, ergibt sich eine Definition wie "zwei Programme sind äquivalent, wenn kein Client-Programm unterschiedliche Antworten auf der Grundlage des Empfangs dieser Programme als Eingaben berechnen kann". Die Quantifizierung aller Client-Programme macht diese Frage schwierig - es scheint, als müssten Sie etwas über alle möglichen Client-Programme sagen, um etwas über zwei bestimmte Codeteile zu sagen.

Der Trick bei der Denotationssemantik besteht darin, eine mathematische Interpretation zu geben, mit der Sie diese universelle Quantifizierung vermeiden können. Sie sagen, dass die Bedeutung eines Codeteils ein mathematischer Wert ist, und vergleichen sie, indem Sie prüfen, ob sie mathematisch gleich oder gleich sind nicht. Dies ist lokal (dh kompositorisch) und beinhaltet keine Quantifizierung über alle möglichen Kunden. (Sie müssen zeigen, dass die Denotationssemantik eine kontextbezogene Äquivalenz impliziert, damit sie stichhaltig ist. Wenn sie vollständig ist - wenn die Denotationsgleichheit genau der kontextbezogenen Äquivalenz entspricht, ist die Semantik "vollständig abstrakt".)

Dies bedeutet jedoch, dass Sie sicherstellen müssen, dass die Denotationssemantik diese Äquivalenzen validiert. Wenn Sie also in diesem Beispiel eine Denotationssemantik für diese Java-ähnliche Sprache angeben möchten, müssen Sie sicherstellen, dass beim Aufruf von new nicht nur ein Heap erstellt und ein neuer Heap mit dem neu erstellten Objekt zurückgegeben wird, sondern auch die Bedeutung des Programms ist unter allen Permutationen des Eingabeheaps gleich. Dies kann recht komplexe mathematische Strukturen beinhalten (zB in diesem Fall in einer Kategorie arbeiten, die sicherstellt, dass alles Modulo einer geeigneten Permutationsgruppe funktioniert).

Es gibt natürlich Möglichkeiten, mit Effekten in (denotationaler) Semantik umzugehen. Zum Beispiel können wir die Idee von Eugenio Moggi verwenden , dass Computereffekte Monaden sind (diese Idee wurde auch beim Entwurf von Haskell verwendet). Eines der Probleme dabei ist, dass Monaden schwer zu kombinieren sind. Gordon Plotkin und John Power schlugen eine Verfeinerung von Moggis Monaden zu Lawvere-Theorien oder algebraischen Theorien, wie sie auch genannt werden, vor, die algebraische Effekte umfassen (die meisten Effekte sind algebraisch, wie Zustand, E / A, Nichtdeterminismus, aber Fortsetzung sind es nicht). Für eine umfassende Behandlung siehe Matija Pretnars These .

Ich sollte auch die mögliche Weltsemantik für den lokalen Staat erwähnen , die von Frank Oles und John Reynolds entwickelt wurde (Entschuldigung, es gibt keinen besseren Link, das Zeug stammt aus dem Jahr 1982) und die Moggis Monaden vorausgeht. Sie verwendeten Kategorien von Presheaves, um eine Semantik einer algolähnlichen Sprache bereitzustellen, die viele Aspekte des lokalen Staates korrekt modellierte (aber nicht alle, ich denke, das Modell erlaubte Snapback, aber vielleicht dient mir mein Gedächtnis falsch).

Matthias Felleisen präsentierte in seiner Reihe "Syntaktische Kontroll- und Zustandstheorien" eine überzeugende Lösung für das Nebenwirkungsproblem in der Semantik.

Aus dieser Arbeit heraus entstand die CESK-Maschine, ein einfaches abstraktes Maschinen-Framework, mit dem funktionale, objektorientierte, imperative und sogar logische Sprachen präzise modelliert werden können. Das CESK-Framework behandelt nicht nur Nebenwirkungen, sondern auch "komplexe" Steuerungskonstrukte wie Ausnahmen, Fortsetzungen, Faulheit und sogar Threads.

Die CESK-Maschine und die Small-Step-Operational-Semantik sind seit etwa zwei Jahrzehnten der De-facto-Standard in der Theorie der Programmiersprachen.

Kurz gesagt, eine CESK-Maschine ist eine Kleinschrittmaschine mit vier Komponenten, die jeden Maschinenzustand beschreiben: die Steuerzeichenfolge (eine Verallgemeinerung des Programmzählers), die Umgebung, einen Speicher (auch Heap genannt) und die aktuelle Fortsetzung.

Die Umgebung ordnet Variablen Adressen zu. Der Store ordnet Adressen Werten zu.

Dies macht es einfach, veränderbare Variablen zu modellieren: Ändern Sie einfach den Wert an seiner Adresse.

Es erleichtert auch das Modellieren von Zeigern und die dynamische Zuordnung: Legen Sie einfach erstklassige Werte für die Speicheradressen fest.

In ähnlicher Weise ergeben sich erstklassige Fortsetzungen daraus, dass sie adressierbare Werte sind.

Wie wirkt sich das Vorhandensein von Nebenwirkungen in einer Programmiersprache auf die Fähigkeit aus, ein Programm einem Rechenmodell zuzuordnen?

Dies macht es nicht unbedingt schwierig, schränkt jedoch die Art und Weise ein, in der die Semantik größerer Ausdrücke aus kleineren Ausdrücken konstruiert werden kann. Es kann sehr schlecht mit bestimmten anderen Programmierkonstrukten interagieren, zum Beispiel, wenn man eine schottische Denotationssemantik für eine Sprache angeben möchte, die die Zuordnung von Funktionen höherer Ordnung zu globalen Referenzen ermöglicht.

Es sind nicht nur Nebenwirkungen wie der Zustand, die das Problem verursachen. Einfache imperative Sprachen wie Dijkstras geschützte Befehlssprache haben diese Art von Nebenwirkungen und eine nette Semantik. Probleme treten bei Erweiterungen des Lambda-Kalküls mit der Art der operativen Semantik auf, die von Programmiersprachen auch ohne Nebenwirkungen erwartet wird: Der frühesten, Plotkins PCF, wurden relativ früh Bezeichnungsmodelle gegeben, aber die Semantik war nicht vollständig abstrakt, was bedeutet, dass Die Denotationssemantik war zu allgemein und entsprach nicht genau ihrer operativen Semantik. In den späten 1980er Jahren erhielt PCF schließlich eine vollständig abstrakte Denotationssemantik mit Spielesemantik, die überhaupt nicht mit Scotts ordnungstheoretischer Semantik vergleichbar ist. Parallelität hat immer noch keine völlig angemessene Denotationsbehandlung erhalten.

Viele hinterfragen die Bedeutung dieser Art von Semantik. Wir können immer eine Art von operationeller Semantik bereitstellen, auch wenn diese "Semantik" nur die Programmquelle und die Namen einiger Maschinen ist, die das Programm kompiliert und ausgeführt haben. Aus diesem Grund hat Strachey die operationelle Semantik verurteilt. Die strukturelle Operationssemantik von Plotkin hat jedoch gezeigt, wie die operationelle Semantik von Maschinenmodellen getrennt werden kann, und Pitts Arbeit hat gezeigt, wie diese Semantik ähnliche Argumente über Programme und Programmiersprachen wie die denotationale Semantik unterstützen kann. Daher ist die operative Semantik eine praktikable Alternative zur denotationalen Semantik und wurde mit Erfolg auf eine beträchtliche Anzahl von Programmiersprachen wie Standard-ML angewendet.

Gibt es Ansätze zur Bewältigung des Zustands, die diesen Prozess verbessern und gleichzeitig Nebenwirkungen zulassen?

In gewissem Maße entsprechen die Schwierigkeiten beim Bereitstellen der Semantik den Schwierigkeiten beim Bereitstellen leistungsfähiger Programmiersprachen, die sich wie erwartet verhalten. Pragmatisch motivierte Entwurfsentscheidungen - wie das Vermeiden der Verwendung des globalen Status zusammen mit der gleichzeitigen Verwendung, normalerweise durch die gleichzeitige Übermittlung von Nachrichten - erleichtern die Bereitstellung von Semantik.