Seminarium Semantyka, Logika I Weryfikacja Oraz Wiele Ich Ciekawych Aplikacji (SLIWOWICA)

Prelegent: Bartek Klin

TEMAT 1:  Mądrej głowie dość dwie słowie, czyli dowody probabilistycznie sprawdzalne

Jak sprawdzić, czy dowód twierdzenia matematycznego jest poprawny, nie czytając go w całości? Dla pewnej klasy problemów i dowodów jest to możliwe. Dowód probabilistycznie sprawdzalny to taki, który można sprawdzić za pomocą algorytmu randomizowanego w ten sposób, że jeśli dowód jest poprawny, to z pewnością zostanie zaakceptowany, a jeśli jest błędny, to zostanie odrzucony z dużym prawdopodobieństwem. Okazuje się, że często algorytmowi sprawdzającemu wystarczy sprawdzić tylko niewielką część sprawdzanego dowodu.

TEMAT 2: Zbiory nominalne, czyli algebra wiązania zmiennych

Indukcja strukturalna to podstawowe narzędzie do operowania na termach zbudowanych nad sygnaturami algebraicznymi. Jej stosowanie jest bardziej problematyczne dla języków z wiązaniem zmiennych, takich jak rachunek lambda czy rachunek pi. Chociaż termy w takich językach są formalnie traktowane z dokładnością do alfa-konwersji, jednak w praktyce operacje na nich są definiowane dla konkretnych wyborów zmiennych związanych, a dowody niezależności tych definicji od wyboru zmiennych są często pomijane. W wykładzie opowiem o zbiorach nominalnych, czyli pewnym modelu, który pozwala pogodzić indukcję strukturalną z alfa-konwersją.

TEMAT 3: Paradoks Alabamy i inne kłopoty z demokracją

W demokracji parlamentarnej regularnie stajemy przed koniecznością podziału mandatów między partie polityczne proporcjonalnie do liczby uzyskanych głosów. Ponieważ pojedynczych mandatów nie można dzielić, uzyskanie doskonałej proporcjonalności jest niemożliwe i niezbędna jest metoda zaokrąglania uzyskanych wyników. Okazuje się, że pewne proste i intuicyjnie przekonujące metody prowadzą do nieoczekiwanych sytuacji takich jak paradoks Alabamy i paradoksy populacyjne. W wykładzie podam kilka naturalnych własności, które powinna mieć idealna metoda podziału mandatów. Opowiem też o klasycznym twierdzeniu, które mówi, że żadna metoda nie ma wszystkich tych własności.