Szymbark lezy mniej wiecej 30 km od granicy i 30 km od Nowego Sacza na wschod, w Beskidach.
38 - 311 Szymbark k/Gorlic Osrodek Wypoczynkowy PAN tel. (0 - 18) 52-67-20
W liniowym rozsylaniu pakiety informacji poczatkowo znajdujace sie w jednym wezle sieci, zwanym zrodlem, musza przewedrowac przez wszystkie pozostale wezly. Z kazdym pakietem zwiazana jest z gory zadana droga, po ktorej ten pakiet moze wedrowac. Zaklada sie, ze kazdy uszkodzony element sieci, wezel lub lacze, niszczy kazdy pakiet przechodzacy przez ten element. Powiemy, ze dany schemat liniowego rozsylania (zbior drog dla pakietow) toleruje f uszkodzen w sieci, jezeli kazdy wezel w sieci zostanie odwiedzony przez co najmniej jeden pakiet, niezaleznie od miejsca wystapienia uszkodzen. (Zrodlo nigdy nie jest uszkodzone.) Na wykladzie podano oszacowanie na minimalna liczbe pakietow, dla ktorej istnieje schemat liniowego rozsylania tolerujcy f uszkodzen w sieci pelnej.
Bibliografia
W referacie przedstawilem probe rozszerzenia izomorfizmu Curry-Howarda na przypadek klasycznej logiki liniowej. Mamy wiec bijekcje pomiedzy formulami logiki liniowej a pewnego rodzaju specyfikacjami dla Pi-rachunku oraz dowodami logiki liniowej a procesami Pi-rachunku. Izomorfizm ten podany jest w rzeczywistosci na poziomie struktur dowodow. Rozne strategie normalizacji dowodow odpowiadaja wtedy technikom ewaluacji procesow Pi-racnunku. Na koncu podalem twierdzenia o adekwantnosci i pelnosci tlumaczenia dla addytywnego i multiplikatywnego fragmentu logiki liniowej.
Bibliografia
Wprowadzenie do logiki liniowej; rachunek sekwentow, sieci dowodow (dla fragmentu multiplikatywnego logiki) jako odpowiednik naturalnej dedukcji; przyklady dowodow w logice liniowej.
Rachunek Mi to system logiczny oparty na operatorach
indukcji i ko-indukcji, ktory w bardzo oszczednej notacji
jest zdolny wyrazic wlasnosci obliczen nieskonczonych.
Przedstawilem zreby tego rachunku w jego najbardziej
abstrakcyjnej postaci.
Byl to tzw wyklad przy piwie.
Dowody interakcyjne i pokrewne pojecie dowodow bez przekazywania informacji (ang. zero-knowledge proofs) to nowy paradygmat obliczenia, ktory znajduje zaskakujace zastosowania w teorii zlozonosci a takze w kryptografii z jawnym kluczem. Przedstawilem idee twierdzenia Shamira o rownowaznosci dowodow interakcyjnych z jednym proverem i klasy PSPACE, a takze zasosowanie dowodow interakcyjnych z wieloma proverami do wykazania, ze problemu kliki nie da sie aproksymowac w czasie wielomianowym przy zalozeniu, ze P =/= NP (rezultaty Arory i Safry).
Wyklad omawial dwa proste algorytmy wyszukiwania wzorca w tekscie, ktore dzialaja w czasie liniowym i uzywaja stalej pamieci. Pierwszy z nich oparty byl na technice zoomingu ktora polega na wyszukiwaniu w tekscie coraz dluzszych nieokresowych przyblizen wzorca. Nieokresowosc wyszukiwanych slow powoduje ze praca wykonywana przy porownywaniu symboli slowa i tekstu jest amortyzowana przez przesuniecie. Drugi algorytm wykorzystuje dwie techniki: technike zoomingu oraz technike probkowania. Zaleta tego algorytmu jest jego prostota oraz liczba porownan ktora ten algorytm wykonuje. Mozna udowodnic ze algorytm ten wykonuje co najwyzej 2n porownan gdzie n jest rozmiarem tekstu.
Oboz byl finansowany z funduszu Rady Kol Naukowych UW.
Deszcz padal, szkoda; i nikt zdjec nie robil, tez szkoda.
kni@zls.mimuw.edu.pl