Programowanie dowodami

Prowadzący: Radosław Rowicki

Nauczymy się masakrować bugi przy użyciu faktów i logiki

Zadania kwalifikacyjne

Kategorie: informatyka teoretyczna

Opis

Nie powinno być niespodzianką, że wiele konceptów z informatyki i logiki jest powiązanych ze sobą tak silnie, że można wręcz je ze sobą scalić i traktować jak identyczne. Jednym z ciekawszych przykładów tego zjawiska jest tzw "izomorfizm Curry'ego i Howarda", który wskazuje na równoważność zdań logicznych oraz typów (takich jak znany i lubiany int). Ekwiwalentnie, dowody owych twierdzeń zrównywane są z wartościami reprezentującymi te typy. W ten sposób można by rzec że 3 jest "dowodem" na inta.

Na warsztatach wprowadzę was w podstawy programowania funkcyjnego w jęzku o majestatycznej nazwie Coq /kok/. Język ten, jak nazwa absolutnie nie wskazuje, jest znany przede wszystkim jako narzędzie do pół-automatycznego dowodzenia twierdzeń matematycznych oraz weryfikacji własności programów. Wspomniany wcześniej izomorfizm jest tym co sprawia, że to pozornie dziwne zastosowanie ma sens, a to wszystko dzięki POTĘŻNEMU systemowi typów jaki oferuje Coq.

Plan

Poznamy Coq jako funkcyjny język programowania. Nauczymy się pisać proste programy funkcyjne i operować funkcjami wyższych rzędów.
Zagłębimy nieco w teoretyczne podstawy teorii typów i zastanowimy się co tam się dzieje pod spodem.
Znienacka wjedzie logika. Ale nie taka zwykła logika co ty gadasz mówie ci złą logikę miałeś ja ci załatwie inną spróbuj ja ci co jakie w liceum była co ty gadasz inną musisz spróbować bo różne sa
Napiszemy nasze pierwsze twierdzenie w Coq i udowodnimy je tylko po to by ogarnąć że już to zrobiliśmy wcześniej
Poznamy język taktyk dowodowych oferowanych przez Coq żeby sprawniej trzaskać dowodziki
W zależności od czasu, będziemy tłuc dowody na liczbach naturalnych, listach, może nawet drzewach i będziemy masakrować bugi przy użyciu faktów i logiki

Wymagania

Wymagane cechy i umiejętności:

Rozumienie indukcji matematycznej
Ogarnianie rekurencji
Programowanie w jakimś języku, najlepiej ze statycznymi typami (dla pythoniarzy mypy)
Komputer i umiejętność instalowania rzeczy na nim

Przydatne rzeczy

Jeśli Python to jedyny język jaki znasz, polecam zapoznać się z https://mypy-lang.org/
Biblia izomorfizmu Curry'ego i Howarda (oraz rachunku lambda): https://disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard.pdf
Przyjemny kalkulator lambd i wstęp do rachunku: https://crypto.stanford.edu/~blynn/lambda/ (może trochę spoilerować zadanka)
Jeśli planujesz przyjść z niemowlakiem, ta gra powinna dobrze przygotować go do zajęć: https://worrydream.com/AlligatorEggs/

Przygotowanie do zajęć

Zainstaluj opam. To taki pip tylko do OCamla, a że Coq jest napisany w OCamlu no to no.
Zainstaluj Coq wpisując w terminalu ("konsoli") swojego komputera opam update && opam pin add coq 8.18.0 && opam install coq
Zainstaluj obsługę Coq w swoim ulubionym edytorze:
- Jeśli używasz vima lub emacsa to nie będę układał ci życia, ogarnij sobie to w swoim brzydkim configu
- Jeśli używasz VS Code, zainstaluj dodatek VsCoq i wpisz w terminalu opam install vscoq-language-server
- Jeśli chcesz używać edytora dostarczonego przez twórców Coq, to zainstaluj coqide, na przykład tak: opam install coqide
Sprawdź czy działa:

Stwórz plik o nazwie test.v i wpisz w nim takie coś:

Theorem lubie_placki : True.
Proof. trivial. Qed.

Następnie ustaw kursor na końcu pliku i w zależności od edytora kliknij:

Emacs: C-c C-RET
Vim: ???
VS Code: Alt-<right> / <option>-<right> (lub odpal "interpret to point" z menu komend)
CoqIDE: Ctrl-<right> (możliwe że Cmd-<right> na macu)

Całość (wraz z Qed) powinna podświetlić się na jakiś kolor.

Kontakt

Można pisać na maila radrowicki w popularnej domenie Googla.