Der Deep Link zur Gleichsetzung von mathematischen Beweisen und Computerprogrammen | Quanta-Magazin

Einige wissenschaftliche Entdeckungen sind wichtig, weil sie etwas Neues enthüllen – zum Beispiel die Doppelhelixstruktur der DNA oder die Existenz von Schwarzen Löchern. Einige Enthüllungen sind jedoch tiefgreifend, weil sie zeigen, dass zwei alte Konzepte, die einst als verschieden galten, tatsächlich dieselben sind. Nehmen Sie die Gleichungen von James Clerk Maxwell, die zeigen, dass Elektrizität und Magnetismus zwei Aspekte eines einzigen Phänomens sind, oder die Verknüpfung der Schwerkraft mit einer gekrümmten Raumzeit durch die Allgemeine Relativitätstheorie.

Die Curry-Howard-Korrespondenz tut dasselbe, allerdings in größerem Maßstab, indem sie nicht nur einzelne Konzepte innerhalb eines Fachgebiets, sondern ganze Disziplinen miteinander verknüpft: Computerwissenschaften und mathematische Logik. Auch bekannt als Curry-Howard-Isomorphismus (ein Begriff, der bedeutet, dass zwischen zwei Dingen eine Eins-zu-eins-Entsprechung besteht) stellt er eine Verbindung zwischen mathematischen Beweisen und Computerprogrammen her.

Einfach ausgedrückt geht der Curry-Howard-Korrespondenz davon aus, dass zwei Konzepte aus der Informatik (Typen und Programme) jeweils äquivalent zu Sätzen und Beweisen sind – Konzepte aus der Logik.

Eine Konsequenz dieser Korrespondenz ist, dass das Programmieren – oft als persönliches Handwerk angesehen – auf die idealisierte Ebene der Mathematik erhoben wird. Das Schreiben eines Programms ist nicht nur „Codieren“, es wird zum Beweis eines Theorems. Dies formalisiert den Akt des Programmierens und bietet Möglichkeiten, mathematisch über die Korrektheit von Programmen nachzudenken.

Die Korrespondenz ist nach den beiden Forschern benannt, die sie unabhängig voneinander entdeckt haben. Im Jahr 1934 bemerkte der Mathematiker und Logiker Haskell Curry eine Ähnlichkeit zwischen Funktionen in der Mathematik und der Implikationsbeziehung in der Logik, die die Form von „Wenn-Dann“-Aussagen zwischen zwei Sätzen annimmt.

Inspiriert durch Currys Beobachtung entdeckte der mathematische Logiker William Alvin Howard 1969 einen tieferen Zusammenhang zwischen Berechnung und Logik und zeigte, dass das Ausführen eines Computerprogramms der Vereinfachung eines logischen Beweises sehr ähnlich ist. Wenn ein Computerprogramm ausgeführt wird, wird jede Zeile „ausgewertet“, um eine einzelne Ausgabe zu erhalten. Ebenso beginnen Sie bei einem Beweis mit komplexen Aussagen, die Sie vereinfachen können (indem Sie beispielsweise überflüssige Schritte eliminieren oder komplexe Ausdrücke durch einfachere ersetzen), bis Sie zu einer Schlussfolgerung gelangen – einer komprimierteren und prägnanteren Aussage, die aus vielen Zwischenaussagen abgeleitet wird .

Während diese Beschreibung einen allgemeinen Sinn für die Korrespondenz vermittelt, müssen wir, um sie vollständig zu verstehen, etwas mehr über das lernen, was Informatiker „Typentheorie“ nennen.

Beginnen wir mit einem berühmten Paradoxon: In einem Dorf lebt ein Friseur, der alle Männer rasiert, die sich nicht selbst rasieren, und nur sie. Rasiert sich der Friseur? Wenn die Antwort „Ja“ lautet, darf er sich nicht rasieren (weil er nur Männer rasiert, die sich nicht selbst rasieren). Wenn die Antwort „Nein“ lautet, muss er sich rasieren (denn er rasiert alle Männer, die sich nicht rasieren). Dies ist eine informelle Version eines Paradoxons, das Bertrand Russell entdeckte, als er versuchte, die Grundlagen der Mathematik mithilfe eines Konzepts namens Mengen zu begründen. Das heißt, es ist unmöglich, eine Menge zu definieren, die alle Mengen enthält, die sich selbst nicht enthalten, ohne auf Widersprüche zu stoßen.

Um dieses Paradoxon zu vermeiden, können wir, wie Russell zeigte, „Typen“ verwenden. Grob gesagt handelt es sich hierbei um Kategorien, deren spezifische Werte als Objekte bezeichnet werden. Wenn es beispielsweise einen Typ namens „Nat“ gibt, der natürliche Zahlen bedeutet, sind seine Objekte 1, 2, 3 usw. Forscher verwenden normalerweise einen Doppelpunkt, um den Typ eines Objekts anzugeben. Die Zahl 7 vom Typ Ganzzahl kann als „7: Ganzzahl“ geschrieben werden. Sie können eine Funktion haben, die ein Objekt vom Typ A nimmt und ein Objekt vom Typ B ausspuckt, oder eine Funktion, die ein Paar von Objekten vom Typ A und Typ B zu einem neuen Typ namens „A × B“ kombiniert.

Eine Möglichkeit, das Paradoxon zu lösen, besteht daher darin, diese Typen in eine Hierarchie einzuordnen, sodass sie nur Elemente einer „niedrigeren Ebene“ als sie selbst enthalten können. Dann kann ein Typ sich nicht selbst enthalten, wodurch die Selbstreferenzialität vermieden wird, die das Paradoxon erzeugt.

In der Welt der Typentheorie kann der Beweis, dass eine Aussage wahr ist, anders aussehen, als wir es gewohnt sind. Wenn wir beweisen wollen, dass die ganze Zahl 8 gerade ist, müssen wir zeigen, dass 8 tatsächlich ein Objekt eines bestimmten Typs namens „Gerade“ ist, bei dem die Zugehörigkeitsregel darin besteht, durch 2 teilbar zu sein. Nachdem wir überprüft haben, dass 8 teilbar ist Aus 2 können wir schließen, dass 8 tatsächlich ein „Einwohner“ vom Typ Even ist.

Curry und Howard zeigten, dass Typen grundsätzlich äquivalent zu logischen Aussagen sind. Wenn eine Funktion einen Typ „bewohnt“ – das heißt, wenn Sie erfolgreich eine Funktion definieren können, die ein Objekt dieses Typs ist –, zeigen Sie effektiv, dass die entsprechende Aussage wahr ist. Funktionen, die eine Eingabe vom Typ A annehmen und eine Ausgabe vom Typ B liefern, die als Typ A → B bezeichnet wird, müssen also einer Implikation entsprechen: „Wenn A, dann B.“ Nehmen Sie zum Beispiel den Satz „Wenn es regnet, ist der Boden nass.“ In der Typentheorie würde dieser Satz durch eine Funktion vom Typ „Raining → GroundIsWet“ modelliert. Die unterschiedlich aussehenden Formulierungen sind mathematisch tatsächlich gleich.

So abstrakt diese Verknüpfung auch klingen mag, sie hat nicht nur die Art und Weise verändert, wie Mathematik- und Informatikpraktiker über ihre Arbeit denken, sondern auch zu mehreren praktischen Anwendungen in beiden Bereichen geführt. Für die Informatik bietet es eine theoretische Grundlage für die Softwareverifizierung, den Prozess zur Sicherstellung der Korrektheit von Software. Indem Programmierer gewünschtes Verhalten in Form logischer Aussagen formulieren, können sie mathematisch beweisen, dass sich ein Programm wie erwartet verhält. Es bietet außerdem eine solide theoretische Grundlage für den Entwurf leistungsfähigerer funktionaler Programmiersprachen.

Und für die Mathematik hat die Korrespondenz zur Geburt von geführt Beweisassistenten, auch interaktive Theorembeweiser genannt. Hierbei handelt es sich um Softwaretools, die bei der Erstellung formaler Beweise helfen, wie z. B. Coq und Lean. In Coq ist jeder Schritt des Beweises im Wesentlichen ein Programm, und die Gültigkeit des Beweises wird mit Typprüfalgorithmen überprüft. Mathematiker haben auch Beweisassistenten eingesetzt – insbesondere die Lean-Theorem-Beweiser – die Mathematik zu formalisieren, was die Darstellung mathematischer Konzepte, Theoreme und Beweise in einem strengen, computerüberprüfbaren Format beinhaltet. Dadurch kann die manchmal informelle Sprache der Mathematik von Computern überprüft werden.

Forscher erforschen immer noch die Konsequenzen dieser Verbindung zwischen Mathematik und Programmierung. Die ursprüngliche Curry-Howard-Korrespondenz verschmilzt Programmierung mit einer Art Logik, die als intuitionistische Logik bezeichnet wird, aber es stellt sich heraus, dass auch andere Arten von Logik für solche Vereinheitlichungen geeignet sein könnten.

„Was in dem Jahrhundert seit Currys Erkenntnis passiert ist, ist, dass wir immer mehr Fälle entdecken, in denen ‚logisches System X dem Rechensystem Y entspricht‘“, sagte er Michael Clarkson, Informatiker an der Cornell University. Forscher haben die Programmierung bereits mit anderen Arten der Logik verknüpft, beispielsweise mit der linearen Logik, die das Konzept der „Ressourcen“ umfasst, und der Modallogik, die sich mit Konzepten von Möglichkeit und Notwendigkeit befasst.

Und obwohl diese Korrespondenz Currys und Howards Namen trägt, sind sie keineswegs die Einzigen, die sie entdeckt haben. Dies zeugt vom grundlegenden Charakter der Korrespondenz: Die Leute nehmen sie immer wieder wahr. „Es scheint kein Zufall zu sein, dass zwischen Berechnung und Logik eine enge Verbindung besteht“, sagte Clarkson.