Wie würde ich die zugrunde liegende Theorie des Coq Proof Assistant erlernen?
40
Ich gehe die Kursnotizen bei CIS 500 durch: Software-Grundlagen und die Übungen machen viel Spaß. Ich bin erst beim dritten Übungssatz, aber ich würde gerne mehr darüber erfahren, was passiert, wenn ich Taktiken verwende, um Dinge wie zu beweisenforall (n m : nat), n + n = m + m -> n = m.
Ein Ausgangspunkt ist das Coq-Referenzhandbuch ( pdf ). Kapitel 4 beschreibt die zugrunde liegende Logik von Coq, und letztendlich basiert alles darauf. Man nennt es den Kalkül (co) induktiver Konstruktionen, und viele Artikel beschreiben dies. Wenn Sie sich mit dem Coq'Art-Buch Interactive Theorem Proving and Program Development vertraut machen, können Sie sich entspannter, aber nicht billig mit Coq vertraut machen .
Um die erforderliche Theorie aufzubauen, müssen Sie sich mit Typentheorie vertraut machen . Am engsten mit der Theorie eines Beweisassistenten verbunden ist wahrscheinlich Per Martin-Löfs Intutionistic Type Theory Notes (oder Buch ) oder das Buch Programming in Martin-Löf Type Theory , in dem es wirklich um das Schreiben und Beweisen von Theoremen in der Typentheorie geht. Eine Programmiersprachenperspektive zur Typentheorie finden Sie in Pierces Types and Programming Languages . Eine weitere hervorragende Referenz sind die Proofs and Types von Girard et al., Die sich auch mit der Bedeutung der Curry-Howard-Korrespondenz befassen. Dann sind Sie wahrscheinlich wirklich bereit, Coquand und Huet's zu lesenDer Kalkül der Konstruktionen . Verfolgen Sie abschließend einige der Verweise im hinteren Teil des Coq-Handbuchs.
Es gibt andere Beweisassistenten , HOL, NuPRL, Mizar, Twelf usw., und sie haben auch ihre Theorie, sodass Sie auch viel lernen können, indem Sie in diese Richtung lesen.
Um einen Überblick über die Geschichte und Zukunft der Proof-Assistenten zu erhalten, lesen Sie abschließend den jüngsten Artikel von Herman Geuvers.
Schöne Liste. Ich werde eine Lesereihenfolge hinzufügen. Pierces TAPL deckt den Hintergrund ab; Der größte Teil des Restes ergibt erst dann Sinn, wenn Sie die Tippregeln beherrschen. Kapitel 2 von ATTAPL führt abhängige Typen relativ vorsichtig ein. Dann können Sie Kapitel 4 des Coq-Handbuchs lesen, in dem die Schreibregeln enthalten sind (Sie müssen in der Bibliographie nach einigen fortgeschrittenen Themen suchen, z. B. nach den genauen Regeln für die Rekursion). Parallel dazu hat das Coq'Art-Buch eine praktischere Perspektive. Bonus-Tipp: Show Treein Coq.
Gilles 'SO- hör auf böse zu sein'
2
Ich bin jemand in mehr oder weniger der gleichen Position wie das OP, wenn auch etwas weiter entfernt. Nach einigem Experimentieren fand ich schließlich die Reihenfolge 1) Lernen Sie funktionale Programmierung 2) Lesen Sie TAPL 3) Lesen Sie über abhängige Typen in ATTAPL, um besser als andere Dinge zu arbeiten. Gut zu wissen, dass ich ungefähr auf dem richtigen Weg bin.
John Salvatier
1
Ich war auch hier und habe das Coq'Art-Buch bekommen. Es ist absolut perfekt für das Verständnis, sie gehen auf jede Taktik im Detail ein und erklären, wann und wie man sie einsetzt. Das Buch führt Sie auch schnell durch alle Grundregeln der Typentheorie und lehrt Sie die Notation und deren Verwendung in Coq. Ich liebe dieses Buch.
Show Treein Coq.Was die typisierte Lambda-Rechnung, die intuitionistische Logik, verschiedene Beweissysteme und den Curry-Howard-Isomorphismus betrifft , die alle Teil des mathematischen Hintergrunds von Coq sind, empfehle ich nachdrücklich "Vorlesungen über den Curry-Howard-Isomorphismus" (von P. Urzyczyn und M. Sørensen).
quelle
Auch Luos Buch über die erweiterte Konstruktionsrechnung ist eine gute Referenz. Das ECC hatte großen Einfluss auf das Design der Coq-Typentheorie.
quelle
Das aktuelle Software Foundations-Buch erklärt dies alles später: https://softwarefoundations.cis.upenn.edu/lf-current/ProofObjects.html
Also, wenn Sie dem Buch folgen, lesen Sie einfach weiter :)
quelle