Jak działają „taktyki” w asystentach dowodowych?

Pytanie: Jak działają „taktyki” w asystentach dowodowych? Wydają się być sposobami na określenie, jak przepisać termin na równoważny (dla pewnej definicji „równoważnego”). Przypuszczalnie istnieją formalne zasady dotyczące tego, w jaki sposób mogę dowiedzieć się, czym one są i jak działają? Czy wiążą się one z czymś więcej niż tylko wyborem kolejności obniżenia wersji beta?

Informacje o moich zainteresowaniach: Kilka miesięcy temu zdecydowałem, że chcę nauczyć się formalnej matematyki. Zdecydowałem się na teorię typów, ponieważ ze wstępnych badań wydaje się, że to właściwa droga do zrobienia rzeczy (TM) i ponieważ wydaje się, że ujednolicenie programowania i matematyki jest fascynujące . Myślę, że moim ostatecznym celem jest umiejętność posługiwania się i rozumienia asystenta dowodu, takiego jak Coq (myślę, że szczególnie mogę używać typów zależnych, ponieważ jestem ciekaw rzeczy takich jak reprezentowanie typów matryc). Zacząłem od znajomości bardzo niewielkiego, nawet podstawowego programowania funkcjonalnego, ale robię powolne postępy. Przeczytałem i zrozumiałem duże fragmenty rodzajów i języków programowania (Pierce) i nauczyłem się kilku języków Haskell i ML.

Podstawowa taktyka polega na uruchamianiu reguły wnioskowania do przodu lub do tyłu (na przykład zamień hipotezy i na lub zamień cel na dwa cele iB A ∧ B A ∧ B A $A$$B$$A\wedge B$$A\wedge B$$A$$B$z tymi samymi hipotezami), zastosuj lemat (zastosowanie funkcji ~), podziel lemat o pewnym typie indukcyjnym na przypadek dla każdego konstruktora i tak dalej. Podstawowe taktyki mogą się powieść lub nie, w zależności od kontekstu, w którym są stosowane. Bardziej zaawansowane taktyki są jak małe programy funkcjonalne, które uruchamiają podstawowe taktyki, wykonują dopasowanie wzorca do warunków w celu i / lub założeniach, dokonują wyborów w oparciu o sukces lub porażkę taktyki i tak dalej. Bardziej zaawansowane taktyki dotyczą arytmetyki i innych specyficznych rodzajów teorii. Kluczowy artykuł na temat języka taktyki Coq jest następujący:

• D. Delahaye. Język taktyki dla systemu Coq . W Proceedings of Logic for Programming and Automated Reasoning (LPAR), Reunion Island, tom 1955 notatek z wykładów z informatyki, strony 85–95. Springer-Verlag, listopad 2000.

Formalne zasady, które stanowią istotę podstawowej taktyki, zdefiniowano w przewodniku dla użytkowników Coq tutaj lub w rozdziale 4 pdf .

Całkiem pouczający artykuł na temat wdrażania taktyki i taktyki (zasadniczo taktyki, które traktują inne taktyki jako argumenty) to:

• Amy Felty. Wdrażanie taktyki i taktyki w języku programowania wyższego rzędu Journal of Automated Reasoning, 11 (1): 43-81, sierpień 1993.

Język taktyki Coq ma takie ograniczenie, że pisane przy jego użyciu dowody prawie nie przypominają dowodów wykonywanych ręcznie. Podjęto szereg prób w celu uzyskania wyraźniejszych dowodów. Należą do nich Isar (dla Isabelle / HOL) i język próbny Mizara .

Poza tym: czy wiesz również, że język programowania ML został pierwotnie zaprojektowany do implementacji taktyki dla dowodu twierdzenia LCF ? Wiele pomysłów opracowanych dla ML, takich jak wnioskowanie typu, wpłynęło na współczesne języki programowania.

LCF jest rzeczywiście dziadkiem wszystkich tych systemów: Coq, Isabelle, HOLs, w tym języka programowania ML (które dziś widzimy jako OCaml, SML, a także F #). Tak, włączam Coq jako członka większej rodziny LCF. W porównaniu do amerykańsko-amerykańskich asystentów dowodowych (w szczególności ACL2) lub całkowicie niezwiązanego Mizara, Coq jest kulturowo dość zbliżony do Isabelle i HOL, głównie ze względu na wspólną ideę taktyki .

Czym więc są taktyki, pozbawione przypadkowych spostrzeżeń na temat przepisywania, konwersji, wprowadzania lub eliminowania połączeń?

Główna zasada warstwowania została odziedziczona po LCF Milnera:

• Wnioskowania podstawowe (rozumowanie z wyprzedzeniem), jako abstrakcyjny typ danych thmw oryginalnym podejściu LCF, lub z osobnym sprawdzaniem terminów dowodu w gałęzi teorii typu rodziny (Coq, Matita). Daje to pewną logiczną podstawę wyników, które prover uważa za twierdzenia. Więc możesz mieć prymitywne wnioskowanie, które bierze ⊢ A i ⊢ B i daje ci ⊢ A ∧ B.Inne prymitywne wnioskowanie mogłoby dać ci ⊢ t = u, gdzie u jest beta-normalną formą t. Żaden z tych mechanizmów nie jest jednak taktyką, są to reguły wnioskowania jak w standardowej logice.

• Dowód ukierunkowany na cel (rozumowanie wstecz). Chodzi o to, że operujesz pewnym pojęciem „stanu celu”, dopracowując go, dzieląc go na coraz więcej poddań, zamykając podzadania, aż wszystko zostanie rozwiązane. Wykończenie stanu celu spowoduje, że pewne twierdzenie wyskoczy z procesu. LCF wprowadził pewną nielogiczną infrastrukturę dla celów, która wciąż istnieje w HOLS: taktyka to pewna funkcja ML, która doprecyzowuje cel i daje pewne uzasadnienie dla udoskonalenia. Na samym końcu dowodu uzasadnienia są odtwarzane w odwrotnej kolejności, aby uzyskać dowód w sposób postępujący zgodnie z pierwotnymi wnioskami zarysowanymi powyżej.

Coq i Matita są nadal bardzo blisko tej zasady LCF. Isabelle jest tutaj inna: już w 1989 roku Larry Paulson zreformował pojęcia celu i taktyki, aby zbliżyć je do logiki, która jest tutaj „czystą” logiczną ramą Isabelle. Isabelle / Pure zapewnia minimalną logikę wyższego rzędu z implikacją ==> i kwantyfikatorem !! które wskazują zarówno strukturę naturalnych reguł dedukcyjnych, jak i stany docelowe.

Na przykład ⊢ A ==> B ==> A ∧ B jest regułą wprowadzania koniunkcji (logiki obiektowej) jako twierdzenie o strukturze logicznej.

Stany celu są również tylko twierdzeniami, zaczynającymi się od ⊢ C ==> C dla początkowego roszczenia C, które jest dopracowane do ⊢ X ==> Y ==> Z ==> C w stanach pośrednich, gdzie X, Y, Z są bieżącymi podzadaniami, a proces kończy się na ⊢ C (brak podzadań).

Wracając do taktyki, która jest bardziej jednolita dla wszystkich tych dowodów: biorąc pod uwagę pewne pojęcie stanu celu (np. Isabelle powyżej), taktyka jest funkcją, która odwzorowuje stan celu na (0, 1 lub więcej) kontynuację stany celu. Co więcej, taktyka jest kombinatorem takich funkcji taktycznych, np. Do wyrażania sekwencyjnego składu, wyboru, powtarzania itp. W rzeczywistości język taktyki i taktyki jest powiązany z podejściem „listy sukcesów” kombinatorów parsera.

Taktyka pozwala na systematyczne opisywanie niektórych strategii udoskonalania celów. Okazały się całkiem udane od czasu wynalezienia ich w LCF w latach 70. i 80., ale produkują notorycznie nieczytelne skrypty próbne.

Najnowszy przegląd niektórych aspektów języków taktycznych podany jest w pracy A. Asperti i in., PLMMS 2009, patrz materiały warsztatowe na stronie 22.

Mizar i Isabelle / Isar zostały wymienione jako alternatywne podejścia do ustrukturyzowanego rozumowania czytelnego dla człowieka i nie opierają się one na taktyce w tym sensie. Mizar nie jest związany z rodziną LCF, więc nie zna tej terminologii taktycznej. Isabelle / Isar do pewnego stopnia włącza tradycję taktyczną, ale jej koncepcja dowodu jest nieco bardziej ustrukturyzowana (z wyraźnym kontekstem dowodu Isar, wyraźnym wskazaniem powiązanych faktów i unikaniem wewnętrznego hakowania celów w trakcie rozumowania).

W ciągu ostatnich dziesięcioleci dokonano wielu dalszych reform i ponownych rozważań dotyczących języków taktyki. Na przykład niedawna gałąź społeczności Coq faworyzuje SSReflect (autorstwa G. Gonthiera) zamiast tradycyjnego Ltac.

Jak działają „taktyki” w asystentach dowodowych?

Podejrzewam, że ta odpowiedź będzie trochę kłopotliwa.

Po pierwsze, nie wystarczy zapytać „jak działają taktyki w asystentach dowodu”, ponieważ działają one inaczej w różnych asystentach dowodu. Istnieją obecnie dwie główne klasy asystentów: pochodzące z oryginalnego LCF, takie jak Isabelle, HOL i HOL light, oraz asystenci dowodowi, tacy jak Coq i Matita. W tych dwóch różnych klasach asystenta dowodu taktyka działa na różne sposoby, co jest odzwierciedleniem tego, że to, co dzieje się pod maską np. Isabelle, jest zupełnie inne niż to, co dzieje się pod maską np. Matita.

Zadaj sobie pytanie: co się dzieje, gdy próbujemy udowodnić propozycję P w Maticie? Wprowadzamy metawymiar X z typem P. Następnie, że tak powiem, gramy w grę, w której dopracowujemy X, dodając coraz więcej struktur do niepełnego terminu, aż otrzymamy pełny termin lambda (tj. Nie zawierający już więcej metawapiennych). Kiedy będziemy już w posiadaniu pełnego terminu lambda, sprawdzamy go w odniesieniu do P, upewniając się, że zamieszkuje on wymagany typ. Widzimy następnie, że w Coq i Maticie taktyka jest jedynie funkcją od niepełnych warunków dowodowych do niekompletnych warunków dowodowych, co, miejmy nadzieję, dodaje nieco struktury do terminu po zastosowaniu (ta obserwacja uzasadniła sporo niedawnej pracy, np. Jojgova , Pientka i inni).

Na przykład, taktyka „wprowadzenie” Matity wprowadza abstrakcję lambda w stosunku do istniejącego terminu, „przypadki” wprowadza wyrażenie dopasowania w tym wyrażeniu, a „zastosowanie” wprowadza zastosowanie jednego terminu do drugiego. Te podstawowe taktyki można łączyć ze sobą, używając funkcji wyższego rzędu, aby tworzyć bardziej złożone. Podstawowa idea jest zawsze taka sama: taktyka zawsze ma na celu dodanie odrobiny struktury do niepełnego terminu próbnego.

Zauważ, że realizatorzy starają się zwrócić termin, który sprawdza typ po każdym zastosowaniu taktyki. Ściśle mówiąc, nie ma dla nich wymogu, ponieważ dla asystentów dowodu opartych na teorii typów ważne jest tylko to, że gdy użytkownik przyjdzie do Qed dowód, jesteśmy w posiadaniu terminu dowodu, który zamieszkuje twierdzenie P. Jak my dotarł do tego terminu dowodu jest w dużej mierze nieistotne. Jednak zarówno Coq, jak i Matita starają się zwrócić użytkownikowi (być może niekompletny) dowód, który sprawdza typ po każdym zastosowaniu taktyki. Jednak ten niezmiennik może (i często się nie udaje), szczególnie w odniesieniu do dwóch kontroli składniowych, które muszą przeprowadzić asystenci ds. Dowodu opartego na CIC.

W szczególności możemy przeprowadzić coś, co wydaje się być ważnym dowodem, stosując szereg taktyk, dopóki nie pozostaną otwarte cele. Następnie dochodzimy do Qed rzekomego dowodu, aby odkryć, że moduł sprawdzania zakończenia Matity lub jego ścisły moduł sprawdzania pozytywności narzeka, ponieważ termin dowodu wygenerowany przez taktykę unieważnił jedną z tych kontroli składniowych (tj. Meta-zmienną w pozycji argumentu do wywołanie rekurencyjne zostało utworzone z terminem, który nie jest składniowo mniejszy niż oryginalny argument). Jest to odzwierciedlenie, że teoria typów CIC jest w pewnym sensie „niewystarczająco silna” i nie odzwierciedla wymagań dotyczących składni i dodatnich wielkości w jej typach (obserwacja, która motywuje typy wielkościowe Abla, oraz niektóre niedawne prace nad typami dodatnimi ).

Z drugiej strony asystenci dowódcy w stylu LCF są zupełnie inni. Tutaj jądro składa się z modułu (zwykle zaimplementowanego w wariancie ML), zawierającego abstrakcyjny typ „thm” oraz funkcji, które implementują reguły wnioskowania logiki asystenta dowodu, odwzorowując „thm” na „thm” i tak dalej naprzód. Opieramy się na dyscyplinie pisania na maszynie ML, aby zapewnić, że jedynym sposobem konstruowania wartości typu „thm” są te reguły wnioskowania (podstawowe taktyki). Jądro Isabelle jest tutaj .

Dowody składają się z szeregu zastosowań tych podstawowych taktyk (lub bardziej złożonych, większych taktyk, które są ponownie tworzone przez połączenie prostszych taktyk za pomocą funkcji wyższego rzędu --- w Isabelle funkcje wyższego rzędu, zwane taktycznymi, mogą być tutaj ). W przeciwieństwie do asystentów dowodowych opartych na teorii typów, asystent w stylu LCF nie musi utrzymywać wyraźnego świadka w dowodzie. Prawidłowość dowodu jest gwarantowana przez konstrukcję, a nasze zaufanie do dyscypliny pisania ML (jednak wielu asystentów, np. Isabelle, generuje warunki dowodu dla swoich dowodów).