Warum sind logische Verknüpfungen und boolesche Werte in Coq getrennt?

Question

Ich komme aus einem JavaScript/Ruby-Programmierung Hintergrund und bin es gewohnt, da dies, wie wahr/falsch Werke (in JS):

!true 
// false 
!false 
// true 

Dann können Sie diese wahr/falsch Werte mit && wie

var a = true, b = false; 
a && !b; 

verwenden

Also und und nicht (und andere logische/Boolean Operatoren) sind Teil eines einzigen Systems; Es scheint, als ob das "logische" System und das "Boolesche" System ein und dasselbe sind.

In Coq sind Logiken und Booleans jedoch zwei verschiedene Dinge. Warum ist das? Das Zitat/der Link unten zeigt, wie ein Theorem notwendig ist, um sie in Beziehung zu setzen.

Wir haben bereits mehrere Orte gesehen, an denen analoge Strukturen in Coqs computergestützten (Typ) und logischen (Prop) Welten gefunden werden können. Hier ist eine weitere: Die booleschen Operatoren andb und orb sind eindeutig Analoga der logischen Konnektoren ∧ und ∨. Diese Analogie kann durch die folgenden Theoreme präzisiert werden, die zeigen, wie man das Wissen über das Verhalten von andb und orb bei bestimmten Eingaben in propositionale Fakten über diese Eingaben übersetzt.

Theorem andb_prop : ∀b c, 
    andb b c = true → b = true ∧ c = true. 

http://www.seas.upenn.edu/~cis500/current/sf/Logic.html#lab211

Answer 1

Im Wesentlichen hat Coq beide, weil sie für verschiedene Dinge nützlich sind: booleans Tatsachen entsprechen, die mechanisch überprüft werden kann (dh mit einem Algorithmus), während Sätzen ausdrücken können mehr Konzepte.

Streng genommen sind die logischen und booleschen Welten in Coq nicht getrennt: Die boolesche Welt ist eine Teilmenge der logischen Welt. Mit anderen Worten, jede Aussage, die Sie als eine boolesche Berechnung formulieren können, kann als eine logische Aussage angesehen werden (dh etwas vom Typ Prop): Wenn b : bool eine Aussage darstellt, können wir bestätigen, dass diese Aussage wahr ist, indem wir b = true sagen vom Typ Prop.

Der Grund, warum es in Coq mehr Logik als nur boolesche gibt, ist, dass die Umkehrung der vorherigen Anweisung nicht gilt: nicht alle logischen Fakten können als boolesche Berechnungen betrachtet werden. Anders gesagt, es ist nicht so, dass Booleans in normalen Programmiersprachen wie Ruby und JavaScript sowohl bool als auch Prop in Coq subsummieren, weil Prop s Dinge ausdrücken können, die Boolesche Sprachen in diesen Sprachen nicht können.

Um dies zu veranschaulichen, betrachten Sie das folgende Coq Prädikat:

Definition commutative {T} (op : T -> T -> T) : Prop := 
    forall x y, op x y = op y x. 

Wie der Name schon sagt, dieses Prädikat behauptet, dass ein Bediener op kommutativ ist. Viele Operatoren in Programmiersprachen sind kommutativ: Nehmen Sie beispielsweise Multiplikation und Addition über Ganzzahlen. Tatsächlich in Coq können wir die folgenden Aussagen beweisen (und ich glaube die Beispiele in der Software Foundations Buch sind):

Lemma plus_comm : commutative plus. Proof. (* ... *) Qed. 
Lemma mult_comm : commutative mult. Proof. (* ... *) Qed. 

Nun versuchen zu denken, wie Sie ein Prädikat wie commutative in einer konventionelleren Sprache übersetzen würden.Wenn dies schwierig erscheint, ist es kein Zufall: Es ist möglich zu beweisen, dass wir kein Programm schreiben können, das einen booleschen Wert in diesen Sprachen zurückgibt, um zu testen, ob eine Operation kommutativ ist oder nicht. Sie können sicher Unit-Tests schreiben zu prüfen, ob diese Tatsache für bestimmte Eingaben wahr ist, zB:

2 + 3 == 3 + 2 
4 * 5 == 5 * 4 

Allerdings, wenn Ihr Betreiber mit einer unendlichen Anzahl von Eingängen arbeitet, können diese Unit-Tests decken nur einen Bruchteil alle möglichen Fälle. Daher ist Testen immer notwendigerweise schwächer als ein vollständiger formaler Beweis.

Sie könnten sich fragen, warum wir Booleans in Coq haben, wenn Prop s alles ausdrücken kann, was booleans kann. Der Grund dafür ist, dass Coq eine konstruktive Logik ist, worauf Vinz in seinem Kommentar anspielte. Die bekannteste Folge dieser Tatsache ist, dass in Coq wir folgendes intuitives Prinzip nicht beweisen können:

Definition excluded_middle := 
    forall P : Prop, P \/ ~ P. 

, die im Wesentlichen besagt, dass jeder Satz entweder wahr oder falsch ist. "Wie könnte das scheitern?", Könnten Sie sich fragen. Grob gesagt, in konstruktiven Logiken (und insbesondere Coq) entspricht jeder Beweis einem Algorithmus, den wir ausführen können. Insbesondere, wenn Sie eine Aussage des Formulars A \/ B in einer konstruktiven Logik beweisen, können Sie einen (immer beendenden) Algorithmus aus diesem Beweis extrahieren, der antwortet, ob A oder B gilt. Wenn wir also das obige Prinzip beweisen könnten, hätten wir einen Algorithmus, der uns anhand eines Satzes sagt, ob dieser Satz gültig ist oder nicht. Die Berechenbarkeitstheorie zeigt jedoch, dass dies im Allgemeinen wegen Unentscheidbarkeit nicht möglich ist: Wenn wir P mit "Programm hält auf Eingang x" annehmen, würde die ausgeschlossene Mitte einen Entscheider für die halting problem ergeben, die nicht existieren kann.

Nun, was interessant ist an Booleans in Coq ist, dass durch Konstruktion erlauben sie die Verwendung der ausgeschlossenen Mitte, weil sie tun entsprechen einem Algorithmus, den wir ausführen können.

Lemma excluded_middle_bool : 
    forall b : bool, b = true \/ negb b = true. 
Proof. intros b; destruct b; simpl; auto. Qed. 

So in Coq es nützlich ist, booleans als Sonderfall von Sätzen zu betrachten, weil sie Formen der Argumentation ermöglichen, dass andere Sätze nicht, nämlich, Fallanalyse: Im Einzelnen können wir folgende beweisen.

Natürlich können Sie denken, dass es albern ist zu verlangen, dass jeder Beweis einem Algorithmus entspricht, und tatsächlich erlauben die meisten Logiken das Prinzip der ausgeschlossenen Mitte. Beispiele für Proof-Assistenten, die standardmäßig diesem Ansatz folgen, sind Isabelle/HOL und Mizar. In diesen Systemen müssen wir nicht zwischen Booleans und Propositionen unterscheiden, und sie werden als dasselbe behandelt. Isabelle zum Beispiel hat nur bool und keine Prop. Coq ermöglicht es Ihnen auch, die Unterscheidung zwischen Booleans und Propositionen zu verwischen, indem Sie Axiome annehmen, mit denen Sie Fallanalysen zu allgemeinen Aussagen durchführen können. Wenn Sie in einer solchen Einstellung eine Funktion schreiben, die einen booleschen Wert zurückgibt, erhalten Sie möglicherweise nicht etwas, das Sie als Algorithmus ausführen können, während das in Coq standardmäßig immer der Fall ist.