Was ist die theoretische Grundlage der imperativen Programmierung?

48

Die funktionale Programmierung hat eine theoretische Grundlage in der Lambda-Rechnung und der kombinatorischen Logik . Als jemand, der sich mit statistischem Rechnen beschäftigt, finde ich diese Konzepte sehr nützlich für die Modellierung.

Gibt es eine äquivalente mathematische Grundlage für die imperative Programmierung , oder ist sie einfach aus der praktischen Hardwareanwendung in Maschinensprache und der anschließenden Entwicklung von FORTRAN entstanden ?

Shane
quelle

Antworten:

27

Wenn Mathematik zum Studieren von X verwendet wird , benötigt man im Allgemeinen zuerst ein Modell von X und entwickelt dann eine Theorie, eine Reihe von Ergebnissen zu diesem Modell. Ich vermute, dass die Theorie eine "theoretische Basis" für X ist . Stellen Sie nun X = Berechnung ein. Es gibt viele Berechnungsmodelle, von denen viele den "Zustand" betreffen. Jedes Modell hat seine eigene "Theorie" und es ist manchmal möglich, zwischen Modellen "zu übersetzen". Ich glaube, es ist schwer zu sagen, welches Modell "grundlegender" ist - sie wurden einfach mit Blick auf unterschiedliche Ziele entworfen.

Turingmaschinen wurden entwickelt, um zu definieren, was berechenbar ist . Sie sind also ein gutes Modell, wenn Sie sich Gedanken darüber machen, ob für ein bestimmtes Problem ein Algorithmus existiert. Dieses Modell wird manchmal missbraucht, um die Effizienz von Algorithmen oder die Härte von Problemen zu untersuchen, unter dem Vorwand, dass es gut genug ist, zumindest wenn Sie sich nur für Polynome / Nicht-Polynome interessieren. Das RAM-Modell ist näher an einem realen Computer und daher besser, wenn Sie eine genaue Analyse eines Algorithmus wünschen. Um die Härte der Probleme zu begrenzen, ist es besser, dies nicht zu tunVerwenden Sie ein Modell, das zu sehr den heutigen Computern ähnelt, da Sie eine Vielzahl möglicher Computer abdecken möchten und dabei präziser als nur polynomiell / nicht polynomiell sind. In diesem Zusammenhang habe ich zum Beispiel das verwendete Zell-Sonden-Modell gesehen.

Wenn Sie Wert auf Korrektheit legen , sind noch andere Modelle hilfreich. Hier haben Sie operationale Semantik (die ich als das Analogon der Lambda-Berechnung für Statefull-Berechnungen bezeichnen würde), axiomatische Semantik (entwickelt von Hoare 1969 auf der Grundlage von Floyds induktiven Behauptungen aus dem Jahr 1967, die Knuth in The Art of Computer Programming popularisiert hat). Band 1) und andere.

Zusammenfassend denke ich, dass Sie Berechnungsmodelle suchen. Es gibt viele solcher Modelle, die mit unterschiedlichen Zielsetzungen entwickelt wurden, und viele haben einen Status, sodass sie einer imperativen Programmierung entsprechen. Wenn Sie wissen möchten, ob etwas berechnet werden kann, schauen Sie sich Turing-Maschinen an. Wenn Sie Wert auf Effizienz legen, schauen Sie sich die RAM-Modelle an. Wenn Sie Wert auf Korrektheit legen, schauen Sie sich Modelle an, die mit "Semantik" enden, z. B. operative Semantik.

Lassen Sie mich zum Schluss erwähnen, dass nur über Computermodelle von John Savage ein großes Buch online ist . Es geht hauptsächlich um Effizienz. Für den Korrektheitsteil empfehle ich, mit den klassischen Papieren von Floyd (1967) , Hoare (1969) , Dijkstra (1975) und Plotkin (1981) zu beginnen . Sie sind alle ziemlich cool.

Radu GRIGore
quelle
4
Ich denke, Operational Semantics ist in der Tat das, wonach das Poster sucht. Ein bisschen mehr Infos auf Wikipedia: en.wikipedia.org/wiki/Operational_semantics
sclv
22

Das einfachste theoretische Modell eines Imperativprogramms ist die Turingmaschine selbst. Es hat beide wesentlichen Komponenten eines imperativen Programms: einen unbegrenzten modifizierbaren Zustand und eine Zustandsmaschine, die darauf arbeitet.

Sie können die imperative Programmierung auch auf die funktionale Programmierung gründen, indem Sie Programme als Kompositionen monadischer Operationen betrachten, die modifizierte Versionen des globalen Zustands übergeben und zurückgeben, wie dies in der Programmiersprache Haskell geschieht.

Alexandre Passos
quelle
2
Die Verwendung von Monaden, um imperativartige Konstrukte in einer rein funktionalen Sprache (wie Haskell) zu erhalten, gibt Ihnen nicht die volle Kraft der imperativen Programmierung. Insbesondere ohne wirklich veränderlichen Zustand (z. B. wie in vielen Sprachen mit Referenzen) gibt es noch viele Datenstrukturen, deren effiziente Implementierung in einer rein funktionalen Sprache unbekannt ist.
Joshua Grochow
@Joshua: Warum drücken Staatsmonaden Ihrer Meinung nach nicht die Semantik von Referenzen aus? Ich verstehe nicht, was der Einwand sein könnte.
Charles Stewart
Eine Zustandsmonade ist im Grunde ein syntaktischer Zucker für eine Sammlung von Funktionen, die alle ein zusätzliches Argument (Zustand) akzeptieren und eine zusätzliche Ausgabe (nächster Zustand) ausgeben. In einer rein funktionalen Sprache können Sie den Status jedoch nicht ändern, um den nächsten Status zu erhalten. Sie müssen ihn dennoch kopieren und rekonstruieren. Ich weiß nicht, ob es bestimmte Datenstrukturen gibt, bei denen bekannt ist , dass sie in einer rein funktionalen Sprache nicht effizient implementiert werden können, aber es gibt sicherlich Hinweise (z. B. Pippenger. Pure vs. unreine Lisp. 1997).
Joshua Grochow
6
Man kann die Semantik der Mutation mit Monaden sehr gut erfassen - siehe z. B. die ST-Monade in Haskell. Wir sprechen hier von Semantik, nicht von Implementierung.
sclv
20

Kurz gesagt, ich würde sagen, dass die imperative Programmierung aus der Maschinensprache und der Programmierpraxis hervorgegangen ist. Andererseits bieten Monaden einen geeigneten semantischen Rahmen zur Beschreibung der Semantik imperativer Programmiersprachenmerkmale. Die Papiervorstellungen von Computing und Monaden von Moggi begründeten die formalen Grundlagen. Phil Wadler machte die Idee populär und trug maßgeblich dazu bei, dass wichtige Funktionen in die Programmiersprache Haskell integriert wurden. Neueste Arbeiten von Plotkin und Power Notions of Computation Determine Monads geht in die andere Richtung und besagt, dass einige, aber nicht alle Begriffe der (imperativen) Berechnung tatsächlich eine Monade ergeben, was bedeutet, dass Monaden in einer sehr wesentlichen Weise imperativen (und anderen) Begriffen der Berechnung entsprechen.

Dave Clarke
quelle
8
Monaden können verwendet werden, um die imperative Programmierung in einer rein funktionalen Welt abzusperren, aber ich kann nicht behaupten, dass sie eine theoretische Grundlage für die imperative Programmierung analog zur Beziehung zwischen dem Lambda-Kalkül und vielen funktionalen Sprachen bilden. Monaden modellieren die Berechnung nicht so sehr, als dass sie eine Abstraktion über Klassen der Berechnung bilden (z. B. reine Berechnung vs. Berechnung, die E / A beinhaltet, oder Berechnung, die auf einem bestimmten Bündel von veränderlichen Zuständen beruht).
blucz
1
Monaden sind eine Möglichkeit, klarere Denotationssemantiken für effektive Sprachen zu schreiben. Warum also nicht?
nponeccop
15

Wenn Sie nach einer rigorosen mathematischen Behandlung einer imperativen Programmiersprache suchen, ist Winskels Buch "Die formale Semantik der Programmiersprachen" (1993) ein Beispiel.

In dem Buch definiert er eine imperative Programmiersprache namens IMP und liefert eine operationelle, denotationale und axiomatische Semantik davon.

yhirai
quelle
14

Ich komme zu dieser Frage spät, aber es ist eine faszinierende Frage. Also, hier sind meine Ansichten.

Als ich Student war, hatten wir einen großartigen Mathematikprofessor, der uns Vorlesungen über Geschichte und Entwicklung der Mathematik hielt. Ihm zufolge entwickelte sich die Mathematik in Wellen der "Expansion" und "Konsolidierung". In einer Expansionsphase wurden bisher unbekannte neue Ideen berücksichtigt und untersucht. In einer Konsolidierungsphase wurden dann die neuen Theorien in den vorhandenen Wissensbestand integriert. Im 20. Jahrhundert würden Expansion und Konsolidierung jedoch parallel stattfinden.

Imperative Programmierung ist derzeit eine Erweiterungstätigkeit für Mathematik. Es war zuvor "unbekannt". (Das mag nicht ganz zutreffen. Hoare sagt uns , dass Euklid in seiner Geometrie so etwas wie imperative Programmierung gemacht hat. Aber die Mathematik hat das Interesse daran verloren.) Mathematiker sind immer noch nicht an imperativer Programmierung interessiert. Soviel der Verlust für sie. Aber ich betrachte die gesamte Informatik als einen Zweig der Mathematik im abstrakten Sinne. Wir studieren es und erweitern dabei die Mathematik.

Es ist mir also egal, ob es eine theoretische Grundlage für die imperative Programmierung von vornherein gibt. Wenn es keinen gibt, lass uns gehen und ihn finden. Was wir bereits wissen, sagt uns, dass imperative Programmierung fantastisch tief und schön ist. Die funktionale Programmierung verblasst im Vergleich. Wir haben jedoch noch viel zu tun, um all diese Theorien den Menschen nahezubringen.

Uday Reddy
quelle
"Funktionale Programmierung verblasst im Vergleich". Wenn ich Sie und Bob Harper nur in eine Kampfarena bringen könnte. Du würdest einen großen Block von Befehlen schwingen und er würde versuchen, einen Schluss auf dich zu ziehen. (PS: Sehr gute Antwort, ich habe es positiv bewertet.)
Andrej Bauer
Nun, er meidet mich irgendwie. Ich weiß nicht, ob das etwas bedeutet :-)
Uday Reddy
11

Die funktionale Programmierung hat eine klare Basis in der Mathematik, da sich die funktionalen Programmiersprachen parallel zur relevanten Mathematik entwickelt haben und ihre Designer die Mathematik in der Regel hoch geschätzt haben. Die starke und direkte Beziehung ist eine sich selbst erfüllende Prophezeiung.

Imperative Programmierung hat eine wesentlich chaotischere Geschichte, die viel enger mit geschäftlichen und technischen Problemen verbunden ist, und befasste sich historisch viel mehr mit der Leistung von Compilern und dem Code, den sie generieren, als mit der Beachtung mathematischer Formalismen.

Viele Leute haben versucht, imperative Programmierung in (traditionell) funktionalen Begriffen zu erklären. Dies ist vielleicht der nächste Weg, den wir zu dem finden, wonach Sie suchen, aber diese Versuche sind immer umständlich, mühsam und forensisch. Ich bin mir ziemlich sicher, dass ich mir lieber die Augen aus dem Gesicht reißen würde, als einen Fortschritts- / Konservierungsnachweis für die CLR zu lesen.

Wenn Sie gegen Ende eines anständigen pl-Lehrbuchs (z. B. Pierces Typen und Programmiersprachen) angelangt sind, werden Sie in der Regel eine formale Modellierung der imperativen Sprachfunktionen bemerken. Das könnte Sie interessieren.

blucz
quelle
11

An Axiomatic Basis for Computer Programming mit dem AUTO HOARE

In dieser Arbeit wird versucht, die logischen Grundlagen der Computerprogrammierung mithilfe von Techniken zu erforschen, die zum ersten Mal in der Erforschung der Geometrie angewendet und später auf andere Bereiche der Mathematik ausgeweitet wurden. Dies beinhaltet die Aufklärung von Axiomensätzen und Inferenzregeln, die für Beweise der Eigenschaften von Computerprogrammen verwendet werden können. Beispiele für solche Axiome und Regeln werden gegeben, und ein formaler Beweis eines einfachen Theorems wird gezeigt. Schließlich wird argumentiert, dass sich aus der Verfolgung dieser Themen wichtige theoretische und praktische Vorteile ergeben könnten.

http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.85.8553&rep=rep1&type=pdf

Vag
quelle
8

Ich nehme an, was Alexandre sagte, dass die Turing-Maschine die ursprüngliche theoretische Grundlage für die imperative Programmierung darstellte. In dem Maße, wie die Organisation imperativer Programmiersprachen die Maschinenarchitektur widerspiegelt, denke ich, dass die Arbeit von John Von Neumann auch ein wesentlicher Bestandteil ihrer theoretischen Grundlagen sein würde.

Kurt
quelle
7

Gibt es eine äquivalente mathematische Grundlage für die imperative Programmierung oder ist sie einfach aus der praktischen Hardwareanwendung in Maschinensprache und der anschließenden Entwicklung von FORTRAN entstanden?

Wenn Sie im historischen Sinne "Basis" meinen, gibt es meiner Meinung nach keine "gleichwertige mathematische Basis". Obwohl die imperative Programmierung aus praktischen Erwägungen hervorgegangen ist, gibt es verschiedene Möglichkeiten, die Bedeutung der imperativen Programmierung auf eine Art und Weise umfassend zu charakterisieren, die Sie als "nützlich für die Modellierung" erachten könnten, wie z. B. die Hoare-Logik .

Apfel
quelle
Wolltest du wirklich dieses Community-Wiki erstellen?
Suresh Venkat
Ja, ich wollte es zum Community-Wiki machen.
Jbapple
7

Die Beiträge, die die Hoare-Logik und die Trennungslogik erwähnen, sind in dieser Hinsicht die richtigen. Mit der Hoare-Logik können Sie Eigenschaften der gesamten Heap-Konfiguration eines Programms angeben, und mit der Trennungslogik können Sie eine "trennende Konjunktion" verwenden, mit der Sie als Vor- und Nachbedingungen für ein Codesegment angeben können, für welche Eigenschaften sie gelten der Teil des Heapspeichers, den das Programmsegment bearbeitet, während der Rest des Heapspeichers quantifiziert wird.

Die Antwort in Bezug auf Monaden ist nicht genau, da in haskell eine Monade nur verwendet wird, weil es sich um eine Abstraktion handelt, die die Codierung der Reihenfolge von Bewertungsbeschränkungen und die explizite Verfolgung der Eigenschaft "E / A-Verwendung möglich" ermöglicht.

Es sei darauf hingewiesen, dass sowohl die Hoare / Separation-Logik als Monade betrachtet werden kann, als auch dass es eine Reihe zeitgenössischer Projekte wie das ynot-Projekt in Harvard gibt, die sich mit diesen Themen befassen.

Die Forschung in der Trennungslogik ist ein fortlaufendes und aktives Feld.

Carter Tazio Schonwald
quelle
Es scheint mir ein Fehler zu sein, die Tatsache zu verwechseln, dass Haskell einen Begriff von Monaden (und eine Monadentypenklasse) mit dem allgemeineren Ansatz verwendet, wie er beispielsweise von Moggi vertreten wird, der Monaden verwendet, um eine Darstellung der kategorialen Semantik zu strukturieren. Die Einführung von Monaden als Werkzeug zur Strukturierung der Programmierung sollte uns nicht vor der Verwendung der kategorialen Semantik als Werkzeug zur Strukturierung der Argumentation über die Programmierung verblenden .
sclv
Sehr gute Klarstellung, obwohl ich glaube, dass eine ganze Reihe von Leuten Monaden a la Haskell verwendet haben, um die Semantik über Monadentransformatoren zu erforschen. Insbesondere die unterschiedliche Semantik für Operationen, die sich aus unterschiedlichen Zusammensetzungen der Transformatoren ergeben (z. B. für Zustand / Veränderlichkeit, Fortsetzungen, Nichtdeterminismus usw.)
Carter Tazio Schonwald
5

Ich komme noch später auf diese Frage, aber ich bin ebenso fasziniert davon.

Warum die Theorie der imperativen Programmierung als weniger entschieden angesehen wird als die der funktionalen Programmierung, entgeht mir. Mit Scott und de Bakker begann es wahrscheinlich 1969 ernst zu werden, als sie die Bedeutung der Rekursion in einer einfachen imperativen Sprache analysierten [1]. Wenn die imperative Sprache an Bedeutung gewinnt, wird die Geschichte ein bisschen chaotischer, aber das ist nur der Preis, den man zahlen muss, wenn man näher am Metall ist. Um eine der umfassenderen Bemühungen zu nennen, verfassten de Bakker, de Bruin und Zucker 1980 eine Monografie zu diesem Thema [2]. Andere wurden oben erwähnt. Diese Referenzen behandeln natürlich die Trennungslogik vor dem Datum, [2] gehen jedoch auf Arrays und gegenseitig rekursive Prozeduren ein.

[1]: 1969 unveröffentlicht, erschien jedoch als Jaco W. de Bakker und Dana S. Scott. Eine Theorie der Programme , Seiten 1-30. In Klop et al. JW de Bakker, 25 Jahre Semantiek. CWI, Amsterdam, 1989. Liber Amoricum.

[2]: Jacobus W. de Bakker, Arie de Bruin, Jeffrey Zucker: Mathematische Theorie der Programmkorrektheit. Prentice Hall 1980.

Kai
quelle
1
Offensichtlich zwingende Programmierung ist sehr gut verstanden. Ich denke, was die Leute meinen, wenn sie sagen, dass es weniger entschieden ist, ist, dass die strukturelle imperative Programmierung reicher ist als die reine funktionale Programmierung, und es wurde viel weniger mathematische Struktur entdeckt, die in dieser oder jener Form der imperativen Programmierung auftaucht. Zum Beispiel können bestimmte Arten von Imperativprogrammen unter Verwendung von Trennungslogik gut begründet werden. Dies hat wahrscheinlich mit Formen des Teilens zu tun. Vielleicht haben solche Programme eine schöne, abstrakte mathematische Charakterisierung?
Martin Berger
1
Ich persönlich meine, die Theorie der Modularität in imperativen Sprachen ist sehr unklar. Wir wissen, was Modularität für funktionale Sprachen bedeutet: relationale Parametrizität. Für imperative Sprachen gibt es viele informationsversteckende Redewendungen, die (a) eindeutig funktionieren, für die uns jedoch (b) gute Beweistechniken fehlen. Es gibt verlockende Hinweise darauf, dass es hier eine tiefe Theorie gibt: Wenn ich zum Beispiel modulare Beweise für sequentielle imperative Programme mache, brauche ich letztendlich Techniken aus der Parallelität. Informell ist Aliasing wie Nebenläufigkeit, aber ich weiß nicht genau, wie ich diese Idee formalisieren soll ...
Neel Krishnaswami
@ Kai. Willkommen im Thread! Es ist lange her, dass ich mir die Arbeit von de Bakker angesehen habe, aber ich denke, das Grundproblem ist, dass der Ansatz nicht skaliert wurde. Eine kurze Zusammenfassung der Fortschritte bei der imperativen Programmierung seitdem finden Sie in meinem Beitrag unter "Was macht die Denotationssemantik aus?". Thread- Link .
Uday Reddy
@NeelKrishnaswami. Ich würde gerne diese Beweise sehen. Sind sie auf Ihrer Webseite? Aliasing ist insofern wie Nebenläufigkeit, als beide ein komplexes Teilen und Verschachteln beinhalten. Gleichzeitig abstrahieren Sie das Interleaving und gehen von Nichtdeterminismus aus (was gut ist). Beim Aliasing zwingen Sie sich, sich mit dem Interleaving auseinanderzusetzen. Die Spielesemantik ist ein hervorragendes Beispiel für dieses erzwungene Interleaving, weshalb ich es nicht mag.
Uday Reddy
3

Kurz nachdem Sie Ihre Frage gestellt hatten, veröffentlichte Mark Bender von der McMaster University eine These: Zuweisungsrechnung: Eine reine imperative Argumentationssprache (8. September 2010). Diese Arbeit beschreibt eine einfache, imperative Sprache, die der Lambda-Rechnung entspricht.

Der Zuweisungskalkül besteht aus nur vier Grundkonstrukten: Zuweisung X:=t, Sequenz t;u, Prozedurbildung ¡tund Prozeduraufruf !t. Für AC werden drei Interpretationen angegeben: eine operationelle Semantik, eine denotationale Semantik und ein System zum Umschreiben von Begriffen. Die drei sind als gleichwertig dargestellt.

Mark Benders Dissertation geht weiter auf Varianten ein, die durch Lazy Evaluation, Backtracking und Procedure Composition erweitert wurden. Dies ähnelt der Erforschung der Lambda-Rechnung mit kleinen Erweiterungen.

Insgesamt liefert die Arbeit eine relativ direkte Antwort auf die OP-Frage.

dmbarbour
quelle
pdf-Link ist kaputt
Quinn Wilson