Opis
Kiedy sto lat temu Russel i Whitehead zaczynali konstruować podstawy matematyki, było to długie i niewdzięczne zajęcie. Dowód faktu, że 1+1=2, zajął 362 strony…
"We are doing ants' work…"
Logicomix: An Epic Search for Truth
Sytuacja zmieniła się, gdy pojawiły się komputery. Poziom szczegółów, który dla człowieka piszącego na papierze jest bardzo ciężko strawny, z użyciem komputera staje się całkiem znośny. W efekcie mamy dowód, w którym wszystkie przejścia mogą być automatycznie zweryfikowane. Rozmaite twierdzenia na temat zbiorów, grup i pierścieni, liczb rzeczywistych, czy rachunku prawdopodobieństwa, całkiem dosłownie mają swój kod źródłowy.
Innym zastosowaniem komputerowego dowodzenia twierdzeń jest weryfikacja programów. Ludowa mądrość głosi, że nie ma programów bez błędów, ale to właśnie obiecuje formalna weryfikacja - mamy więc np. kompilator C, którego poprawność została matematycznie udowodniona!
Możliwa jest nawet ekstrakcja programu - wygenerowanie kodu źródłowego na podstawie dowodu (piszemy dowód zdania "dla każdej listy istnieje jej permutacja, która jest uporządkowana" i dostajemy funkcję sortującą listy). Ci, którzy słyszeli co nieco o rachunku lambda, pewnie domyślają się, na czym to polega.
Na warsztatach chcę przede wszystkim pokazać, że pisanie dowodów na komputerze to świetna zabawa - pod pewnymi względami przypomina programowanie, ale zamiast wskaźników i tablic manipulujemy czystą matematyczną Prawdą :)
Dla kogo
- dla matematyków, których ciekawi logika i podstawy matematyki,
a także
- dla informatyków, którzy czerpią przyjemność z programowania, i lubią poznawać nowe języki i paradygmaty.
Wstępny program
- dowody w logice zdaniowej i pierwszego rzędu
- interaktywne dowodzenie twierdzeń: zbudujemy jakiś kawałek matematyki od podstaw
- być może również weryfikacja programów
- na koniec trochę o różnych narzędziach, formalizmach i zastosowaniach
Warsztaty będą polegać głównie na "klepaniu kodu" na komputerze. Postaram się przygotować paczkę z odpowiednimi narzędziami.
Wymagania
Obycie z formułami logiki zdaniowej i pierwszego rzędu. Zadania kwalifikacyjne będą to sprawdzać.
Jeśli ktoś chciałby poczytać więcej, może zajrzeć do skryptu z Podstaw Matematyki prof. Urzyczyna z MIM UW. Warsztaty zaczniemy od naturalnej dedukcji, choć niekoniecznie w dokładnie takiej postaci, w jakiej jest w skrypcie.
Zadania kwalifikacyjne
Zadania znajdują się tu: thp-kwalifikacja.pdf (ostatnia poprawka 12 lipca).
Rozwiązania wysyłajcie na moc.liamg|celopmuh#moc.liamg|celopmuh, lub poprzez warsztatową aplikację. Jeśli ktoś zauważy błędy w zadaniach, również proszę o wiadomość.
Materiały
Isabelle - system, z którego korzystamy
Wręczałt z naturalną dedukcją i podstawami obsługi Isabelle
Źródła
Naturalna dedukcja + rozwiązania
Liczby naturalne + rozwiązania
Do dalszego czytania
Isabelle Primer na temat dowodzenia twierdzeń, uczy pisania strukturyzowanych dowodów (Isar), nie "apply"
Tutorial koncentrujący się bardziej na weryfikacji programów (ale mówi też o matematyce - zbiorach, relacjach itd.)