You are not logged in |
Prerun wykładów habilitacyjnych
- Speaker(s)
- Bartek Klin
- Affiliation
- Uniwersytet Warszawski
- Date
- Jan. 16, 2012, 10:15 a.m.
- Room
- room 4790
- Seminar
- Seminar Semantics, Logic, Verification and its Applications
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.
