Programowanie w Logice

Warszataty najprawdopodobniej nie odbędą się z powodu niedyspozyjności prowadzącego. Nadal szukamy zastępstwa.

Opis

Większość (szczególnie młodych) programistów jest przyzwyczajona do tzw. programowania imperatywnego. W owym paradygmacie traktujemy program jak coś w stylu przepisu kulinarnego w którym deklarujemy jakieś składniki (zmienne) i określamy kolejne kroki które mają być wykonane, na przykład

1. Pokrój kurczaka
2. Wypakuj kurczaka z opakowania
3. Napal w piecu
4. Dosyp piasku
5. Napełnij kurczaka wodą
6. Obracaj na rożnie przez 4 godziny w temperaturze 23 st. Celsjusza
7. Dopraw solą i serwuj

(zawsze byłem w to słaby)

Okazuje się jednak że nie wszystkie programy muszą być definiowane w ten sposób. Obsługa zmiennych i rozróżnianie stanu programu "przed" i "potem" staje się problematyczna w sytuacjach w których mamy doczynienia z większym codebasem, więc w systemach dużej skali stopniowo się od nich odchodzi na rzecz tzw. programowania funkcyjnego w którym programy są jedynie nieruchomymi zbiorami funkcji, które jedyne co opisują to wynik obliczenia z zadanych argumentów – bez żadnych efektów ubocznych, zmieniających się rzeczy czy "kolejnych kroków". Po prostu wynik.

Takie podejście cechuje się wprawdzie nieco mniejszą wydajnością, ale zwraca się wielokrotnie w postaci dużo bardziej czytelnego kodu, o którym można wiele więcej powiedzieć w oderwaniu od jego kontekstu.

Na tych warsztatach posuniemy się o krok dalej. Poznamy paradygmat programowania w logice, w którym nie dość, że nie budujemy imperatywnych sekwencji instrukcji, to również nie definiujemy funkcji które rozdzielają dziedzinę od przeciwdziedziny. W tym, nie ukrywając – egzotycznym, podejściu ograniczamy się do opisywania co jest prawdziwe zamiast co jest czym lub co ma się dziać, a runtime naszego języka zajmie się domyślaniem się jak dopasować wartości zmiennych tak, by nasze założenia zaszły. W ten sposób nie dość, że nasza praca ogranicza się do napisania samej specyfikacji programu, to jeszcze zupełnie naturalnie dopuszczamy wielokrotne wyniki oraz zacieramy koncepcyjną granicę między daną, a wynikiem.

Magia? Jak wszystkie inne niesamowite rzeczy na tym świecie – nie. Na warsztatach nauczymy się nie tylko jak programować przy użyciu surowych predykatów logicznych, ale też sięgniemy wiedzy co się dzieje za kurtyną algorytmu stanowiącego mózg naszego systemu.

Btw, wspomniałem że język nazywa się Prolog?

Wymagania

Wymagane cechy i umiejętności:

1. Znajomość logiki matematycznej na poziomie licealnym + ogarnianie czym są modele logiczne
2. Programowanie w dowolnym języku na poziomie podstawowym
3. Umiejętność korzystania z rekurencji
4. Indukcja matematyczna
5. Laptop z Linuxem byłby spoko

Przydatne rzeczy

Z przyjemnością odpowiem na wszelkie pytania i wątpliwości. Piszcie na mejla: radrowicki w popularnej domenie googla.

Warto wiedzieć:

• Model w rachunku zdań to po prostu wartościowanie zmiennych: przypisanie każdej z nich jakiejś wartości (tutaj, prawda/fałsz).
• Model w logice I oraz II rzędu to nośnik (dowolny zbiór czegokolwiek) oraz ustalone wyniki predykatów zaaplikowanych do elementów nośnika. Przykładowy model dla formuły ∀x ∃ y. p(y, y) /\ not q(x, y) to zbiór {1, 2, 3} oraz założenia p(1, 1), q(1, 1), q(2, 3), q(2, 2).
• W logice I oraz II rzędu nie ma zmiennych wolnych, czyli "niezadeklarowanych" w żadnym kwantyfikatorze poziom wyżej. Przykładowo, w ∀x. x \/ y zmienna y jest wolna, a x związana.
• Formuła jest spełnialna jeśli istnieje model w którym jest ona prawdziwa.
• Formuła jest tautologią jeśli jest prawdziwa w każdym modelu.

Uwaga: Od edycji 2021, uczestnicy przesyłają rozwiązania przez stronę, a nie prowadzącym na maila.