Was ist der Unterschied zwischen einem Kalkül und einer Programmiersprache?

Ich glaube, ich bin ziemlich verwirrt darüber, was als Kalkül und was als Programmiersprache bezeichnet wird.

Ich neige dazu, zu denken und könnte gesagt worden sein, dass ein Kalkül ein formales System ist, um über die Gleichwertigkeit von Programmen zu argumentieren. Programme haben eine von einer Maschine festgelegte operationale Semantik, die (glaube ich) deterministisch sein sollte. Auf diese Weise ist ein (korrekter) Kalkül für eine Sprache eine Beweismethode für die Programmäquivalenz.$L$

Dies scheint mir eine vernünftige Trennung zu sein, aber ist dies die allgemein akzeptierte Bedeutung? Oder ist es vielleicht sogar falsch?

Verwandte, warum sind einige operationale Semantiken nicht deterministisch (nehmen Sie an, dass sie konfluent sind)? Was bringt es, die Wahl der Strategie offen zu lassen?

Ich würde es wirklich begrüßen, wenn dies geklärt würde. und konkrete Hinweise noch mehr! Vielen Dank!

Die Bedeutung der Wörter ist nicht festgelegt, aber ich kann Ihnen meine Interpretation geben.

Ein Kalkül ist etwas, mit dem wir im Sinne des Jonglierens von Gleichungen rechnen (denken Sie an die Manipulation von Taylor-Reihen oder die Berechnung von Integralen in der Analyse). Ein Kalkül sagt uns, welche Manipulationsregeln es gibt, nicht aber welche, die wir in einer bestimmten Situation anwenden sollten.

Eine Programmiersprache sagt uns, wie man berechnet. Es sagt uns genau, wie wir die Regeln anwenden sollen. In der Regel lässt der Computer die Regeln verwenden, da diese viel schneller sind. Die Regeln können nicht deterministisch sein, und es kann sehr gute Gründe dafür geben, dass sie nicht deterministisch sind. Es liegt möglicherweise in der Natur des Kalküls, dass es nicht deterministisch ist (denken Sie an gleichzeitige Kommunikationsprozesse), oder die Festlegung einer bestimmten Strategie kann sich nachteilig auf die Implementierungstechniken und die Optimierung auswirken.

Zum Beispiel ist der Kalkül eine Gleichungstheorie . Es gibt Ausdrücke und Gleichungen, die uns sagen, wann Ausdrücke gleich sind. Die Gleichungen sagen uns nicht , wie wir sie anwenden sollen, obwohl Menschen normalerweise versteckte Pläne haben und sie die Gleichungen präsentieren, damit sie später nützliche Bewertungsstrategien daraus ableiten können. Aber im Wesentlichen ist λ- Kalkül ein Bündel von Gleichungen. Es ist keine Programmiersprache.$\lambda$$\lambda$

Im Gegensatz dazu ist Standard ML eine Programmiersprache. Es wird in Bezug auf die operationale Semantik, dh die Berechnungsregeln, angegeben. Es gibt abgeleitete Gleichheitsbegriffe (Kontextgleichheit, Beobachtungsgleichheit usw.), die wir als eine Art Kalkül auffassen können.

Natürlich gibt es oft nützliche Zusammenhänge zwischen einem Kalkül und seiner Manifestation als Programmiersprache. Konfluente Normalisierung ist nur eine Möglichkeit, vom Kalkül in die Programmiersprache überzugehen (obwohl einige Menschen es leider zu einer Art Religion gemacht haben). Das Zusammenspiel von Kalkülen und Programmiersprachen ist wichtig: Die Programmiersprachen können tatsächlich verwendet werden, aber die Kalküle erklären, worum es in den Programmen geht.

Um die Leute zu ärgern, möchte ich auch festhalten, dass die Behauptung, dass es keinen Unterschied zwischen einem Kalkül und seiner operativen Manifestation gibt, manchmal zu verzerrten Ansichten über die Programmierung und Minireligionen innerhalb der Programmierergemeinschaft führt. Sie können versuchen zu erraten, welche Sprache ich im Sinn habe. (Es ist eine sehr coole Sprache!)

Das Ziel von Calculi ist es nicht nur, Programmäquivalenzen zu studieren, sondern Programme zu studieren. Ein Beispiel für ein ausgefallenes Kalkül ist dieses, bei dem die Strategie (Call-by-Value oder Call-by-Name) lokal festgelegt wird. Es könnte eines Tages in einer Programmiersprache implementiert werden, wird aber zuerst als Kalkül studiert. Sie verwenden auch Kalküle, um Typensysteme zu studieren (mit einigen Kalkülen wie der in der Martin-Löf-Typentheorie werden auch Typen berechnet).

Ich glaube, der Hauptunterschied ist, dass Kalküle formal (relativ) leicht zu lernen sein sollen, während Programmiersprachen (relativ) leicht zu bedienen sein sollen. Dies führt zu folgenden Unterschieden:

Kalküle sind in der Regel minimalistisch, während PLs in der Regel redundant sind (für Schleife, wenn Sie bereits eine while-Schleife haben, wechseln Sie, wenn Sie bereits eine if-Schleife haben, ...), um das Ausdrücken der gewünschten Elemente zu vereinfachen.

Kalküle haben eine vollständig spezifizierte Semantik, während eine PLs-Semantik häufig von einem Standardinterpreter / -compiler beschrieben wird.

Einige operationale Semantiken sind nicht deterministisch, da sie Folgendes ermöglichen:

• Um Dinge über alle "Subsemantics" zu beweisen.
• Die Implementierung wählen zu lassen und damit (vielleicht) die Dinge zu beschleunigen.
• Denn manchmal haben Sie eine "radnom ()" - Operation, und wenn Sie sich nicht für Wahrscheinlichkeiten interessieren, sondern nur für das, was möglich ist, ist Nichtdeterminismus eine gute Möglichkeit, sie darzustellen.

Beachten Sie, dass Call-by-Value nicht deterministisch ist: Sie können entweder die Funktion oder das Argument zuerst auswerten.

"Programmiersprache" und "Kalkül" sind polysemische Begriffe, das heißt, sie haben je nach Kontext unterschiedliche Bedeutungen.

In einigen Zusammenhängen haben sich Programmiersprachen und Kalküle auf dasselbe Konzept bezogen, nämlich ein Umschreibesystem, das auf einem Satz formaler Regeln basiert, die "mechanisch" angewendet werden können.

Der Grund, warum diese Konvergenz für uns gelegentlich rätselhaft ist (aber nicht für arbeitende Softwareentwickler oder Mathematiker), besteht darin, konkrete Programmiersprachen so zu konzipieren, als wären sie Kalküle, und Kalküle physikalisch in konkrete Programmiersprachen zu verkörpern.

Um Ihre Frage direkt zu beantworten, ist die Verwechslung von Kalkül und Programmiersprache (soweit vorhanden) kein Zufall, sondern ein Projekt. Unser Projekt. Es ist ein Beweis für unseren relativen Erfolg als wissenschaftliche Disziplin.