Wie hängen Programmiersprachen und Grundlagen der Mathematik zusammen?

Grundsätzlich sind mir drei Grundlagen für Mathematik bekannt

1. Mengenlehre
2. Typentheorie
3. Kategorietheorie

Inwiefern hängen Programmiersprachen und Grundlagen der Mathematik zusammen?

BEARBEITEN

Die ursprüngliche Frage lautete "Programmiersprachen, die auf mathematischen Grundlagen basieren".

mit der zusätzlichen Paragrafie von

Und Implementierungen der Theorie
1. Typentheorie in Coq
2. Mengen-Theorie in SETL
3. Kategorietheorie in Haskell

Aufgrund eines Vorschlags wurde dies geändert zu "Wie hängen Programmiersprachen und Grundlagen der Mathematik zusammen?"

Da dies eine dieser Fragen ist, bei denen ich nicht genug über meine Fragen wusste, aber etwas lernen wollte, ändere ich die Frage, um sie für das Lernen und andere wertvoller zu machen, ohne die Details zu belassen, um das zu ändern Die aktuelle Antwort von Andrej Bauer scheint vom Thema abzulenken.

Vielen Dank für all die Kommentare und die Antwort, die ich bisher von ihnen gelernt habe.

[Anmerkung: Diese Absätze sind 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 in dem Slogan Proofs-as-Programme enthalten , der auf verschiedene Arten zum Funktionieren gebracht werden kann. Die Curry-Howard-Korrespondenz ist die offensichtlichste. Damit verbinden wir gleichzeitig Typentheorie, Logik und Programmierung. Es sollte jedoch betont werden, dass die Curry-Howard-Korrespondenz bei allgemeiner Rekursion (da jeder Typ bewohnt wird), die von jeder allgemeinen Programmiersprache unterstützt wird, nicht sehr gut funktioniert.

Eine subtilere Möglichkeit, den Slogan Proofs-as-Programs zum Laufen zu bringen, ist die 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 wichtigste Beispiel einer Programmiersprache auf einem Fundament basiert Agda , die einfach ist eine Implementierung von abhängiger Typ Theorie. Agda ist jedoch keine Allzweck-Programmiersprache, da sie keine allgemeine Rekursion unterstützt. Jede Funktion in Agda ist total, und es gibt berechenbare Funktionen, die in Agda nicht implementiert werden können. In der Praxis werden Programmierer dies nicht bemerken, aber sie werden bemerken, dass Agda keine undefinierten Werte zulässt, zum Beispiel Endlosschleifen.

Coq ist keine Programmiersprache, sondern ein Proof-Assistent. Es verfügt jedoch auch über Extraktionsfunktionen, mit denen Programme aus Proofs erstellt werden können. Proof-Assistenten und Programmiersprachen sollten nicht miteinander verwechselt werden.

Wir sollten diesen Prolog und andere nicht vergessen logische Programmiersprachen von der Idee inspirieren lassen, dass Rechnen eine Beweissuche ist . Damit sind sie natürlich eng mit der Logik verbunden.

Haskell ist eine universelle Programmiersprache, die auf der Domänentheorie basiert . Das heißt, ihre Semantik ist domänentheoretisch, weil sie Teilfunktionen und Rekursionen berücksichtigen muss. Die Haskell-Community hat eine Reihe von Techniken entwickelt, die von der Kategorietheorie inspiriert sind, darunter auch Monaden sind. sind am bekanntesten, sollten aber nicht mit Monaden verwechselt werden . Im Allgemeinen werden fortgeschrittene Programmierfunktionen in der Regel mit einer Kombination aus Domänentheorie und Kategorietheorie behandelt, aber das ist etwas, mit dem der Haskell-Programmierer auf der Straße nicht vertraut ist. Die sogenannte "syntaktische Kategorie" von Haskell-Typen ist eine Sichtweise eines Laien, wie Haskell und Kategorietheorie einander entsprechen.

Mengenlehre (klassisch oder konstruktiv) scheint in geringerem Maße Ideen in der Programmiersprache anzuregen. Natürlich hat die konstruktive Mengenlehre ihre Verbindung zur Programmierung durch konstruktive Logik. Eine wichtige Anwendung der intuitionistischen Mengenlehre auf Programmiersprachen gab Alex Simpson, der sie verwendete, um die Theorie der synthetischen Domänen funktionieren zu lassen. Aber das ist ziemlich fortgeschrittenes Zeug, vielleicht sehen Sie diese Folien . Jean-Louis Krivine hat eine sehr interessante Marke der Realisierbarkeit für die klassische Mengenlehre entwickelt. Dies scheint ein guter Weg zu sein, um klassische Mengenlehre und Programmierung in Beziehung zu setzen.

Zusammenfassend verwendet die Theorie der Programmiersprachen grundlegende Techniken. Dies ist nicht überraschend, da wir die Berechnung als ein grundlegendes Konzept betrachten. Es ist jedoch zu naiv zu sagen, dass Programmiersprachen auf einer bestimmten Grundlage "basieren". Tatsächlich ist die Trichotomie der Grundlagen "Mengenlehre - Typentheorie - Kategorietheorie" wieder nur eine nützliche Beobachtung auf hoher Ebene, die auf verschiedene Arten mathematisch präzise gemacht werden kann, aber es gibt nichts Notwendiges daran. Es ist ein historischer Unfall.

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

Computersprachen haben sich über viele Jahrzehnte entwickelt, aber es gibt zwei originale Programmiersprachen, die zeigen, dass Mathematik und Informatik eng miteinander verbunden sind:

• Turings Artikel von 1936 über das Problem des Stillstands . ein theoretisches Konstrukt , das Problem von Hilbert an der Wende des Jahrhunderts, die vorgeschlagene zu lösen Entscheidungsproblem , also ein automatisiertes Verfahren zur Lösung mathematische Probleme!

• Die zur gleichen Zeit entwickelte Lambda-Rechnung der Kirche ist in Sprachen wie Lisp und Schema noch erhalten

Es gibt zwei Schlüsselfiguren, die in "Programmiersprachen" die Grenzen von Mathematik und Informatik überschritten haben:

• Die von Shannon entwickelte Informationstheorie zeigt die tiefe Verbindung zwischen Mathematik und Informatik

• Eine weitere Schlüsselfigur zwischen Mathematik und Informatik ist Von Neumann . er erfand die von neumann architektur, programme im speicher abzulegen.

noch frühere "Programmiersprachen":

• Das englische Wort "Computer" bedeutete ursprünglich eher etwas wie ein "Taschenrechner", der mathematische Operationen mit Zahlen verwendete, und seine Bedeutung hat sich wesentlich zum allgemeinen Programmierkonzept von heute verlagert. es besteht also eine Verbindung zwischen Programmiersprachen und frühen Taschenrechnern.
• Lochkarten für Webstühle aus dem späten 19. und frühen 20. Jahrhundert verwendet wurden, waren eine "Programmiersprache" für Webmuster. Beachten Sie, dass Lochkarten in den 1960er Jahren häufig für die Programmierung von Großrechnern verwendet wurden. Diese wurden ursprünglich als "Rechenmaschinen" (unter Verwendung von Mathematik!) angesehen, weniger als moderne Allzweckcomputer.
• Babbage und Ada Lovelace entwickelten die rudimentären frühen Konzepte von "Programmiersprachen" Mitte des 19. Jahrhunderts auf einer "Rechenmaschine".
• boolsche Algebra war ursprünglich ein rein mathematisches Konzept, das von Boole erfunden wurde
• Der uralte (Jahrtausende alte) Abakus für mathematische Berechnungen gilt als Vorläufer des modernen Computers. aber man könnte sagen, dass Operationen zur Manipulation eine Art "Programmiersprache" waren (gefolgt von Menschen)

In modernen Programmiersprachen hat sich die klare, direkte Verbindung zur Mathematik im Laufe der Jahrzehnte etwas verringert, da die Abstraktion zugenommen und zugenommen hat. In mancher Hinsicht hat sie sich jedoch immer weiter verstärkt. Zum Beispiel haben Sprachen wie Java mit ihren strengen Typen Verbindungen zur Mathematik, und in den späten 1990er Jahren haben die gängigen Computersprachen (z. B. c ++, Java, Ruby usw.) damit begonnen, viele mathematisch übergeordnete Objekte explizit als Nahe-Primitive in das zu implementieren Sprachen wie Sets, Bäume (zB Btrees oder Hashmaps) usw.