Wie würde ich die zugrunde liegende Theorie des Coq Proof Assistant erlernen?

Antworten:

32

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 .

Sehen Sie sich diese frühere Frage an, um zu erfahren, wie Taktiken funktionieren: Wie funktionieren Taktiken in Proofassistenten?

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.

Dave Clarke
quelle
5
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.
Lance Pollard
15

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).

Marcin Kotowski
quelle
Wir scheinen heute auf der gleichen Wellenlänge zu sein . ;-)
Marc Hamann
Es scheint der Curry-Howard-Tag zu sein: cstheory.stackexchange.com/questions/5848/…
Dave Clarke
6

Auch Luos Buch über die erweiterte Konstruktionsrechnung ist eine gute Referenz. Das ECC hatte großen Einfluss auf das Design der Coq-Typentheorie.

Dominic Mulligan
quelle