Coq -Coq

Informacje na temat koenzymu i suplementu diety można znaleźć w artykule Koenzym Q10 . Aby zapoznać się ze skróconą nazwą miejsca, zobacz Coquihalla . Informacje na temat koguta można znaleźć w artykule Rooster .
Coq (oprogramowanie)
Deweloperzy Zespół programistów Coq
Pierwsze wydanie 1 maja 1989 ; 33 lata temu (wersja 4.10) ( 1989-05-01 )
Wersja stabilna
8.17.0  Edytuj to w Wikidanych / 27 marca 2023 ; 18 dni temu ( 27 marca 2023 )
Magazyn github.com/coq/coq _ _ _
Napisane w OCaml
System operacyjny Międzyplatformowe
Dostępne w język angielski
Typ Asystent dowodu
Licencja LGPLv2.1
Strona internetowa coq .inria .fr
Interaktywna sesja sprawdzająca w CoqIDE, pokazująca skrypt sprawdzający po lewej stronie i stan sprawdzający po prawej.

Coq to interaktywny program do dowodzenia twierdzeń, wydany po raz pierwszy w 1989 roku. Umożliwia wyrażanie twierdzeń matematycznych , mechanicznie sprawdza dowody tych twierdzeń, pomaga znaleźć dowody formalne i wyodrębnia certyfikowany program z konstruktywnego dowodu jego formalnej specyfikacji . Coq zajmuje się teorią rachunku konstrukcji indukcyjnych , pochodną rachunku konstrukcji . Coq nie jest automatycznym narzędziem do dowodzenia twierdzeń, ale obejmuje automatyczne taktyki ( procedury ) dowodzenia twierdzeń oraz różne procedury decyzyjne .

Association for Computing Machinery przyznało Thierry'emu Coquandowi , Gérardowi Huetowi , Christine Paulin-Mohring , Bruno Barrasowi, Jean-Christophe Filliâtre, Hugo Herbelinowi, Chetanowi Murthy'emu, Yves Bertot i Pierre'owi Castéranowi nagrodę ACM Software System Award 2013 za Coq.

Nazwa „Coq” jest grą słowną imienia Thierry'ego Coquanda, Rachunku Konstrukcji lub „CoC” i jest zgodna z francuską tradycją informatyczną polegającą na nazywaniu oprogramowania na cześć zwierząt (coq po francusku oznacza koguta ) .

Przegląd

Postrzegany jako język programowania, Coq implementuje zależny język programowania funkcjonalnego ; gdy jest postrzegany jako system logiczny, implementuje teorię typów wyższego rzędu . Rozwój Coq jest wspierany od 1984 roku przez INRIA , obecnie we współpracy z École Polytechnique , University of Paris-Sud , Paris Diderot University i CNRS . W latach 90. ENS Lyon był również częścią projektu. Rozwój Coq został zainicjowany przez Gérarda Hueta i Thierry'ego Coquanda, a ponad 40 osób, głównie badaczy, wniosło wkład w podstawowe funkcje systemu od jego powstania. Zespół wdrożeniowy był kolejno koordynowany przez Gérarda Hueta, Christine Paulin-Mohring, Hugo Herbelina i Matthieu Sozeau. Coq jest implementowany głównie w OCamlu z odrobiną C . Podstawowy system można rozszerzyć za pomocą mechanizmu wtykowego .

Nazwa coq oznacza po francusku „ koguta ” i wywodzi się z francuskiej tradycji nazywania narzędzi badawczych i rozwojowych imionami zwierząt. Do 1991 roku Coquand wdrażał język zwany Rachunkiem Konstrukcyjnym , który wtedy nosił po prostu nazwę CoC. W 1991 roku rozpoczęto nową implementację opartą na rozszerzonym rachunku konstrukcji indukcyjnych i zmieniono nazwę z CoC na Coq w pośrednim nawiązaniu do Coquand, który wraz z Gérardem Huetem opracował rachunek konstrukcji i przyczynił się do powstania rachunku konstrukcji indukcyjnych z Christine Paulin-Mohring.

Coq zapewnia język specyfikacji o nazwie Gallina („ kura ” po łacinie, hiszpańsku, włosku i katalońsku). Programy napisane w Gallinie mają słabą właściwość normalizacji , co oznacza, że ​​zawsze się kończą. Jest to charakterystyczna właściwość języka, ponieważ nieskończone pętle (programy niekończące się) są powszechne w innych językach programowania i jest to jeden ze sposobów uniknięcia problemu zatrzymania .

Jako przykład dowód przemienności dodawania na liczbach naturalnych w 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_indoznacza indukcję matematyczną , eq_indzastępowanie równych i f_equalprzyjmowanie tej samej funkcji po obu stronach równości. Wcześniejsze twierdzenia są odwoływane pokazując i .

Godne uwagi zastosowania

Twierdzenie o czterech kolorach i rozszerzenie SSReflect

Georges Gonthier z Microsoft Research w Cambridge w Anglii i Benjamin Werner z INRIA użyli Coq do stworzenia możliwego do zbadania dowodu twierdzenia o czterech kolorach , który został ukończony w 2002 roku. Ich praca doprowadziła do opracowania pakietu SSReflect („Odbicie w małej skali”) , co było znaczącym rozszerzeniem Coq. Pomimo swojej nazwy, większość funkcji dodanych do Coq przez SSReflect to funkcje ogólnego przeznaczenia i nie ograniczają się do obliczeniowego stylu dowodu. Funkcje te obejmują:

  • Dodatkowe wygodne notacje dla niepodważalnego i obalnego dopasowywania wzorców na typach indukcyjnych z jednym lub dwoma konstruktorami
  • Niejawne argumenty funkcji stosowane do argumentów zerowych, co jest przydatne podczas programowania z funkcjami wyższego rzędu
  • Zwięzłe anonimowe argumenty
  • Ulepszona settaktyka z silniejszym dopasowaniem
  • Wsparcie dla refleksji

SSReflect 1.11 jest swobodnie dostępny, posiada podwójną licencję w ramach licencji open source CeCILL-B lub CeCILL-2.0 i jest kompatybilny z Coq 8.11.

Inne aplikacje

Zobacz też

Bibliografia

Linki zewnętrzne

Podręczniki
Samouczki