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