Die tiefe Verbindung zwischen mathematischer Logik und Computerprogrammcode: Spiegelbilder voneinander

Manchen wissenschaftlichen Entdeckungen wird große Bedeutung beigemessen, weil etwas Neues enthüllt wird, etwa die Doppelhelixstruktur der DNA oder die Existenz von Schwarzen Löchern. Aber diese Offenbarungen haben eine tiefere Bedeutung, denn sie zeigen, dass zwei alte Konzepte, die zuvor sehr unterschiedlich schienen, tatsächlich dieselben sind. Beispielsweise zeigte das von James Clerk Maxwell entdeckte Gleichungssystem, dass Elektrizität und Magnetismus zwei verschiedene Aspekte desselben Phänomens sind, während die allgemeine Relativitätstheorie die Schwerkraft mit der gekrümmten Raumzeit verknüpfte.

Das Gleiche gilt für die Curry-Howard-Korrespondenz, und sie bezieht sich nicht nur auf zwei verschiedene Konzepte in einem Bereich, sondern auf zwei komplette Disziplinen: Informatik und mathematische Logik. Diese Entsprechung wird auch als Curry-Howard-Isomorphismus bezeichnet (Isomorphismus bezieht sich auf eine bestimmte Eins-zu-Eins-Entsprechung zwischen zwei Dingen), die einen bestimmten Zusammenhang zwischen mathematischen Beweisen und Computerprogrammen herstellt.

Einfach ausgedrückt geht die Currie-Howard-Korrespondenz davon aus, dass zwei Konzepte in der Informatik (Typen und Programme) zwei Konzepten in der Logik (Sätze und Beweise) entsprechen.

Ein Ergebnis dieser Korrespondenz ist, dass die Programmentwicklung auf ein idealisiertes mathematisches Niveau gehoben wurde, während früher normalerweise angenommen wurde, dass Programmentwicklung nur eine Handwerksarbeit sei. Bei der Programmentwicklung geht es nicht nur um das „Schreiben von Code“, sie ist zum Beweis von Theoremen geworden. Dies formalisiert das Verhalten der Programmentwicklung und bietet eine Möglichkeit, mathematisch über die Programmkorrektheit nachzudenken.

Der Name dieser Korrespondenz stammt von zwei Forschern, die diese Korrespondenz unabhängig voneinander entdeckt haben. Im Jahr 1934 bemerkte der Mathematiker und Logiker Haskell Curry die Ähnlichkeit zwischen Funktionen in der Mathematik und der Implikationsbeziehung in der Logik. Die Form einer Implikationsrelation ist eine „Wenn-Dann“-Aussage zwischen zwei Aussagen.

Inspiriert durch Curries Beobachtungen entdeckte der mathematische Logiker William Alvin Howard 1969 einen tieferen Zusammenhang zwischen Berechnung und Logik: Computerprogramme ähneln stark vereinfachten Logikbeweisen. Wenn Sie ein Computerprogramm ausführen, wird jede Codezeile „ausgewertet“, um eine Ausgabe zu erzeugen. Wenn Sie an einem Beweis arbeiten, beginnen Sie in ähnlicher Weise mit einer komplexen Aussage und vereinfachen diese dann (z. B. indem Sie überflüssige Schritte eliminieren oder komplexe Ausdrücke durch einfachere ersetzen), bis Sie zu einer Schlussfolgerung gelangen – von vielen aus. Eine Übergangsaussage führt zu einer prägnanteren Stellungnahme.

Obwohl diese Beschreibung eine ungefähre Vorstellung davon vermittelt, was diese Korrespondenz bedeutet, erfordert das vollständige Verständnis mehr darüber, was Informatiker als „Typentheorie“ bezeichnen.

Beginnen wir mit einem berühmten Paradoxon: Es gab einen Friseur in einem Dorf, der sich nur für alle rasierte, die sich nicht selbst rasierten. Rasiert sich dieser Friseur also? Wenn die Antwort „Ja“ lautet, darf er sich nicht rasieren (denn er rasiert sich nur für Menschen, die sich nicht selbst rasieren). Wenn die Antwort „Nein“ lautet, muss er sich rasieren (denn er rasiert jeden, der sich nicht selbst rasiert). Dies ist eine informelle Version eines Paradoxons, das Bertrand Russell entdeckte, als er versuchte, mithilfe eines Konzepts namens Mengen die Grundlage der Mathematik zu schaffen. Das heißt: Es ist unmöglich, eine Menge zu definieren, die alle Mengen enthält, die sich nicht selbst enthalten, und bei diesem Prozess treten zwangsläufig Widersprüche auf.

Russells Forschung zeigt, dass wir Typen verwenden können, um dieses Paradoxon zu vermeiden. Grob gesagt sind Typen Kategorien, deren konkrete Werte Objekte genannt werden. Wenn es beispielsweise einen Typ Nat gibt, der natürliche Zahlen darstellt, dann sind seine Objekte 1, 2, 3 usw. Forscher verwenden häufig Doppelpunkte, um die Art des Objekts anzugeben. Für den Ganzzahltypwert 7 kann er beispielsweise als „7: Ganzzahl“ geschrieben werden. Wir können eine Funktion verwenden, um ein Objekt vom Typ A in ein Objekt vom Typ B umzuwandeln, oder wir können eine Funktion verwenden, um zwei Objekte vom Typ A und B zu einem neuen Objekt vom Typ „A×B“ zu kombinieren.

Um dieses Paradox zu lösen, besteht eine Möglichkeit darin, diese Typen so zu schichten, dass sie nur Elemente enthalten, die eine Ebene unter sich selbst liegen. Dann kann ein Typ sich nicht selbst enthalten, wodurch die Selbstreferenz vermieden wird, die das obige Paradoxon erzeugt.

In der Welt der Typentheorie kann der Prozess des Beweises, dass eine Aussage wahr ist, anders sein, als wir es gewohnt sind. Wenn wir beweisen wollen, dass die ganze Zahl 8 gerade ist, dann besteht der Schlüssel zum Problem darin, zu beweisen, dass 8 tatsächlich ein Objekt vom Typ „gerade“ ist und die Regel dieses Typs definiert, dass die Elemente durch 2 teilbar sind. Nachdem wir überprüft haben, dass 8 durch 2 teilbar ist, können wir daraus schließen, dass 8 ein „Resident“ vom Typ „gerade“ ist.

Currie und Howard haben bewiesen, dass Typen grundsätzlich äquivalent zu logischen Aussagen sind. Wenn eine Funktion einen bestimmten Typ „bewohnt“, das heißt, wenn die Funktion ein Objekt dieses Typs ist, können wir effektiv beweisen, dass die entsprechende Aussage wahr ist. Daher muss eine Funktion, die ein Objekt vom Typ A als Eingabe und ein Objekt vom Typ B als Ausgabe (bezeichnet als Typ A→B) verwendet, einer Implikation entsprechen: „Wenn A, dann B.“ Angenommen, es gibt das Satz „Wenn es regnet, dann ist der Boden nass.“ In der Typentheorie wird dieser Satz als Funktion des Typs „Regen → Boden ist nass“ modelliert. Diese beiden Darstellungen sehen unterschiedlich aus, sind aber mathematisch gleich.

Obwohl dieser Zusammenhang abstrakt erscheinen mag, verändert er nicht nur die Art und Weise, wie Mathematik- und Informatikpraktiker über ihre Arbeit denken, sondern führt auch zu einigen praktischen Anwendungen in beiden Bereichen. In der Informatik bildet dieser Zusammenhang eine theoretische Grundlage für die Softwareverifikation, den Prozess der Sicherstellung der Softwarekorrektheit. Durch die Beschreibung des gewünschten Verhaltens anhand logischer Aussagen können Programmentwickler mathematisch nachweisen, ob sich ein Programm wie erwartet verhält. Und dieser Zusammenhang bietet auch eine solide theoretische Grundlage für den Entwurf leistungsfähigerer funktionaler Programmiersprachen.

Im Bereich der Mathematik hat diese Korrespondenz zur Entstehung des Beweisassistenten geführt, der auch als interaktiver Theorembeweis bekannt ist. Diese Softwaretools können bei der Erstellung formaler Beweise helfen, Beispiele hierfür sind Coq und Lean. In Coq ist jeder Beweisschritt im Wesentlichen ein Programm, und die Gültigkeit des Beweises wird durch einen Typprüfungsalgorithmus überprüft. Mathematiker haben auch Beweisassistenten (insbesondere Lean-Theorembeweiser) eingesetzt, um die Mathematik zu formalisieren. Dazu gehört die Darstellung mathematischer Konzepte, Theoreme und Beweise in einem strengen Format, das von einem Computer überprüft werden kann. Dadurch können manchmal informelle mathematische Sprachen von Computern getestet werden.

Forscher erforschen auch die möglichen Ergebnisse dieser Verbindung zwischen Mathematik und Programmierung. Die ursprüngliche Curry-Howard-Korrespondenz verband die Programmentwicklung mit einer Art von Logik, die als intuitionistische Logik bezeichnet wird, aber es stellt sich heraus, dass es noch viele weitere Arten von Logik gibt, die vereinheitlicht werden können.

Der Informatiker der Cornell University, Michael Clarkson, sagte: „In dem Jahrhundert, seit Currie seine Erkenntnisse erlangte, haben wir immer mehr Fälle von ‚Logiksystem X entspricht Rechensystem Y‘ gefunden.“ Forschungsautoren haben auch die Programmierung verknüpft zu anderen Arten der Logik, wie etwa der linearen Logik, die das Konzept der „Ressourcen“ umfasst, und der modalen Logik, die die Konzepte der Möglichkeit und Notwendigkeit umfasst.

Und obwohl dieser Briefwechsel den Namen Curry und Howard trägt, sind sie keineswegs die einzigen Entdecker dieses Briefwechsels. Dies zeigt die grundlegende Natur dieser Korrespondenz: Menschen nehmen sie immer wieder wahr. Clarkson sagte: „Die tiefe Verbindung zwischen Informatik und Logik scheint kein Zufall zu sein.“

Das obige ist der detaillierte Inhalt vonDie tiefe Verbindung zwischen mathematischer Logik und Computerprogrammcode: Spiegelbilder voneinander. Für weitere Informationen folgen Sie bitte anderen verwandten Artikeln auf der PHP chinesischen Website!