Unter der Curry-Howard-Korrespondenz oder locker "Beweise-als-Programme", haben wir auch "Programme-als-Beweise" und was würde einige Arb. Programm beweisen?

Ja. Aber in der Regel sind die dazugehörigen Beweise uninteressant.

Denken Sie daran, dass wir unter der Korrespondenz haben

• Typen$\longleftrightarrow$Vorschläge
• Programme$\longleftrightarrow$Beweise

Schauen wir uns also Ihren Beispielcode an. Wir bekommen eine Funktion$\mathtt{gcd} : \mathbb{N} \times \mathbb{N} \to \mathbb{N}$. Mit eben diesem Typ beweist sich das Programm

„Wenn es ein Element von gibt$\mathbb{N} \times \mathbb{N}$, dann gibt es ein Element von$\mathbb{N}$"

ein völlig uninteressantes Theorem, ich denke, Sie würden mir zustimmen. Vor allem die einfache Funktion$\pi_2 (x,y) = y$, die auch einen Typ hat$\mathbb{N} \times \mathbb{N} \to \mathbb{N}$beweist denselben Satz. Warum? Weil es sich um zwei Funktionen des gleichen Typs handelt!

Nun, offensichtlich der Code für$\mathtt{gcd}$etwas Interessantes tut, also erweist es sich sicherlich als etwas Interessanteres als das Naive$\pi_2$Funktion. Die Antwort auf diese Frage hängt davon ab, wie ausdrucksstark Ihr Typsystem ist. Wenn Sie nur Zugriff auf einen Typ haben$\mathbb{N}$, dann hast du leider Pech. Aber zum Glück können wir durch die Sprache der abhängigen Typen über interessantere Typen und damit interessantere Aussagen sprechen.

In der Welt der Softwareentwicklung verwenden wir Typen, um das gewünschte Verhalten eines Programms auszudrücken . Typen entsprechen Spezifikationen für Programme.

Auf der einfachsten Ebene sagen sie Ihnen, welche Eingaben und Ausgaben eine bestimmte Funktion erwartet, aber mit abhängigen Typen können wir das gewünschte Verhalten einer Funktion vollständig klassifizieren. Zum Beispiel könnte die naive Art von Mergesort sein

alles, was wir sehen, ist, dass es eine Liste von Dingen des Typs enthält$a$und spuckt eine Liste von Dingen des Typs aus$a$. Aber auch dies ist keine interessante Spezifikation. Die Identitätsfunktion oder sogar die Funktion, die ihre Eingabe ignoriert und die leere Liste zurückgibt, bewohnen ebenfalls diesen Typ. Und wieder, da Typen Sätze sind, sehen wir das$\mathtt{mergesort}$beweist eine sehr uninteressante Aussage: "Wenn eine Liste von$a$s existiert, dann eine Liste von$a$s existiert .... wie .... ja, offensichtlich.

Also peppen wir unser Typensystem auf und sehen uns stattdessen so etwas an:

Ich verzichte auf einige Syntax und eine formale Definition von$\mathtt{isSorted} : [a] \to \mathtt{Bool}$, aber hoffentlich ist klar, wie man eine solche Funktion schreibt.

Also jetzt$\mathtt{mergesort}$muss eine strengere Spezifikation erfüllen. Es ist nicht erlaubt, eine Liste von zurückzugeben$a$S. Es muss eine sortierte Liste von zurückgegeben werden$a$S. Als Funktion dieses Typs$\mathtt{mergesort}$beweist

„Wenn eine Liste von$a$s existiert, dann eine sortierte Liste von$a$s existiert"

Auch dies ist kein bahnbrechendes Theorem, aber es ist besser als das, was wir zuvor hatten.

Leider entspricht die konstante leere Listenfunktion immer noch dieser Spezifikation. Immerhin ist die leere Liste (leer) sortiert! Aber wir können wieder gehen. Vielleicht schreiben wir so einen Typ$\mathtt{mergesort}$beweist

„Wenn eine Liste von$a$s existiert, dann gibt es eine sortierte Liste von$a$s mit genau den gleichen Elementen"

was als Vorschlag ein bisschen interessanter wird. Dies legt nun das gewünschte Verhalten von Mergesort fest. Überlegen Sie außerdem, wie Sie eine solche Behauptung beweisen würden. Wenn jemand sagte "beweise, dass eine sortierte Liste mit denselben Elementen existiert", würdest du sagen "sortiere sie einfach!" und das ist genau der Beweis dafür$\mathtt{mergesort}$bietet.

Was dann, von Ihrem$\mathtt{gcd}$Beispiel? Nun, wie bei$\mathtt{mergesort}$, funktioniert dasselbe Programm, um mehrere Dinge zu beweisen. Es ist wirklich der Typ , der zählt. Mit ein wenig Arbeit könnte Ihr Code ein Beweis dafür sein

„Wenn es zwei natürliche Zahlen gibt, dann gibt es eine natürliche Zahl, die beide teilt, die größer ist als jede andere natürliche Zahl, die beide teilt“

das beginnt, wie ein interessanter (wenn auch grundlegender) mathematischer Satz auszusehen!

Ich hoffe das hilft ^_^

Die Curry-Howard-Korrespondenz kann sowohl als „Beweise-als-Programme“ als auch als „Programme-als-Beweise“ angesehen werden, vorausgesetzt, wir spezifizieren, was die Logik für Beweise und die Sprache für Programme sind.

Die ursprüngliche Formulierung der Curry-Howard-Korrespondenz besteht zwischen Beweisen in einer bestimmten Logik (das implikationale Fragment der intuitionistischen Logik, auch bekannt als minimale Logik) und Programmen in einer bestimmten Sprache (einfach getippt$\lambda$-Rechnung ). Später wurde die Korrespondenz auf andere Logiken und Sprachen ausgedehnt (z. B. Minimallogik mit Implikation und Konjunktion und einfach getippt$\lambda$-Rechnen mit Paaren; Klassische Logik u$\lambda\mu$-Rechnung ; usw.).

Ein entscheidender Punkt ist, dass die "Programmiersprache" in keiner Version der Curry-Howard-Korrespondenz Turing-vollständig sein kann . Tatsächlich ist die Logik, in der Beweise geschrieben werden, kohärent, und in der Beweistheorie bedeutet dies, dass ein Theorem namens Cut-Elimination oder Normalisierung gilt, das impliziert, dass jedes in der entsprechenden "Programmiersprache" geschriebene Programm seine Ausführung beenden muss. Nun ist bekannt, dass eine Sprache, die es uns nicht erlaubt, ein Programm zu schreiben, das sich endlos wiederholt, nicht Turing-vollständig ist.

Um Ihre spezielle Frage zu beantworten, das von Ihnen geschriebene Programm enthält das whileKonstrukt, das Endlosschleifen erzeugen kann, daher kann es keine logische Interpretation im Sinne von Curry-Howard haben, dh es entspricht keinem Beweis in irgendeiner Logik.

Es stimmt, dass es einige Problemumgehungen für diese Einschränkung gibt. Als Programmiersprache können wir zum Beispiel einfach typisiert betrachten$\lambda$-Kalkül mit einem Fixpunkt-Kombinator, der Turing-vollständig ist (siehe auch eine Diskussion hier ). Bei dieser Variante wird der einfach getippt$\lambda$-Kalkül whilekann das Konstrukt kodiert werden. Aber was ist der logische Inhalt einer solchen Programmiersprache aus der Curry-Howard-Perspektive? Nichts, denn der Fixpunkt-Kombinator würde einem Axiom in unserem logischen System entsprechen, das den Cut-Elimination-Theorem bricht.

Grob gesagt repräsentiert in der Beweistheorie ein Beweissystem ohne Schnitteliminationssatz eine inkohärente Logik, also eine "Nicht-Logik". Anders gesagt, Curry-Howard zeigt, dass es eine unüberbrückbare Spannung zwischen zwei wichtigen Aspekten gibt (siehe auch hier ): Kohärenz (in der Logik) und Turing-Vollständigkeit (in Programmiersprachen). Das eine schließt das andere aus, aber eine Logik ohne Kohärenz ist keine Logik, und eine Programmiersprache, die nicht Turing-vollständig ist, garantiert nicht, dass Sie das Programm schreiben können, das Sie schreiben möchten (aber es gibt „Programmiersprachen“ wie z System F , die auf Curry-Howard-Korrespondenz basieren und sehr ausdrucksstark sind, obwohl sie nicht Turing-vollständig sind).

Selbstverständlich sind in der Praxis verwendete Programmiersprachen wie C, Python, C++, Java, OCaml etc. Turing-vollständig und benutzerfreundlich konzipiert, also für beliebige Programmtypen$A \to B$in einer dieser Sprachen geschrieben ist, ist es von Natur aus unmöglich, einen logischen Beweis dafür zu extrahieren$A \to B$in jedem Beweissystem, es sei denn, das Programm verwendet sehr grundlegende Konstrukte, die in eine der "Programmiersprachen" übersetzt werden können, für die die Curry-Howard-Korrespondenz gilt (leider ist dies ziemlich selten, zum Beispiel ist es nicht der Fall, wenn das Programm enthält eine whileSchleife).

Lassen$M$sei der gemessene Speicherplatz einer Maschine, auf der ein in Sprache geschriebenes Programm läuft$L$,$M$kann sein$\Bbb{Z}/2^{32}$oder eine Norm$\text{int}$Datentyp auf vielen Maschinen. Oder es könnte sein$\prod_{i=1}^n(\Bbb{Z}/2^{32})$für einige$n \geq 1$.

Dies ist ein gutes Maß dafür, was das Programm tut: Das Programm wirkt auf die Register, den Cache, den Arbeitsspeicher und die Speicherung einer Maschine, und das deckt so ziemlich alles ab. Um an einen Port zu schreiben, würden Sie einen der oben genannten verwenden, z

Also dann ein Programm, das den Datentyp nimmt$M$als Eingabe und Verdopplung (modulo$2^{32}$) sieht in Python so aus:

(Nehmen wir an, Python hat int32 und keine Ganzzahlen mit beliebiger Genauigkeit, was standardmäßig in der Standardversion von CPython der Fall ist.)

a = int(input("a="))
a = a << 1

Rufen Sie mit an python double_int.py 2. Ich weiß, dass es keine Ausgabe an das Programm gibt, aber dies ist für ein theoretisches Argument. Also ein Programm$f$nimmt eine Maschine in gemessenen Zustand$m \in M$und mutiert die Maschine so, dass sie sich im gemessenen Zustand befindet$f(m) \in M$.

Ich möchte sagen, dass ein Programm eine Implementierung eines Algorithmus darstellt$A$so dass, wenn Sie das Programm ausführen$f$auf seinem (notwendigerweise begrenzten, aber manchmal riesigen) Speicherplatz$M$), dh Sie rechnen$f(m)$für alle$m \in M$und das Ergebnis manuell überprüfen oder das Ergebnis mit dem Ergebnis eines vertrauenswürdigen anderen Programms vergleichen (Einheitentest) und das Ergebnis auscheckt, dann ist das Programm ein Beweis dafür$A$ist in der Sprache realisierbar$L$, und das$A$ist in der Tat ein gültiger Algorithmus, der berechnet, was er sagt.

Also wann$|M| \lt \approx 10^{9}$und es läuft ein$\log(m)$Zeit oder weniger, kann man innerhalb weniger Sekunden bis zu einer Stunde einen "Proof of Algorithmus" überprüfen$A$„Benutzung der Maschine$M$, und das Programm$f$.