Biorąc pod uwagę tematy poruszane na konferencji, takie jak STOC, czy naukowcy zajmujący się algorytmem lub złożonością aktywnie korzystają z COQ lub Isabelle? Jeśli tak, to jak wykorzystują go w swoich badaniach? Zakładam, że większość ludzi nie użyłaby takich narzędzi, ponieważ dowody byłyby zbyt niskie. Czy ktoś używa tych asystentów dowodu w sposób, który ma kluczowe znaczenie dla ich badań, w przeciwieństwie do miłego suplementu?
Jestem zainteresowany, ponieważ mógłbym zacząć uczyć się jednego z tych narzędzi i byłoby fajnie poznać je w kontekście dowodów na zmniejszenie, poprawność lub czas pracy.
Odpowiedzi:
Ogólna zasada jest taka, że im bardziej abstrakcyjna / egzotyczna matematyka ma być mechanizowana, tym łatwiej. I odwrotnie, im bardziej konkretna / znajoma jest matematyka, tym trudniej będzie. Tak więc (na przykład) rzadkie zwierzęta, takie jak predykcyjna topologia bez punktów, są znacznie łatwiejsze do zmechanizowania niż zwykła topologia metryczna.
Początkowo może się to wydawać nieco zaskakujące, ale dzieje się tak głównie dlatego, że konkretne obiekty, takie jak liczby rzeczywiste, uczestniczą w wielu różnorodnych strukturach algebraicznych, a dowody z nimi związane mogą korzystać z dowolnej właściwości z dowolnego ich widoku. Aby więc być w stanie zrozumieć zwykłe rozumowanie, do którego matematycy są przyzwyczajeni, musisz zmechanizować wszystkie te rzeczy. W przeciwieństwie do tego, wysoce abstrakcyjne konstrukcje mają (celowo) mały i ograniczony zestaw właściwości, więc musisz zmechanizować znacznie mniej, zanim dojdziesz do dobrych bitów.
Dowody w teorii złożoności oraz algorytmach / strukturach danych (z reguły) wykorzystują wyrafinowane właściwości prostych gadżetów, takich jak liczby, drzewa lub listy. Np. Argumenty kombinatoryczne, probabilistyczne i teoretyczne rutynowo pojawiają się jednocześnie w twierdzeniach teorii złożoności. Uzyskanie wsparcia biblioteki asystenta dowodu do tego stopnia, że jest to przyjemne do zrobienia, to sporo pracy!
Jednym z kontekstów, w których ludzie chętnie angażują się w pracę, są algorytmy kryptograficzne. Istnieją bardzo subtelne ograniczenia algorytmiczne ze złożonych przyczyn matematycznych, a ponieważ kod kryptograficzny działa w środowisku przeciwnym, nawet najmniejszy błąd może być katastrofalny. Na przykład w ramach projektu Certicrypt zbudowano wiele infrastruktury weryfikacyjnej w celu budowania sprawdzanych maszynowo dowodów poprawności algorytmów kryptograficznych.
źródło
Jednym z bardzo znaczących przykładów jest oczywiście formalizacja Gonthiersa Coqa twierdzenia o 4 kolorach w Coq, który wykorzystuje wiele kombinacji.
Mój kolega Uli Schöpp wykorzystał do tego celu bibliotekę ssreflect opracowaną przez Gonthiera w celu zweryfikowania (i nieznacznego rozszerzenia) również w Coq wyniku Cooka i Rackoffa na automatach grafowych. https://scholar.google.at/scholar?oi=bibs&cluster=4944920843669159892&btnI=1&hl=de (Schöpp, U. (2008). Sformalizowana dolna granica nieukierunkowanej dostępności grafów. W logice programowania, sztucznej inteligencji i uzasadnienia ( str. 621-635). Springer Berlin / Heidelberg.)
źródło