Bücher zur Programmiersprachensemantik

31

Ich habe Nielson & Nielsons " Semantics with Applications " gelesen und ich mag das Thema wirklich. Ich hätte gerne noch ein Buch über Programmiersprachensemantik - aber ich kann wirklich nur eines bekommen.

Ich habe mir das Turbak / Gifford- Buch angesehen, aber es ist zu langatmig. Ich dachte, Winskel wäre in Ordnung, aber ich habe keinen Zugang dazu (es befindet sich nicht in unserer Universitätsbibliothek und mir fehlt das Geld), und ich bin mir nicht einmal sicher, ob es nicht veraltet ist. Slonneger scheint in Ordnung zu sein, aber der praktische Teil macht es etwas zu lang, und ich bin mit seinem Stil nicht sehr zufrieden.

Meine Frage ist also - ist Winskel ein gutes Buch? Und ist es veraltet?

Gibt es auch andere knappe Bücher zu diesem Thema?

reference-request pl.programming-languages semantics denotational-semantics books Jay
quelle
5
Links zu Verlagsseiten für alle Bücher hinzugefügt. könnte für andere nützlich sein, die suchen, um zu stöbern.
Suresh Venkat
2
Für welche Art von Semantik interessieren Sie sich? Denotational? Betriebsbereit? Ein Überblick?
Ohad Kammar
@Ohad Kammar: Beides interessiert mich.
Jay

Antworten:

31

Es kommt darauf an, wie tief du gehen willst und wie viel du bereits weißt. Für einen Anfänger ist Winksel's Buch wirklich schön, aber ja, es führt Sie nicht in den Stand der Semantik ein, wie er vor ungefähr 20 Jahren geschrieben wurde. Trotzdem ist es immer noch eine gute erste Einführung in das Thema. Es könnte sich auch lohnen, darauf hinzuweisen, dass T. Nipkow einen wesentlichen Teil von Winskels Buch in Isabelle / HOL formalisiert hat, siehe hier . Wenn Sie also lernen möchten, interaktive Proof-Assistenten zu verwenden und die Semantik von Programmiersprachen zu verstehen, müssen Sie auf eine Menge zusammenhängenden Materials zurückgreifen.

Andere Bücher, die fortgeschrittener sind, sind:

  • Gunter, Semantik der Programmiersprachen , ein fortgeschritteneres Buch, das sich mit denotationaler Semantik befasst, einem Ansatz zur Semantik, der die Erwartungen nicht erfüllt. Konzentriert sich auf rein funktionale Sprachen und ignoriert Parallelität. Dies ist das Buch, von dem ich mir als Student Semantik beigebracht habe, und im Nachhinein wünschte ich, ich hätte stattdessen Winksel's Buch verwendet. Für einen Anfänger ist Gunter keine einfache Lektüre.

  • Domains und Lambda-Kalküle von Amadio und Curien. Ein weiteres Buch, das mehr in der domänentheoretischen Tradition geschrieben wird, obwohl es Prozesskalküle behandelt.

  • John Mitchells Bücher, die bereits oben erwähnt wurden. Meist geht es auch um sequentielle Berechnungen.

Bücher wie Pierces TAPL sind sehr schön, konzentrieren sich jedoch eng auf einen Aspekt der Programmiersprachen, nämlich die Typen, die so wichtig sind. Ich würde es nicht als erste Einführung in den allgemeinen Bereich der Programmiersprachen empfehlen, aber es ist obligatorisch, für alle zu lesen, die etwas über Typen lernen möchten.

Um ehrlich zu sein, ich denke, es gibt derzeit kein aktuelles Einführungsbuch zur Sprachsemantik, das die erheblichen Fortschritte des letzten Jahrzehnts widerspiegelt, mit seiner entscheidenden Verlagerung von Denotationsmethoden und sequentiellen Berechnungen hin zur Nebenläufigkeit (Prozesskalküle und Spielesemantik). , Axiomatik-Semantik und die Verwendung interaktiver Proof-Assistenten bei der Verifikation.

Update 22. April 2014: Tobias Nipkow und Gerwin Klein haben ein neues Buch veröffentlicht

was als "Winskel in Isabelle / HOL" gesehen werden kann. Es ist eine Einführung in die Semantik von Programmiersprachen (hauptsächlich operationell und axiomatisch), aber im Gegensatz zu früheren Ansätzen auf Stift- und Papierbasis bringt dieses Buch all seine Mathematik in Isabelle / HOL zum Ausdruck. Mit anderen Worten, es ist gleichzeitig ein Buch über das Beweisen von Theoremen.

Das Buch ist brandneu, daher habe ich es nicht zum Unterrichten verwendet, aber es eignet sich sehr gut als Einführung, die niedriger ist als die von Software Foundations von Pierce et al.

Martin Berger
quelle
2
Gibt es eine Abkehr von den Bezeichnungsmethoden? Scheint mir eher wie die Art von Menschen, die früher handgewellte Proofs verwendeten, von denen heutzutage erwartet wird, dass sie formelle Proofs produzieren. Da Denotationsmethoden immer noch nicht einfach alles modellieren können, was wir tun, und viel mehr Voraussetzungen erfordern, verwenden diese Forscher zugänglichere Methoden wie Spiele, Prozesskalküle und Beweisassistenten. Ich bin mir nicht sicher, ob es einen Rückgang der Bezeichnungsmethoden gibt.
Ohad Kammar
4
Bitte verwechseln Sie die Denotationssemantik nicht mit der Domänentheorie . Die Spielesemantik kann und ist in der Regel perfekt denotational, dh die Bedeutung eines Programms ist eine Funktion der Bedeutungen seiner Teile.
Andrej Bauer
2
Ich habe einen neuen Thread zu diesem Kommentar eröffnet. Aber auch wenn ich nicht sicher bin, ob ich Ihrer Definition zustimme, ist die Spielesemantik denotationaler Natur. Ich denke, ich sollte "Spiele" in meinem Kommentar durch "operative Semantik" ersetzen und die Spielesemantik als möglicherweise eine andere Form der Suche nach denotationaler Semantik einbeziehen. cstheory.stackexchange.com/questions/3577/…
Ohad Kammar
1
Ich bin nicht überzeugt, dass es eine Verschiebung gibt. Siehe meinen ersten Kommentar im Lichte von Andrejs Kommentar.
Ohad Kammar
1
Gibt es eine Verschiebung? Eine interessante Frage. Wie können wir eine Verschiebung messen? Es gibt so viele Kriterien, die wir anwenden könnten, von den relativ konkreten Kriterien wie der Höhe der Resarch Grants, die für verschiedene Ansätze vergeben werden, bis hin zu vagen Ideen wie Mind-Share. Angesichts der Tatsache, dass wir als Forscher, als Mitarbeiter und als Antragsteller für Zuschüsse am Ergebnis einer solchen Frage beteiligt sind, ist es unwahrscheinlich, dass wir uns auf eine Antwort einigen.
Martin Berger
20

Hier ist eine zufällige Auswahl von Materialien, die kostenlos online verfügbar sind:

  • Winskel, Die formale Semantik von Programmiersprachen , Vorschau auf Google Books . Ich weiß nichts über dieses Buch. Es ist auf der Liste, weil die Frage speziell nach dem Inhalt fragt, der hauptsächlich online ist.
  • Morgan, Programming from Specification , Liste der ps-Dateien . Das Thema ist Verfeinerung, dh der Prozess, bei dem mit nicht ausführbaren Beschreibungen auf hoher Ebene begonnen und dann systematisch in etwas Ausführbares verwandelt wird. Natürlich muss bei jedem Verfeinerungsschritt die Semantik erhalten bleiben, daher wird auch eine bestimmte Art von Semantik behandelt (hauptsächlich basierend auf Prädikat-Treansformern).
  • Harper, Praktische Grundlagen der Programmiersprachen , pdf des Entwurfs . Siehe den Kommentar von Dave Clarke weiter unten.
  • Remy, Using, Understanding und Unraveling der OCaml-Sprache , pdf . Dies ist das Buch , aus dem ich den funktionalen Programmierung gelernt (OCaml, genauer gesagt) und ich mochte es sehr viel . Es stellt die Semantik grundlegender Sprachmerkmale auf eine sehr schöne Art und Weise vor und präsentiert dabei Lambda-Kalkül und Typentheorie auf einer Basis, die man wissen muss.
  • Peyton Jones, Die Implementierung funktionaler Programmiersprachen , djvu . In den ersten Kapiteln wird der Lambda-Kalkül (und seine "operative Semantik") beschrieben und wie übergeordnete Sprachfunktionen in den Lambda-Kalkül umgewandelt werden. In diesem Sinne gibt der Aufsatz eine operationelle Semantik für funktionale Sprachen.
  • Pierce (ed), Fortgeschrittene Themen in Typen und Programmiersprachen , Google Books-Vorschau .
  • Slonneger, Syntax und Semantik von Programmiersprachen , Liste der PDF-Dateien . Ich habe das vor langer Zeit kurz angeschaut und es nicht sehr gemocht. Es steht auf der Liste, weil es in der Frage erwähnt wird.
  • Brookes, Eine Semantik für die Logik der gleichzeitigen Trennung , pdf . Dies ist ein großer Artikel (80 Seiten), kein Buch. Ich habe es aufgenommen, weil es eine ziemlich neue Entwicklung ist, die ich interessant finde.
Radu GRIGore
quelle
1
Das ist eine Menge Links :)
Suresh Venkat
3
Dies wäre nützlicher, wenn es als Liste dargestellt worden wäre. Jedenfalls würde ich das Harper-Buch empfehlen: Klicken Sie auf "Macht".
Dave Clarke
Genau. Radu, könntest du die Bücher auflisten, damit wir wissen, worauf wir klicken? Dies wäre eine hervorragende Ressource.
Suresh Venkat
Es ist jetzt eine Liste. (Die erste Version wurde gegen 2 Uhr morgens veröffentlicht, nachdem sie in der vergangenen Nacht
ungefähr
16

Ich würde die Bücher zur Programmiersprachensemantik in zwei Klassen unterteilen: jene, die sich auf die Modellierung von Programmiersprachenkonzepten konzentrieren, und jene, die sich auf die grundlegenden Aspekte der Semantik konzentrieren. Es gibt keinen Grund, warum ein Buch nicht beides kann. Aber in der Regel kann man nur so viel in ein Buch schreiben, und die Autoren haben auch ihre eigenen Vorlieben für das, was wichtig ist.

Das bereits erwähnte Buch von Winskel leistet einen Beitrag zu beiden Aspekten. Und es ist ein gutes Buch für Anfänger. Ein ebenso gutes, vielleicht sogar noch besseres Buch ist das, mit dem ich angefangen habe: Gordons Denotational Description of Programming Languages . Dies war mein erstes Buch über Semantik, das ich kurz nach Abschluss meines Studiums las. Ich muss sagen, es hat mir eine solide Grundlage in der Semantik gegeben, und ich musste mich nie wundern, wie sich die Denotationssemantik von der operativen Semantik oder der axiomatischen Semantik usw. unterscheidet. Dieses Buch wird mein absoluter Favorit auf dem Gebiet der Denotationssemantik bleiben.

Andere Bücher, die sich eher auf Modellierungsaspekte als auf grundlegende Aspekte konzentrieren, sind die folgenden:

  • Tennents Semantik der Programmiersprachen , ein mehr oder weniger aktuelles Buch über die Semantik imperativer Programmiersprachen. Es ist leicht zu lesen. In späteren Abschnitten des Buches ist es jedoch eher abstrakt, und es kann sein, dass Sie Schwierigkeiten haben, herauszufinden, warum die Dinge auf eine bestimmte Art und Weise erledigt werden.

  • Reynolds ' Theorien der Programmiersprachen . Jeder, der sich auf Semantik spezialisiert hat, sollte dieses Buch unbedingt lesen. Es ist immerhin von Reynolds. (David Schmidt bemerkte einmal zu mir: "Auch wenn Reynolds Ihnen die Morgenzeitung vorliest, möchten Sie aufmerksam zuhören, weil Sie vielleicht etwas Wichtiges lernen"!) Sie deckt sowohl die Modellierungsaspekte als auch die grundlegenden Aspekte gut ab.

Die besten Bücher zu grundlegenden Aspekten sind Gunters (das ich als ein Lehrbuch für Hochschulabsolventen betrachte) und Mitchells (das ein gutes Nachschlagewerk ist, das Sie in Ihrem Bücherregal haben sollten, weil es ziemlich umfassend ist).

Uday Reddy
quelle
Es ist sehr schön, dich hier zu haben, Uday!
Radu GRIGore
Ich bin froh, auch hier zu sein. Dies ist eine sehr schöne Ressource!
Uday Reddy
Wie wäre es mit: Übergänge und Bäume: Eine Einführung in die strukturelle Betriebssemantik von Hans Hüttel 2010. Scheint, gute Kritiken zu haben, aber niemand erwähnt es hier.
Arturo Hernandez
1
@Uday: Danke für die Antwort. Was bedeuten "Modellierung von Programmiersprachenkonzepten" und "Grundlagen der Semantik"? Was sind ihre Unterschiede und Beziehungen?
Tim
1
@Tim: Um die Semantik einer Programmiersprache zu vermitteln, müssen Sie einige mathematische Strukturen bilden, z. B. Mengen im einfachsten Fall, aber ausgefeilte Strukturen wie Domänen, Kategorien, Kohlegebren usw. für Probleme, die Mengen nicht behandeln können. Mit "grundlegenden Aspekten" meine ich die Theorie dieser komplexeren Strukturen. Im ersten Fall liegt der Schwerpunkt auf den Programmiersprachen und im zweiten Fall auf den mathematischen Grundlagen.
Uday Reddy
8

Ich habe es wirklich genossen, Winskel zu lesen, als ich den Semantikkurs belegte. Ich kann jedoch nicht sagen, ob es veraltet ist, da ich auf diesem Gebiet nicht forsche. Ein Plus von Winskel ist, dass es auch in anderen Sprachen als Englisch übersetzt ist.

Für eine weiterführende Lektüre, eher für Absolventen, würde ich John Mitchells Bücher Foundations for Programming Languages und Concepts in Programming Languages vorschlagen . Wenn Sie nur die ersten Kapitel lesen, erfüllen sie vermutlich auch Ihre Anforderungen an die Prägnanz.

Sie werden keine freien Entwürfe für diese Bücher finden. Wenn Sie also ein begrenztes Budget haben, wählen Sie in Radus Antwort die "Macht".

Alessandro Cosentino
quelle
6

Nun, ich bin kein Experte auf diesem Gebiet, aber es gibt einige allgemeine Ratschläge, die ich geben kann.

Erstens gibt es einige Leute, die das Buch bereits gelesen und Rezensionen dazu abgegeben haben. Zum Beispiel fand ich für das Winskel-Buch Die formale Semantik der Programmiersprachen (siehe [1] und [2] ) Rezensionen bei Amazon.

Teil einer Bewertung lautet:

Dieses Buch verwechselt von Anfang an Syntax und Semantik, so wie man die Literale von ihren Werten trennt. Es wurden keine speziellen Notationen verwendet, um sie zu unterscheiden. Dies ist ein entscheidendes Thema, das der Autor in einem solchen Thema ansprechen sollte. Auch einige andere von ihm verwendete Notationen sind ziemlich verwirrend, wie das Zeigen der Prämissen und Schlussfolgerungen.

Der Autor schien davon auszugehen, dass Sie ALLE notwendigen Voraussetzungen haben, da er die Hintergrundmaterialien in den ersten Kapiteln (dh Mengenlehre, Operationssemantik, Induktionen, induktive Definitionen) sehr kurz erklärt hat. Der Stil, den der Autor in der Einleitung verwendet, besteht darin, zwei oder drei Absätze von Texten und einige Formeln zu setzen und dann Übungen zu geben. Was für mich ziemlich frustrierend ist ...

18/20 Personen finden die Bewertung hilfreich. Sie können nach Amazon (oder anderen Quellen) suchen, um weitere Bewertungen zu erhalten.

Zweitens bietet Amazon zusammen mit diesem Buch Typen und Programmiersprachen sowie grundlegende Kategorietheorien für Informatiker an. Zu einem anderen Thema bietet Dave Clarke diese Bücher als hervorragende Bücher zum Thema "Typensysteme und Semantik von Programmiersprachen" an. Auch hier bin ich kein Experte, aber diese könnten für Sie nützlich sein.

MS Dousti
quelle
TaPL geht für meinen Geschmack etwas zu langsam. Es ist ein gutes Buch, aber ich habe es erwähnt, weil die fragende Person sich Sorgen um "langatmige" Bücher zu machen scheint.
Radu GRIGore
@ Radu: TAPL ist zwar langsam, aber eine recht gute Einführung. Das Harper-Buch, das Sie in Ihren Links erwähnt haben, geht viel schneller und deckt viel mehr Themen ab, obwohl es noch nicht abgeschlossen ist.
Dave Clarke
4
Nehmen Sie die Amazon-Rezension von Winskels Buch mit einer Prise Salz. Es wird oft als empfohlener Text in Semantikkursen für Studenten verwendet und zieht möglicherweise verärgerte Studenten an. Ich habe das Buch gelesen und die einleitenden Kapitel mehr als ausreichend gefunden. Seine Notation schien ebenfalls völlig normal zu sein.
Dominic Mulligan