Nauka zautomatyzowanego dowodzenia twierdzeń

^{Uczę się samodzielnie Automated Theorem Proving / Solver SMT / Proof Assistants i piszę serię pytań na temat tego procesu, zaczynając tutaj.}

^{Zauważ, że te tematy nie są łatwe do zrozumienia bez tła w logice (matematycznej). Jeśli masz problemy z podstawowymi terminami, przeczytaj je, na przykład Logika w informatyce M. Hutha i M. Ryana (w szczególności rozdziały pierwszy, drugi i czwarty) lub Wprowadzenie do logiki matematycznej i teorii typów autorstwa P. Andrews.
Krótkie wprowadzenie do logiki wyższego rzędu (HOL) znajduje się tutaj .}

Spojrzałem na Coq i przeczytałem między innymi pierwszy rozdział wprowadzenia do Isabelle ; Rodzaje automatycznych dostawców twierdzeń

Znam Prolog od kilku dekad i uczę się teraz języka F #, więc ML, O'Caml i LISP są bonusem. Haskell to inna bestia.

Mam następujące książki

„Handbook of Automated Reasoning” pod redakcją Alana Robinsona i Andrieja Wornkowa

„Handbook of Practical Logic and Automated Reasoning” Johna Harrisona

„Przepisywanie terminów i wszystko inne” Franza Baadera i Tobiasa Nipkowa

1. Jakie są różnice między Coq a Isabelle?

2. Czy powinienem nauczyć się Isabelle, Coq, czy obu?

3. Czy jest korzyść z nauki najpierw Isabelle lub Coq?

^{Znajdź następne pytanie z serii tutaj .}

Preferuję Coq, ale wyobrażam sobie, że inni wolą Isabelle. Jedną z dziwnych rzeczy, które znalazłem w Isabelle jest to, że istnieje dwupoziomowa składnia, w której niektóre z twoich definicji muszą znajdować się w podwójnym cudzysłowie. W Coq nie ma takich bzdur.

Ostatecznie ten, który jest najbardziej odpowiedni dla ciebie, może zależeć od tego, co chcesz udowodnić. Oba języki mają wiele wsparcia dla bibliotek i aktywne społeczności zajmujące się wszelkiego rodzaju programowaniem i przykładowymi teoriami. Jeśli jeden język zapewnia odpowiednią bibliotekę (lub inny) wsparcie dla rodzajów teorii, które chcesz rozwinąć, wybrałbym ten język.

Jedną ze strategii jest wykonanie prostego samouczka w obu językach i kontynuacja tego, który wydaje się najlepszy. Na przykład,

• Coq w pośpiechu Yves Bertot, lub
• pierwsza część A Proof Assistant for Higher-Order Logic autorstwa Tobiasa Nipkowa, Lawrence'a C. Paulsona i Markusa Wenzela.

Oto post na blogu, w którym krótko porównuje te dwa przez kogoś, kto ostatecznie woli Isabelle.

Upewnij się, że używasz właściwego IDE (takiego jak ProofGeneral ), zamiast robić rzeczy w wierszu poleceń.

Innym sposobem na dostanie się do Coq jest wypróbowanie książki online Software Foundations autorstwa Benjamina Pierce'a i in. Zapewnia doskonały samouczek z mnóstwem szczegółowych informacji. Nacisk kładziony jest głównie na semantykę języka programowania, ale po drodze omówiono wiele podstaw (i nie tylko) Coq oraz półautomatycznego dowodzenia twierdzeń.

Jedną z rzeczy, które moim zdaniem będą interesujące, jest to, że termin „dowodzenie twierdzenia” różni się znacznie w zależności od dziedziny, w której się znajdujesz. Chociaż są one - w sposób abstrakcyjny - nieco powiązane, praktyczne dowodzenie twierdzeń (takie jak patrz rozwinięte w Handbook of Automated Reasoning) ma mniej wspólnego z Coq lub Isabelle, niż mogłoby się wydawać.

Kiedy po raz pierwszy zacząłem uczyć się o twierdzeniu dowodzącym pokrewnych rzeczy, pierwszą książką, którą przeczytałem (chociaż teraz dość przestarzałą?) Była doskonała logika pierwszego rzędu i automatyczne dowodzenie twierdzeń Melvina Fittinga. Ta książka była naprawdę doskonała i obejmowała rodzaje tematów, które zobaczysz, które dotyczą logiki niższego rzędu, w której można uzyskać całkiem sporo automatyzacji. Logika, której się uczysz, powinna być podyktowana tym, o czym chcesz wnioskować, a nie tyle twierdzeniem, które z tego powodu. Na przykład, podczas gdy logika pierwszego rzędu zapewnia dużą ekspresję i umiejętność rozumowania, większość społeczności języków programowania (w której ostatnio skończyłem) opuściła starszą szkołę dowodzenia twierdzeń i sprawdzania modeli (które wchodzą w koszyk rzeczy, które są bardziej rozstrzygalne, ale mniej wyraziste).

Nie oznacza to jednak, że takie rzeczy, jak wnioskowanie pierwszego rzędu i sprawdzanie modelu, nie były wyjątkowo przydatne w praktyce. Oni byli! Możesz spojrzeć na ACL2 jako przykład provera zbudowanego na logice pierwszego rzędu, który ma niesamowity sukces w sferze przemysłowej. Oprócz tego nastąpił niesamowity rozwój rozwiązań w zakresie SMT. Nowoczesne solwery SMT są zbudowane na bardzo potężnych solverach SAT (głównie dzięki odkryciom w ciągu ostatnich dwudziestu lat w celu ulepszenia DPLL) i znalazły wiele zastosowań w symbolicznych wykonaniach.

Jednak, jak już powiedziałem, chociaż bardziej tradycyjny „dowodzenie twierdzenia” jest zabawny, jest o wiele więcej do nauczenia się. Nauka uczenia się - na przykład - ma niewiele wspólnego z uczeniem się narzędzi automatyzacji, które ci daje, i ma znacznie więcej wspólnego z uczeniem się teorii typów, na której się opiera (rachunek predykcyjny konstrukcji koindukcyjnych). Jeśli nie jesteś przyzwyczajony do konstruktywnej logiki, izomorfizmu curry Howarda lub teorii typów, będziesz miał ekscytujący czas na naukę tych narzędzi, ale trudno mi pomyśleć, że są zbyt blisko związane z rzeczami, które zobaczysz w pierwszym tomie podręcznika.

Zdecyduj więc, co chcesz zrobić: zweryfikuj modele i twierdzenia w logice pierwszego rzędu lub użyj potężnej teorii typów, aby uzasadnić poprawność swoich programów (lub twierdzeń w logice konstruktywnej). Jeśli to pierwszy, dowiedz się więcej o technikach opartych na zautomatyzowanej dedukcji, jeśli to drugi, dowiedz się więcej o Coq, HOL itp. Nawiasem mówiąc, jeśli chcesz nauczyć się Coq, a powyższe odniesienia są dobre, myślę, że istnieją dwa podstawowe odniesienia do nauki języka Coq:

Książka założycieli Benjamina Pierce'a (Dr. Pierce jest znakomitym pisarzem. Polecam również przyjrzeć się jego bardziej popularnej „książce z cegły”, jeśli jeszcze tego nie zrobiłeś).

Certyfikowane programowanie z typami zależnymi (Adam Chlipala również pisze całkiem dobrze, chociaż jego książki zakładają nieco więcej dojrzałości i inteligencji niż być może prostsze wprowadzenie Pierce'a).

Istnieje wiele systemów do interaktywnego sprawdzania twierdzeń (ITP) - patrz także konferencja o tej nazwie - Coq, Isabelle, HOLs, ACL2, PVS itp.

Wszystkie z nich są stosunkowo trudne do nauczenia się, a każda z nich ma swoją specyficzną kulturę. To jest jak nauka języka obcego: powiedzmy, że znasz już angielski, a następnie wybierz język francuski, niemiecki, włoski, hiszpański, portugalski. Wszystkie są w jakiś sposób powiązane - to nie jest Chińczyk - ale niewielu ludzi zarządza tym wszystkim jednocześnie. Dlatego powinieneś spróbować zasmakować każdej kultury i społeczności, a następnie podjąć zobowiązanie.

Może być też „funkcja zabójcy”, której naprawdę potrzebujesz do swojej pracy.

Pomaga także mieć wokół siebie innych ekspertów od jednego z tych systemów.

• Jakie są różnice między Coq a Isabelle?

Obaj są potomkami systemu LCF ze Stanford / Edinburgh / Cambridge. W 1985 roku G. Huet i L. Paulson pracowali razem nad ostatnią wersją Cambridge LCF. Następnie nastąpił podział w stosunku do Coc / CIC / COQ (obecnie Coq) we Francji oraz Isabelle w Cambridge i Monachium. Należy pamiętać, że HOL4, HOL-Light, HOL-XYZ są innymi pokrewnymi potomkami LCF.

Ponad 20 lat temu rozróżnienie Coq vs. Isabelle zostałoby dokonane zgodnie z logicznymi podstawami: tutaj logika konstruktywna zależna, tutaj logika klasyczna uproszczona. Obecnie w praktyce jest to zaskakująco mało, ponieważ na każdym systemie formalnym dodawanych jest coraz więcej warstw, w tym dodatkowe narzędzia i biblioteki.

• Czy powinienem nauczyć się Isabelle, Coq, czy obu?

Powinieneś spojrzeć na oba i spróbować poczuć, czy lubisz więcej wina i sera, czy kiełbasy i kapusty kiszonej. (Jako jeden z facetów stojących za Isabelle, ale obecnie we Francji, jestem zaskoczony, ilu Francuzów naprawdę lubi Sauerkraut, kiedy są prywatnie w domu i nikt nie patrzy :-)

• Czy jest korzyść z nauki najpierw Isabelle lub Coq?

Nie wydaje mi się Może istnieć niebezpieczeństwo, że utkniesz z tym, którego próbujesz pierwszy, a nie drugim, lub że rozczarujesz się zbyt wcześnie z pierwszym i odrzucisz go zbyt wcześnie. W każdym razie potrzebujesz czasu i wytrwałości, aby osiągnąć produktywność w obu systemach.

Ponieważ już wspomniano o Proof General jako „IDE”: Proof General / Emacs był standardowym interfejsem ujednolicającym zarówno dla Coq, jak i Isabelle przez wiele lat, ale nigdy nie nazwałbym tego IDE. Istnieje również CoqIDE z „IDE” w nazwie, ale jest stosunkowo prostym edytorem oprócz widżetów Gtk. Obecna Isabelle zawiera Isabelle / jEdit, która nie ma w nazwie „IDE”, ale ma na celu przybliżenie rzeczy, które widzisz rutynowo w Netbeans lub IntelliJ IDEA --- dla tekstów próbnych zamiast kodu Java.

Oto kilka ładnych samouczków wideo Coq autorstwa Andreja Bauera. Nie jest w żaden sposób kompletny, ale myślę, że to dobre wprowadzenie.

To wprowadzenie do Isabelle jest dość wyczerpujące.

Zobacz także wprowadzenie do Isabelle

Ogólnie rzecz biorąc, Isabelle jest stosunkowo łatwa na początek, ponieważ istnieje wiele dostępnych przykładów. Na przykład na oficjalnej stronie internetowej

PS - Nie jestem w żaden sposób związany z Isabelle, jestem teoretykiem metod formalnych, ale wiem, że Isabelle często pojawia się jako domyślny punkt wyjścia.

Niedawno przyszedłem do tych samouczków Coq z conf2017, więc doszedłem do wniosku, że warto się tutaj podzielić dla każdego, kto odwiedza to pytanie później.$\lambda$

• Gabriel Claramunt - Wprowadzenie do Coq - Część 1 z 2 - λC 2017
• Gabriel Claramunt - Wprowadzenie do Coq - Część 2 z 2 - λC 2017

Ponadto, DeepSpec Summer School's Software Foundations ma kilka fajnych wykładów:

• DeepSpec Summer School, 13-28 lipca 2017 r
• DeepSpec Summer School, 16-27 lipca 2018 r

Niektóre wykłady oparte na serii Software Foundations, o których już wspomniano.

• Coq Intensive

• Zweryfikowane algorytmy funkcjonalne