Foundations of Computer Science

Theoretical Computer Science
Faculty of Mathematics and Computer Science
Jagiellonian University

Computer Science Foundations Seminar

Wednesday: 12:15 - 14:00, room 117

Research seminar devoted to problems related to asymptotic densities in logic, computability theory, computational logic, typed lambda calculus, logic programming, logics of programs, functional programming.

table edited by: Marek Zaionc

04.06.2008, Mateusz Kostanek	Quantale semantics of linear logic (2)

28.05.2008, Ken-etsu Fujita, Shimane Univ. Japan	A translation from lambda2 into lambda_exists
	This talk shows that there exist translations between polymorphic lambda calculus and a subsystem of minimal logic with existential types, which form a Galois insertion (embedding). The translation from polymorphic lambda calculus into the existential type system is the so-called call-by-name CPS-translation that can be expounded as an adjoint from the neat connection. The construction of an inverse translation is investigated from a viewpoint of residuated mappings. The duality appears not only in the reduction relations but also in the proof structures such as paths between the source and the target calculi. From a programming point of view, this result means that abstract data types can interpret polymorphic functions under the CPS-translation. We may regard abstract data types as a dual notion of polymorphic functions. This talk is based on an extended and improved version of the paper presented at TLCA2005.
21.05.2008, Mateusz Kostanek	Quantale semantics for linear logic

14.05.2008, Jakub Kozik	Realizability

07.05.2008, Bożena Woźna, Akademia im. Jana Długosza, Częstochowa	Ograniczona Weryfikacja Modelowa dla systemów wieloagentowych i systemów z czasem
	W referacie przedstawię wyniki moich badań w zakresie automatycznej weryfikacji modelowej systemów czasu rzeczywistego oraz systemów wieloagentowych. Wyniki te zostały osiągnięte we współpracy z prof. Wojciechem Penczkiem (IPI PAN Warszawa), dr Andrzejem Zbrzeznym (AJD, Częstochowa) oraz dr Alessio Lomuscio (UCL, Londyn). W szczególności opowiem o zaproponowanej przeze mnie Ograniczonej Weryfikacji Modelowej, którą zastosowałam zarówno do systemów z czasem jak i systemów wieloagentowych. Zrobię również krótkie wprowadzenie do formalizmów stosowanych w automatycznej weryfikacji modelowej wy?ej wymienionych systemów. System czasu rzeczywistego to (zgodnie z definicją IEEE) system, którego poprawność działania zależy nie tylko od poprawności logicznych rezultatów, lecz również od czasu, w jakim te rezultaty są osiągane. Systemy czasu rzeczywistego znajdują zastosowanie między innymi w przemyśle do nadzorowania procesów technologicznych, przy implementacji protokołów komunikacyjnych, w planowaniu i kontroli ruchu lotniczego, itd. Agent to jednostka, która działa w pewnym ustalonym środowisku, jest zdolna do komunikowania się, monitorowania swego otoczenia i podejmowania autonomicznych decyzji. System wieloagentowy to sieć komunikujących się i współpracujących między sobą agentów, realizujących zarówno wspólne jak i prywatne cele. Systemy wieloagentowe mają już swoją ugruntowaną pozycję w wielu dziedzinach związanych z technologią informacji, np.: w inżynierii oprogramowania, e-handlu, sieciach telekomunikacyjnych, automatycznym wnioskowaniu i argumentacji, wspomaganiu zarządzaniem w przedsiębiorstwie, itd. Weryfikacja modelowa jest jedną z najbardziej rozpowszechnionych metod automatycznej weryfikacji poprawności systemów czasu rzeczywistego oraz systemów wieloagentowych. Pierwsze prace na ten temat ukazały się w 1981 roku i od tamtego czasu trwa nieustanny rozwój narzędzi wykorzystujących udoskonalane algorytmy. Różnorodność dostępnych podejść, jak też rozwiązań, jest wynikiem istnienia wielu modeli dla wyżej wymienionych systemów, np. przeplotowych i nieprzeplotowych, jak też wielu metod opisu własności tych systemów, np. poprzez automaty, algebry procesów lub logiki temporalne. Istotny postp w dziedzinie weryfikacji dokonał się w 1990 roku po opracowaniu metod bazujących na obliczeniach symbolicznych, wykorzystujących formalizm Boolowskich Diagramów Decyzyjnych. Następny krok do przodu został wykonany w 1999 roku po sprowadzeniu problemu weryfikacji modelowej do problemu testowania spełnialności dla formuł zdaniowych i wykorzystaniu efektywnych algorytmów dla tego ostatniego problemu.
23.04.2008, Mateusz Juda	Arytmetyka Heytinga
	Na podstawie skryptu Thomasa Streichera (patrz poprzednie referaty tego samego autora).
16.04.2008, Tomasz Połacik, Uniw. Śląski	Modele Kripkego dla teorii pierwszego rzędu
	Druga część referatu jest poświęcona modelom Kripkego dla logiki pierwszego rzędu. Omówimy podstawowe własności modeli i twierdzenie o pełności. Przedstawimy w niej również rezultaty dotyczące konstrukcji modeli Kripkego dla intuicjonistycznych teorii pierwszego rzędu, ze szczególnym uwzglednieniem Arytmetki Heytinga.
09.04.2008, Tomasz Połacik, Uniw. Śląski	Modele Kripkego dla intuicjonistycznej logiki zdań
	W pierwszej części referatu zajmiemy się zagadnieniami związanymi z modelami Kripkego dla intuicjonistycznej logiki zdań. Poza podstawowymi własnościami i intuicjami dotyczącymi modeli, przedstawione zostanie twierdzenie o pełności Rachunku Heytinga względem semantyki kripkowskiej. Omówimy też najważniejsze konstrukcje modeli Kripkego i pokażemy semantyczne dowody niektórych własności Rachunku Heytinga.
02.04.2008, Paweł Waszkiewicz	O analizie infinitezymalnej w światach gładkich
	Zanim zaproponowano pojęcie granicy, matematycy tacy jak Fermat czy Leibnitz posługiwali się w dowodach swoich twierdzeń analitycznych pojęciem wartości nieskończenie małych. Podczas seminarium opowiem o rachunku wartości nieskończenie małych, który przypomina metody analityczne sprzed 350-400 lat, ale - w odróżnieniu od nich - jest doskonale precyzyjny. Modele tego rachunku nz. światami gładkimi. Co czyni światy gładkie ciekawymi jest m.in. fakt, iż w takim świecie prosta rzeczywista R jest prawdziwym continuum, tzn. nie można z niej wydzielić żadnego nietrywialnego podzbioru. (Podzbiór U wydziela się z R, jeśli dla każdego x z R albo x należy do U, albo x nie należy do U.) Wykład przygotowałem na podstawie: J.L.Bell, A Primer on Infinitesimal Analysis, Cambridge Univ. Press, 1998. Google: ,,John L. Bell''. Warto.
19.03.2008, Mateusz Juda	Introduction to Constructive Logic and Mathematics (II)
	Omawiamy kolejne tematy ze skryptu Thomasa Streichera. Dzisiaj: - Constructive Arithmetic and Analysis - Constructive Real Numbers
12.03.2008, Jakub Kozik	Jak wiele formuł ma konstruktywne dowody?
	W referacie przedstawię wyniki otrzymane z A. Genitrini dotyczące ilościowego porównania zdaniowych logik: klasycznej i intuicjonistycznej. W rozważanych formułach dopuszczamy wszystkie zwykle używane łączniki (koniunkcja, alternatywa, implikacja) oraz stałą "absurd" (bottom). Nasz główny wynik można nieformalnie wypowiedzieć jako: "około 5/8 tautologii logiki klasycznej ma konstruktywne dowody." Ciekawym wynikiem dodatkowym jest zgodność dwóch, pozornie niezależnych, metod liczenia gęstości.
05.03.2008, Mateusz Juda	Introduction to Constructive Logic and Mathematics (I)
	Mateusz referuje pierwszą część skryptu Thomasa Streichera, pod tym samym tytułem, dostępnego TUTAJ. Możemy spodziewać się następujących zagadnień: - Natural Deduction for Constructive Logic - A Hilbert Style System for CL - Truth–Value Semantics of CL - Embedding Classical into CL (Constructive = Intuitionistic)
27.02.2008, Paweł Waszkiewicz	Konstruktywizm wg Bridgesa. Piękno wg Patarai.
	Tematem naszego seminarium w tym semestrze jest konstruktywizm i intuicjonizm. Podczas pierwszego spotkania przedstawię artykuł Douglasa Bridgesa pt. Reality and Virtual Reality in Mathematics, w którym autor daje nam krótki kurs historii matematyki konstruktywnej. Aby zniszczyć humanistyczny nastrój, który nieuchronnie wytworzy się podczas wykładu historycznego, zakończę twardym, ale konstruktywnym dowodem faktu, że każda funkcja monotoniczna f:X->X na posecie zupełnym X, wyposażonym w element najmniejszy, posiada najmniejszy punkt stały. Dowód, pochodzący od gruzińskiego matematyka Dimitriego Patarai, nie używa liczb porządkowych.
23.01.2008, Kacper Marcisz	An application of stream calculus to signal flow graphs
	Pan Kacper referujr artykuł Jana Ruttena pod tym samym tytułem. Dane bibliograficzne artykułu: Proceedings FMCO 2003 (Formal Methods for Components and Objects). Editors: F.S. de Boer, M.M. Bonsangue, S. Graf, W.P de Roever. Lecture Notes in Computer Science 3188, Springer Verlag, 2004, pp. 276-291. Jest to kontynuacja tematyki przedstawionej przez panią Dominikę Majsterek wcześniej na naszym seminarium.
16.01.2008, Szymon Wójcik	Parallel reductions in lambda calculus
	The notion of parallel reduction is extracted from the simple proof of the Church-Rosser theorem by Tait and Martin-Löf. Intuitively, this means to reduce a number of redexes (existing in a lambda term) simultaneously. During the talk, after reevaluating the significance of the notion of parallel reduction in Tait-and-Martin-Löf type proofs of the Church-Rosser theorems, we show that the notion of parallel reduction is also useful in giving short and direct proofs of some other fundamental theorems in reduction theory of lambda calculus.
09.01.2008, Dominika Majsterek UJ	Behavioural differential equations: a coinductive calculus (część 2)
	Pani Dominika referuje artykuł: J.J.M.M. Rutten Behavioural differential equations: a coinductive calculus of streams, automata, and power series. Theoretical Computer Science vol. 308(1-3), pp. 1-53, 2003.
19.12.2007, Mikołaj Bojańczyk, Instytut Informatyki, Uniwersytet Warszawski	Automaty ścieżkowe
	Automat ścieżkowy to rodzaj automatu skończonego na drzewach. W odróżnieniu od powszechnie używanych automatów na drzewach, automat taki przetwarza drzewo sekwencyjnie, a nie równolegle. Pokażę, że automat ścieżkowy mało potrafi.
12.12.2007, Dominika Majsterek	Behavioural differential equations: a coinductive calculus
	Pani Dominika referuje artykuł: J.J.M.M. Rutten Behavioural differential equations: a coinductive calculus of streams, automata, and power series. Theoretical Computer Science vol. 308(1-3), pp. 1-53, 2003. Abstract: We present a theory of streams (infinite sequences), automata and languages, and formal power series, in terms of the notions of homomorphism and bisimulation, which are cornerstones of the theory of (universal) coalgebra. This coalgebraic perspective leads to a unified theory, in which the observation that each of the aforementioned sets carries a so-called final automaton structure, plays a central role. Finality forms the basis for both definitions and proofs by coinduction, the coalgebraic counterpart of induction. Coinductiove definitions take the shape of what we have called behavioural differential equations, after Brzozowski's notion of input derivative. A calculus is developed for coinductive reasoning about all of the aforementioned stuctures, closely resembling calculus from classical analysis.
05.12.2007, Tytus Bierwiaczonek	Logical aspects of finite automata
	Pan Tytus referuje przeglądowy artykuł Wolfganga Thomasa pt. Languages, Automata and Logic. Usłyszymy o zależnościach pomiędzy automatami i monadyczną logiką drugiego rzędu. Artykul dostępny jako [Tho96] na stronie http://www.automata.rwth-aachen.de/publications/pub-Thomas.html albo od razu tutaj .
28.11.2007, Thierry Joly	Undeciding lambda-definability again
	The Definability Problem (DP for short) is the question whether a given functional of some hereditarily finite type structure over a single atomic type is the interpretation of a closed lambda-term or not. DP was first considered about Full Type Structures by G. Plotkin in 1973, [Plo73]. R.Statman [Sta82] pointed out that deciding it would solve at once quite a few existential problems of the typed lambda-calculus, the most famous of which is the (still open) Matching Problem: "Given lambda-terms A, B, is there a lambda-term X such that AX=B?" Then DP became a little Graal, finally proved undecidable by R. Loader in 1993, [Loa01]. Is that the end of the story? One may object that in smaller models than the Full Type Structures, the few lambda-definable functionals would not be so easily lost and that deciding definability in any class of (smaller) models that is strongly complete with respect to the lambda-calculus (in the sense of [Sta82]) would also yield the benefits pointed out by Statman. Unfortunately, we will show in this talk that the restriction of DP to a fixed model M is actually undecidable for a fair amount of models M, including all the non trivial stable models and order extensional models, except possibly the 2 element Scott model. These stronger results were obtained by cleaning previous proofs and by identifying their efficient ingredients. This work of simplification also yields a particularly short and easy proof of the undecidability of DP for Church pure typed lambda-calculus that will first be detailed. [Plo73] Gordon Plotkin. Lambda-definability and logical relations. Memorandum SAI-RM-4, University of Edinburgh, 1973. [Sta82] Richard Statman. Completeness, invariance and lambda-definability. JSL 47:17-26, 1982. [Loa01] Ralph Loader. The Undecidability of lambda-Definability. In Logic, Meaning and Computation: Essays in Memory of A. Church, 331-342, Anderson & Zeleny editors, Kluwer Acad. Publishers, 2001.
21.11.2007, Tomasz Połacik, Instytut Matematyki, Uniwersytet Śląski, Katowice	Problemy modeli Kripkego dla teorii pierwszego rzędu
	Jest faktem ogólnie znanym, że modele Kripkego stanowią ważne i efektywne narzędzie służące do badania intuicjonistycznych teorii pierwszego rzędu. Na przykład, znane są ich liczne interesujące zastosowania w przypadku takich konstruktywnych teorii jak arytmetyka Heytinga czy intuicjonistycza teorii mnogości Kripkego-Platka. Na uwagę zasługuje jednak fakt, że w przeciwieństwie do sytuacji teorii modeli klasycznych, wciąż brakuje ogólnych metod i konstrukcji dla modeli Kripkego. Przypomnijmy, że - nieformalnie - na model Kripkego możemy patrzeć jak na rodzinę klasycznych modeli dla danego języka pierwszego rzędu, w której określony jest porządek wyznaczony przez homomorfizmy modeli tej rodziny. Na całej tej strukturze zdefiniowane jest pojęcie spełnialności. Przy czym, w odróżnieniu od klasycznej spełnialności (w sensie Tarskiego) traktowanej lokalnie, w pojedynczym modelu rozważanej rodziny, spełnialność zdefiniowana na modelu Kripkego jest spełnialnością intuicjonistyczną. Nietrudno jest zauważyć, że model Kripkego wyznaczony przez pojedynczy klasyczny model M z identycznościowym homomorfizmem może być utożsamiony z M widzianym jako model klasyczny. W tym sensie, pojęcie modelu Kripkego można uważać za uogólnienie klasycznego pojęcia modelu pierwszego rzędu. W sposób naturalny powstaje więc kwestia stosownego uogólnienia pojęć i związków klasycznej teorii modeli na przypadek modeli Kripkego. Jedno z podstawowych zagadnień teorii modeli dotyczy elementarnej równoważności. W referacie rozważony zostanie problem elementarnej równoważności w odniesieniu do modeli Kripkego, a w celu jego rozwiązania, wprowadzone zostanie pojęcie bisymulacji dla modeli Kripkego pierwszego rzędu. Pojęcie to jest, z jednej strony, rozszerzenieniem pojęcia bisymulacji dla modeli Kripkego dla intuicjonistycznej logiki zdań oraz, z drugiej strony, uogólnieniem - w opisanym wyżej sensie - pojęcia gry Ehrenfeuchta dla klasycznych modeli pierwszego rzędu. Oprócz omówienia podstawowych własności bisymulacji, zostaną zaprezentowane również jej zastosowania. W szczególności, przedstawiona zostanie konstrukcja elementarnego podmodelu modelu Kripkego.
14.11.2007, Mateusz Kostanek	Tree walking automata cannot be determinized
	Mateusz zreferuje artykul Mikołaja Bojańczyka i Thomasa Colcombeta, który otrzymał tytuł ,,best paper'' na konferencji ICALP 2004. Abstrakt: Tree-walking automata are a natural sequential model for recongnizing languages of finite trees. Such automata walk around the tree and may decide in the end to accept it. It is shown that deterministic tree-walking automata are weaker than nondeterministic tree-walking automata.
07.11.2007, 24.10.2007, Mariusz Łusiak	On learning monotone Boolean functions under the uniform distribution
	We prove two general theorems on monotone Boolean functions which are useful for constructing a learning algorithm for monotone Boolean functions under the uniform distribution. The first result is that a single variable function f(x) = x_i has the minimum correlation with majority function among all fair monotone functions. The second result is on the relationship between the influences and the average sensitivity of a monotone Boolean function. The talk is based on a paper by Kazuyuki Amano and Akira Maruoka.
17.10.2007, Mateusz Juda	Automata for XML - A survey
	Mateusz referuje artykul Thomasa Schwenticka pod tym samym tytułem z Journal of Computer and System Sciences 73(2007), str. 289-315. Abstract artykułu: Automata play an important role for the theoretical foundations of XML data management, but also in tools for various XML processing tasks. This survey article aims to give an overview of fundamental properties of the different kinds of automata used in this area and to relate them to the four key aspects of XML processing: schemas, navigation, querying and transformation.
03.10.2007, Jakub Kozik	Intuitionistic versus Classical Tautologies
	We consider propositional formulas built on implication. The size of a formula is measured by the number of occurrences of variables. We assume that two formulas which differ only in the naming of variables are identical. For every n we investigate the proportion between the number of intuitionistic tautologies of size n compared with the number of classical tautologies of that size. We prove that the limit of that fraction is 1 when n tends to infinity.

webmaster: www-tcs@tcs.uj.edu.pl