Coq -Coq

Für Coenzym und Nahrungsergänzungsmittel siehe Coenzym Q10 . Für den abgekürzten Ortsnamen siehe Coquihalla . Für den Hahn siehe Hahn .
Coq (Software)
Entwickler Das Coq-Entwicklungsteam
Erstveröffentlichung 1. Mai 1989 ; Vor 33 Jahren (Version 4.10) ( 1989-05-01 )
Stabile Version
8.17.0  Bearbeiten Sie dies auf Wikidata / 27. März 2023 ; Vor 18 Tagen ( 27. März 2023 )
Repository github .com /coq /coq
Geschrieben in OCaml
Betriebssystem Plattformübergreifend
Verfügbar in Englisch
Typ Beweisassistent
Lizenz LGPLv2.1
Webseite coq .inria .fr
Eine interaktive Proof-Session in CoqIDE, die das Proof-Skript auf der linken Seite und den Proof-Status auf der rechten Seite zeigt.

Coq ist ein interaktiver Theorembeweiser, der erstmals 1989 veröffentlicht wurde. Er ermöglicht das Ausdrücken mathematischer Behauptungen, überprüft mechanisch Beweise dieser Behauptungen, hilft beim Auffinden formaler Beweise und extrahiert ein zertifiziertes Programm aus dem konstruktiven Beweis seiner formalen Spezifikation . Coq arbeitet innerhalb der Theorie des Kalküls induktiver Konstruktionen , einer Ableitung des Konstruktionskalküls . Coq ist kein automatisierter Theorembeweiser, beinhaltet aber automatische Theorembeweistaktiken ( Prozeduren ) und verschiedene Entscheidungsverfahren .

Die Association for Computing Machinery zeichnete Thierry Coquand , Gérard Huet , Christine Paulin-Mohring , Bruno Barras, Jean-Christophe Filliâtre, Hugo Herbelin, Chetan Murthy, Yves Bertot und Pierre Castéran mit dem ACM Software System Award 2013 für Coq aus.

Der Name „Coq“ ist ein Wortspiel mit dem Namen Thierry Coquand, Calculus of Constructions oder „CoC“, und folgt der französischen Informatiktradition, Software nach Tieren zu benennen (coq bedeutet auf Französisch Hahn ) .

Überblick

Als Programmiersprache betrachtet, implementiert Coq eine abhängig typisierte funktionale Programmiersprache ; Wenn es als logisches System betrachtet wird, implementiert es eine Typentheorie höherer Ordnung . Die Entwicklung von Coq wird seit 1984 von INRIA unterstützt , jetzt in Zusammenarbeit mit der École Polytechnique , der Universität Paris-Süd , der Universität Paris Diderot und dem CNRS . In den 1990er Jahren war auch ENS Lyon Teil des Projekts. Die Entwicklung von Coq wurde von Gérard Huet und Thierry Coquand initiiert, und mehr als 40 Personen, hauptsächlich Forscher, haben seit seiner Einführung Funktionen zum Kernsystem beigetragen. Das Implementierungsteam wurde nacheinander von Gérard Huet, Christine Paulin-Mohring, Hugo Herbelin und Matthieu Sozeau koordiniert. Coq ist hauptsächlich in OCaml mit etwas C implementiert . Das Kernsystem kann über einen Plug-in- Mechanismus erweitert werden.

Der Name coq bedeutet auf Französisch „ Hahn “ und stammt aus einer französischen Tradition, Forschungs- und Entwicklungsinstrumente nach Tieren zu benennen. Bis 1991 implementierte Coquand eine Sprache namens Calculus of Constructions , die damals einfach CoC genannt wurde. 1991 wurde eine neue Implementierung basierend auf dem erweiterten Kalkül der induktiven Konstruktionen gestartet und der Name wurde von CoC in Coq geändert, in einem indirekten Hinweis auf Coquand, der den Konstruktionskalkül zusammen mit Gérard Huet entwickelte und zum Kalkül der induktiven Konstruktionen beitrug mit Christine Paulin-Mohring.

Coq bietet eine Spezifikationssprache namens Gallina (" Henne " auf Latein, Spanisch, Italienisch und Katalanisch). In Gallina geschriebene Programme haben die schwache Normalisierungseigenschaft , was bedeutet, dass sie immer terminieren. Dies ist eine charakteristische Eigenschaft der Sprache, da Endlosschleifen (nicht terminierende Programme) in anderen Programmiersprachen üblich sind, und eine Möglichkeit darstellt, das Halteproblem zu vermeiden .

Als Beispiel ein Beweis der Kommutativität der Addition auf natürliche Zahlen in Coq: 

plus_comm =
fun n m : nat =>
nat_ind (fun n0 : nat => n0 + m = m + n0)
  (plus_n_0 m)
  (fun (y : nat) (H : y + m = m + y) =>
   eq_ind (S (m + y))
     (fun n0 : nat => S (y + m) = n0)
     (f_equal S H)
     (m + S y)
     (plus_n_Sm m y)) n
     : forall n m : nat, n + m = m + n

nat_indsteht für mathematische Induktion , eq_indfür Substitution von Gleichen und f_equalfür die Übernahme der gleichen Funktion auf beiden Seiten der Gleichheit. Frühere Theoreme werden referenziert und zeigen und .

Bemerkenswerte Verwendungen

Vierfarbensatz und SSReflect-Erweiterung

Georges Gonthier von Microsoft Research in Cambridge , England , und Benjamin Werner von INRIA verwendeten Coq, um einen überschaubaren Beweis des Vierfarbensatzes zu erstellen , der 2002 fertiggestellt wurde. Ihre Arbeit führte zur Entwicklung des Pakets SSReflect ("Small Scale Reflection") , was eine bedeutende Erweiterung von Coq war. Trotz seines Namens sind die meisten von SSReflect zu Coq hinzugefügten Funktionen Allzweckfunktionen und nicht auf den rechnerischen Reflexionsstil des Beweises beschränkt. Zu diesen Funktionen gehören:

  • Zusätzliche praktische Notationen für unwiderlegbare und widerlegbare Mustererkennung auf induktiven Typen mit einem oder zwei Konstruktoren
  • Implizite Argumente für Funktionen, die auf Nullargumente angewendet werden, was beim Programmieren mit Funktionen höherer Ordnung nützlich ist
  • Prägnante anonyme Argumente
  • Eine verbesserte setTaktik mit stärkerem Matching
  • Unterstützung für Reflexion

SSReflect 1.11 ist frei verfügbar, doppelt lizenziert unter der Open-Source- Lizenz CeCILL-B oder CeCILL-2.0 und kompatibel mit Coq 8.11.

Andere Anwendungen

Siehe auch

Verweise

Externe Links

Lehrbücher
Tutorials