Programowanie dowodami

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:

1. Rozumienie indukcji matematycznej
2. Ogarnianie rekurencji
3. Programowanie w jakimś języku, najlepiej ze statycznymi typami (dla pythoniarzy mypy)
4. 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/

Kontakt

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

Mem