Nie jesteś zalogowany |
Prerun wykładów habilitacyjnych
- Prelegent(ci)
- Bartek Klin
- Afiliacja
- Uniwersytet Warszawski
- Termin
- 16 stycznia 2012 10:15
- Pokój
- p. 4790
- Seminarium
- Semantyka, Logika I Weryfikacja Oraz Wiele Ich Ciekawych Aplikacji
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.
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.
