Prüfen, ob ein beliebiger Beweis zirkulär ist?

13

Ich habe über Beweise nachgedacht und bin auf eine interessante Beobachtung gestoßen. Beweise entsprechen also Programmen über den Curry-Howard-Isomorphismus, und Zirkelbeweise entsprechen einer unendlichen Rekursion. Aber wir wissen aus dem Problem des Stillstands, dass es im Allgemeinen unentscheidbar ist, zu testen, ob ein beliebiges Programm für immer wiederkehrt. Bedeutet das für Curry-Howard, dass es keinen "Proof Checker" gibt, der feststellen kann, ob ein Proof Zirkelschluss verwendet?

Ich war immer der Meinung, dass Beweise aus leicht überprüfbaren Schritten bestehen sollten (die der Anwendung von Inferenzregeln entsprechen). Wenn Sie alle Schritte überprüfen, können Sie sicher sein, dass die Schlussfolgerung folgt. Aber jetzt frage ich mich: Vielleicht ist es tatsächlich unmöglich, einen solchen Proof Checker zu schreiben, weil es keine Möglichkeit gibt, das Stopp-Problem zu umgehen und Zirkelschlussfolgerungen zu erkennen?

logic curry-howard hewasonlyacat
quelle

Antworten:

15

Die überwiegende Mehrheit der Beweissysteme erlaubt keine unendlichen, zirkulären Beweise, aber sie tun dies, indem sie ihre Sprachen, die nicht Turing sind, vervollständigen.

In einer normalen funktionalen Sprache ist die einzige Möglichkeit, ein Programm für immer fortzusetzen, die Rekursion, und theoretisch betrachten wir die Rekursion als den Kombinator, ein Programm vom Typ ∀ a . ( a → a ) → a : Das heißt, eine Funktion ruft ein anderes "Selbst" -Argument auf und verwandelt es in eine einzige rekursive Funktion.Y∀a.(a→a)→a

Nun gelten die Curry-Howard Isomorphismus dazu: Wir haben jetzt einen Beweis , dass für jeden Satz , wenn ein selbst schon sagt, dann können wir beweisen , ein . So können wir alles beweisen!aaa

Der Schlüssel hier ist, dass der Y-Kombinator in eine Sprache eingebaut ist, er wird als Axiom genommen. Wenn Sie also möchten, dass es Ihnen keine Probleme bereitet, sollten Sie es einfach als Axiom loswerden!

Aus diesem Grund setzen die meisten formalen Beweissysteme eine fundierte Rekursion voraus. Sie akzeptieren nur Funktionen, von denen sie beweisen können, dass sie zum Stillstand kommen. Infolgedessen lehnen sie einige Programme ab, die zwar anhalten, für die sie es jedoch nicht beweisen können.

Coq tut dies auf eine ziemlich eingeschränkte Art und Weise: Es wird lediglich vorausgesetzt, dass alle rekursiven Funktionen ein Argument haben, während alle rekursiven Aufrufe nur streng kleinere Versionen dieses Arguments verwenden. Agda macht etwas Ähnliches, aber mit ein wenig mehr Lust zu überprüfen, um ein paar weitere Programme zu akzeptieren.

jmite
quelle
1
Schliesst Coq einige legitime Theoreme aus, die Sie sonst beweisen könnten? Oder gibt es immer Workarounds, wenn der Totality Checker zu konservativ ist? (Ich
gehe
1
@boyers FWIW, in Coq kann man mit Functionoder Program FixpointKonstruktionen beweisen, dass eine Funktion total ist, wenn die Totalitätsprüfung fehlschlägt. Ein einfaches Beispiel ist die Zusammenführungssortierfunktion für Listen. Man muss manuell beweisen, dass wir Listen (mit einer Länge> 1) in streng kleinere Unterlisten aufteilen.
Anton Trunov
@boyers Ja, es muss nach Gödels erstem Satz Dinge geben, die man in Coq nicht beweisen kann. In der Praxis sind sie selten anzutreffen, aber es gibt immer das diagonale Argument: Coq kann Coq selbst nicht beweisen, es kann nur eine Teilmenge beweisen (eine sehr große Teilmenge, einschließlich aller Funktionen, aber mit einer niedrigeren Grenze für den Rekursionsgrad es kann damit umgehen). Ich erinnere mich, dass ich gelesen habe, dass Coqs Theorie den Peano-Axiomen plus der Existenz einer bestimmten großen Ordnungszahl entspricht (und Beweise, die von einer noch größeren Ordnungszahl ausgehen, passen nicht), aber ich kann die Referenz jetzt nicht finden.
Gilles 'SO- hör auf böse zu sein'
@AntonTrunov In diesem Zusammenhang Programund dergleichen sind ein roter Hering. Sie ändern nichts an der Theorie. Was sie tun, ist syntaktischer Zucker, um ein Maß in einem Beweis zu verwenden: Anstatt zu argumentieren, dass das Objekt, an dem Sie interessiert sind, kleiner wird, fügen Sie eine Indirektionsebene hinzu: Berechnen Sie, dass ein anderes Objekt kleiner wird (z. B. eine bestimmte Größe), und beweisen Sie, dass es kleiner wird wird kleiner. Siehe die WfBibliothek.
Gilles 'SO- hör auf böse zu sein'
@ Gilles Ich nahm an, der Kontext handele von der praktischen (konkreten) Seite, wie wenn die Heuristik von Coq versagt ... Könnten Sie bitte versuchen, das von Ihnen erwähnte Papier zu finden? Ein Link wäre sehr dankbar.
Anton Trunov