Wie hängen Programmiersprachen und Grundlagen der Mathematik zusammen?

Question

Grundsätzlich bin ich mir drei Grundlagen für Mathematik bewusst

1. Mengenlehre
2. Typentheorie
3. Kategoriestheorie

Inwiefern sind Programmiersprachen und Fundamente der Mathematik bezogen?

BEARBEITEN

Die ursprüngliche Frage lautete "Programmiersprachen basierend auf Grundlagen der Mathematik"

mit dem zusätzlichen Paragarph von

Und Implementierungen der Theorie
1. Geben Sie die Theorie ein Coq
2. Legen Sie die Theorie ein Setl
3. Kategorie -Theorie in Haskell

Basierend auf einem Vorschlag wurde dies in "Wie sind Programmiersprachen und Grundlagen der Mathematik im Zusammenhang mit dem Zusammenhang" geändert? "

Da dies eine dieser Fragen ist, wusste ich nicht genug über das, was ich gefragt habe, aber etwas lernen wollte, ich modifiziere die Frage, um es wertvoller für das Lernen und andere zu machen, aber die Details in der Lage, das nicht zu machen, um das nicht zu machen Aktuelle Antwort von Andrej Bauer scheinen das Thema zu sein.

Vielen Dank für alle Kommentare und die bisherige Antwort, ich lerne von ihnen.

Answer 1

Hinweis: Dieser Absatz ist jetzt veraltet.] Der Titel Ihrer Frage enthält eine ungerechtfertigte Annahme, nämlich dass Programmiersprachen "auf Grundlagen der Mathematik basieren". Dies ist im Allgemeinen nicht der Fall, obwohl die beiden Bereiche wichtige Beziehungen haben. Eine genauere Aussage wäre, dass (einige) Programmiersprachen mit grundlegenden Techniken entworfen wurden. Eine bessere Frage wäre "Wie hängen Programmiersprachen und Grundlagen der Mathematik zusammen?"

Die allgemeinste Verbindung ist im Slogan verkörpert Proofs-as-Programme, was dazu gebracht werden kann, auf verschiedene Weise zu arbeiten. Das Curry-Howard-Korrespondenz ist der offensichtlichste. Damit beziehen wir uns sofort typen Theorie, Logik und Programmierung. Es sollte jedoch betont werden, dass die Curry-Howard-Korrespondenz in Gegenwart einer allgemeinen Rekursion nicht sehr gut funktioniert (weil jeder Typ bewohnt wird), was jede allgemeine Programmiersprache unterstützt.

Eine subtilere Methode, um die Slogan-Proofs-as-programms funktionieren zu lassen, besteht darin, die Verwendung zu verwenden Realisierbarkeit. Auch hier beziehen wir Beweise und Programme, aber jetzt geht die Richtung von Beweisen zu Programmen: Jeder Beweis gibt ein Programm, aber nicht jedes Programm ist notwendigerweise ein Beweis.

Das Hauptbeispiel einer Programmiersprache, die auf einer Stiftung basiert, ist Agda, was einfach ist eine Implementierung der abhängigen Typtheorie. AGDA ist jedoch keine allgemeine Programmiersprache, da sie keine allgemeine Rekursion unterstützt. Jede Funktion in AGDA ist total und es gibt rechenbare Funktionen, die in AGDA nicht implementiert werden können. In der Praxis werden Programmierer dies nicht bemerken, aber sie werden feststellen, dass AGDA nicht undefinierte Werte zulässt, beispielsweise unendliche Schleifen.

Coq ist nicht Eine Programmiersprache, sondern ein Beweisassistent. Es hat jedoch auch Extraktionsfunktionen, die Programme aus Beweisen geben. Proof -Assistenten und Programmiersprachen sollten nicht miteinander verwechselt werden.

Das sollten wir nicht vergessen Prolog und andere Logikprogrammierung Sprachen lassen sich von der Idee inspirieren, die Berechnung ist eine Beweissuche. Dies bezieht sie natürlich eng mit der Logik.

Haskell ist eine allgemeine Programmiersprache, die auf Domain -Theorie. Das heißt, seine Semantik ist domänen-theoretisch, weil sie teilweise Funktionen und Rekursion berücksichtigen muss. Die Haskell -Community hat eine Reihe von Techniken entwickelt, die von der Kategorie -Theorie inspiriert wurden, von denen Monaden sind am bekanntesten, sollten aber nicht verwechselt werden mit Monaden. Im Allgemeinen werden fortschrittliche Programmiermerkmale normalerweise mit einer Kombination aus Domänentheorie und Kategorie -Theorie behandelt, aber dies ist nicht etwas, worüber der Haskell -Programmierer auf der Straße geschickt ist. Die sogenannte "syntaktische Kategorie" von Haskell-Typen ist die Sicht des Laiens, wie Haskell und Kategorie Theorie einander entsprechen.

Die festgelegte Theorie (klassisch oder konstruktiv) scheint in geringerem Maße Ideen in der Programmiersprache zu inspirieren. Natürlich hat die konstruktive festgelegte Theorie ihre Verbindung zur Programmierung durch konstruktive Logik. Eine wichtige Anwendung der intuitionistischen festgelegten Theorie auf Programmiersprachen wurde von Alex Simpson gegeben, der sie verwendet hat, um die Theorie der synthetischen Domänen zum Laufen zu bringen. Aber das ist ziemlich fortgeschrittenes Zeug, vielleicht sehen Diese Folien. Jean-Louis Krivine hat eine sehr interessante Marke der Realisierbarkeit für die klassische Set-Theorie entwickelt. Dies scheint eine gute Möglichkeit zu sein, die klassische Set -Theorie und -Programmierung in Beziehung zu setzen.

Zusammenfassend lässt sich sagen, dass die Theorie der Programmiersprachen grundlegende Techniken verwendet. Dies ist nicht überraschend, da wir die Berechnung als ein grundlegendes Konzept betrachten. Es ist jedoch zu naiv zu sagen, dass die Programmiersprachen auf bestimmten Grundlagen "basieren". Tatsächlich ist die Trichotomie der Grundlagen "Set-Theorie-Typ Theorie-Kategorie Theorie" wieder nur eine nützliche Beobachtung auf hoher Ebene, die auf verschiedene Weise mathematisch präzise gemacht werden kann, aber es ist nichts notwendig. Es ist ein historischer Unfall.

Answer 2

Dies ist ein sehr komplexes Thema und es gibt viele großartige Bücher zu diesem Thema, ein neuerer heißt Turings Kathedrale, Ursprünge des digitalen Universums und auch Motoren der Logik, Mathematiker und die Ursprünge des Computers.

Computersprachen haben sich über viele Jahrzehnte weiterentwickelt, aber ob Sie es glauben oder nicht, es gibt zwei originelle Programmiersprachen, die zeigen, dass Mathematik und Informatik eng miteinander verflochten sind:

• Turings 1936 Papier auf der Problem stoppen. Eine theoretische Konstruktion zur Lösung des von Hilbert vorgeschlagenen Problems um die Jahrhundertwende, die Entscheidungsproblem, dh ein automatisiertes Verfahren zur Lösung mathematischer Probleme!

• Lambda -Kalkül der Kirche gleichzeitig entwickelt überlebt immer noch in Sprachen wie lispeln und planen

Es gibt zwei Schlüsselfiguren, die sich mit den mathematischen und Informatikgrenzen von "Programmiersprachen" überschritten haben:

• Informationstheorie Pionierarbeit von Shannon Zeigt die tiefen Verbindungen zwischen Mathematik und Informatik

• Eine weitere Schlüsselfigur, die zwischen Mathematik und Informatik kreuzt, ist Von Neumann. Er erfand die von Neumann -Architektur des Speichers von Programmen im Gedächtnis.

Noch frühere "Programmiersprachen":

• Das englische Wort "Computer" bedeutete ursprünglich etwas mehr wie ein "Taschenrechner", der mathematische Operationen für Zahlen verwendete und seine Bedeutung hat sich erheblich auf das allgemeine Programmierkonzept von heute verschoben. Es besteht also eine Verbindung zwischen Programmiersprachen und frühen Taschenrechnern.
• Stanzkarten verwendet in Webstreifen Ab dem späten 19. und frühen 20. Jahrhundert waren eine "Programmiersprache" für das Webmuster. Beachten Sie, dass Punchkarten in den 1960er Jahren zum Programmieren von Mainframes verwendet wurden. Diese wurden ursprünglich als "Berechnungsmaschinen" (unter Verwendung von Mathematik!) Angesehen, nicht so sehr moderne, allgemeine Zwecke.
• Babbage und Ada Lovelace entwickelte die rudimentären frühen Konzepte von "Programmiersprachen" Mitte des 19. Jahrhunderts auf einer "berechnenden Engine"
• boolsche Algebra war ursprünglich ein rein mathematisches Konzept, das von Boole erfunden wurde
• die Antike (Millenia alt) Abakus Für die mathematische Berechnung wird als Vorläufer des modernen Computers angesehen. Es könnte jedoch gesagt werden, dass Operationen zur Manipulation eine Art "Programmiersprache" waren (gefolgt von Menschen)

In modernen Programmiersprachen, mit denen die Abstraktion zugenommen und skaliert hat, hat die klare, direkte Verbindung zur Mathematik im Laufe der Jahrzehnte etwas abgenommen, aber es wird immer ziemlich intrinsisch und in gewisser Weise gestärkt. Zum Beispiel haben Sprachen wie Java mit seinen strengen Typen Verbindungen zur Mathematik, und Anfang der späten ~ 1990er Mainstream-Computersprachen (z. B. C ++, Java, Ruby usw.) wurden explizit viele mathematische höhere Objekte als nahe Primitive in der implementierten Sprachen wie Sets, Bäume (z. B. Brees oder Hashmaps) usw.