Foundations of Computer Science

Theoretical Computer Science
Faculty of Mathematics and Computer Science
Jagiellonian University

Foundations of Computer Science

Computer science foundations Seminar

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

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

23.05.2012, Maciej Bendkowski	On the expressive power of schemes by Dowek G, Jiang Y
	We present a calculus, called the scheme-calculus, that permits to express natural deduction proofs in various theories. Unlike lambda-calculus, the syntax of this calculus sticks closely to the syntax of proofs, in particular, no names are introduced for the hypotheses. We show that despite its non-determinism, some typed scheme-calculi have the same expressivity as the corresponding typed lambda-calculi.
09.05.2012, Piotr Zaborski	APPROXIMATION ALGORITHMS FOR THE EUCLIDEAN TRAVELING SALESMAN PROBLEM WITH DISCRETE AND CONTINUOUS NEIGHBORHOODS by KHALED ELBASSIONI, ALEKSEI V. FISHKIN and RENE SITTERS
	In the Euclidean traveling salesman problem with discrete neighborhoods, we are given a set of points P in the plane and a set of n connected regions (neighborhoods), each containing at least one point of P. We seek to nd a tour of minimum length which visits at least one point in each region. We give (i) an O(\alpha)-approximation algorithm for the case when the regions are disjoint and -fat, with possibly varying size; (ii) an O(\alpha^3)- approximation algorithm for intersecting -fat regions with comparable diameters. These results also apply to the case with continuous neighborhoods, where the sought TSP tour can hit each region at any point. We also give (iii) a simple O(logn)-approximation algorithm for continuous non-fat neighborhoods. The most distinguishing features of these algorithms are their simplicity and low running-time complexities.
25.04.2012, Maciej Gawron	COUNTING d-DIMENSIONAL POLYCUBES AND NONRECTANGULAR PLANAR POLYOMINOES by GADI ALEKSANDROWICZ and GILL BAREQUET
	A planar polyomino of size n is an edge-connected set of n squares on a rectangular two-dimensional lattice. Similarly, a d-dimensional polycube (for d 2) of size n is a connected set of n hypercubes on an orthogonal d-dimensional lattice, where two hypercubes are neighbors if they share a (d-1)-dimensional face. There are also two-dimensional polyominoes that lie on a triangular or hexagonal lattice. In this paper we describe a generalization of Redelmeier's algorithm for counting two-dimensional rectangular polyominoes, which counts all the above types of polyominoes. For example, our program computed the number of distinct three-dimensional polycubes of size 18. To the best of our knowledge, this is the first tabulation of this value.
18.04.2012, Patryk Zaryjewski	Deciding if a Regular Language is Generated by a Splicing System by Lila Kari Steffen Kopecki
	Splicing as a binary word/language operation is inspired by the DNA recombination under the action of restriction enzymes and ligases, and was first introduced by Tom Head in 1987. Shortly after, it was proven that the languages generated by (finite) splicing systems form a proper subclass of the class of regular languages. However, the question of whether or not one can decide if a given regular language is generated by a splicing system remained open. In this paper we give a positive answer to this question. We namely prove that if a language is generated by a splicing system, then it is also generated by a splicing system whose size is a function of the size of the syntactic monoid of the input language, and which can be effectively constructed.
04.04.2012, Michał Feret	Optimal Stopping and Applications 5
	Chapter 6. Maximizing the Rate of Return.
	references: Thomas S. Ferguson, Optimal Stopping and Applications
28.03.2012, Agnieszka Łupińska	Optimal Stopping and Applications 4
	Chapter 5. Monotone Stopping Rule Problems.
	references: Thomas S. Ferguson, Optimal Stopping and Applications
21.03.2012, Szymon Kałasz	Optimal Stopping and Applications 3
	Chapter 3. THE EXISTENCE OF OPTIMAL STOPPING RULES.
	references: Thomas S. Ferguson, Optimal Stopping and Applications
14.03.2012, Paweł Wanat	Optimal Stopping and Applications 2
	Chapter 4. Applications. Markov Models.
	references: Thomas S. Ferguson, Optimal Stopping and Applications
07.03.2012, Jonasz Pamuła	Optimal Stopping and Applications 1
	First chapters of the book Optimal Stopping and Applications, by Thomas S. Ferguson.
29.02.2012, Jakub Kozik	Property B - two coloring of uniform hypergraphs.
	m(n) is defined to be the smallest number for which there exists an n-uniform hypergraph with m(n) edges which is not 2-colorable. Erdos and Lovasz conjectured that m(n) asymptotically behaves like n 2^n. I will present a simple proof of the best known lower bound sqrt(n/log(n)) 2^n, originally derived by Radhakrishnan and Srinivasan in 2000.
18.01.2012, Michał Marczyk	Unification through Projectivity by S. Ghilardi
	We introduce an algebraic approach to E-unification, through the notions of finitely presented and projective object. As applications and examples, we determine the unification type of varieties generated by a single finite quasi-primal algebra, of distributive lattices and of some other equational classes of algebras corresponding to fragments of intuitionistic logic.
11.01.2012, Michał Marczyk	Unification through Projectivity by S. Ghilardi
	We introduce an algebraic approach to E-unification, through the notions of finitely presented and projective object. As applications and examples, we determine the unification type of varieties generated by a single finite quasi-primal algebra, of distributive lattices and of some other equational classes of algebras corresponding to fragments of intuitionistic logic.
04.01.2012, Patryk Zaryjewski	State complexity of power by Michael Domaratzki, Alexander Okhotin
	The number of states in a deterministic finite automaton (DFA) recognizing the language L^k where L is regular language recognized by an n-state DFA, and k>=2 is a constant, is shown to be at most n2^((k-1)n) and at least (n-k)2^((k-1)(n-k)) in the worst case, for every n > k and for every alphabet of at least six letters. Thus, the state complexity of L^k is Θ(n2^((k-1)n)). In the case k=3 the corresponding state complexity function for L^3 is determined as (6n-3)/8 4^n - (n-1)2^n - n with the lower bound witnessed by automata over a four-letter alphabet. The nondeterministic state complexity of L^k is demonstrated to be nk. This bound is shown to be tight over a two letter alphabet.
21.12.2011, Dominik Dudzik	Higher Order Matching and Games by Colin Stirling
	Assume simply typed lambda calculus with base type 0 and the definitions of α-equivalence, β and η-reduction. A matching problem has the form v = u where v,u : A for some type A, and u is closed. The order of the problem is the maximum of the orders of the free variables x1,...,xn in v. A solution of a matching problem is a sequence of terms t1 ,..., tn such that v {t1/x1 ,..., tn/xn} =βη u. We provide a game-theoretic characterisation of higher-order matching. The idea is suggested by model checking games. We then show that some known decidable instances of matching can be uniformly proved decidable via the game-theoretic characterisation.
14.12.2011, Adam Zydroń	Spanning forests on the Sierpinski gasket
	We study the number of spanning forests on the Sierpinski gasket SGd(n) at stage n with dimension d equal to two, three and four, and determine the asymptotic behaviors. The corresponding results on the generalized Sierpinski gasket SGd,b(n) with d = 2 and b = 3; 4 are obtained. We also derive upper bounds for the asymptotic growth constants for both SGd and SG2,b.
07.12.2011, Michał Handzlik	SOME IMPROVEMENTS TO TURNER'S ALGORITHM FOR BRACKET ABSTRACTION by M. Bunder
	A computer handles lambda terms more easily if these are translated into combinatory terms. This translation process is called bracket abstraction. The simplest abstraction algorithm-the (fab) algorithm of Curry (see Curry and Feys [6])-is lengthy to implement and produces combinatory terms that increase rapidly in length as the number of variables to be abstracted increases. A measure of the efficiency of an abstraction algorithm was first introduced by Kennaway as an upper bound of the length of the obtained combinatory term, as a function of the length of the original term and the number of variables to be abstracted. Mulder used these methods and experiments with many special cases, to compare the efficiency of the main algorithms listed above. The algorithm of Statman came out as the most efficient in the limiting case, but showed up as almost the worst in a number of reasonably simple special cases. Turner's algorithm was generally the best in these cases and was in fact Mulder's choice overall. In this paper, firstly we note that what Turner describes as "the improved algorithm of Curry", on which his own is based, is in fact not equivalent to any of Curry's algorithms. Turner's abstracts lack a basic property possessed by all of Curry's as well as many others. Secondly we give methods whereby Turner's algorithm (as well as others) can be more efficiently implemented, while providing simpler abstracts.
30.11.2011, Piotr Wójcik	A note on propositional proof complexity of some Ramsey-type statements by Jan Krajicek
	A Ramsey statement denoted n -> (k, 2, 2) says that every undirected graph on n vertices contains either a clique or an independent set of size k. Any such valid statement can be encoded into valid DNF formula RAM(n, k) of size O(n^k) and with terms of size {k \choose 2}. Let r_k be the minimal n for which statement holds. We prove that RAM(r_k, k) requires expotential size constant depth Frege systems, answering a problem of Krishnamurthy and Moll.
23.11.2011, Jakub Kozik	Optimal stopping for covert expansion.

16.11.2011, Michał Masłowski	Coarse-graining of cellular automata, emergence, and the predictability by Navot Israeli, Nigel Goldenfeld
	Using nearest neighbor, one-dimensional Cellular Automata (CA), we show how to construct local coarse-grained escriptions of CA with different complexity classification. Large-scale behavior can be emulated by them without small-scale details. We show that coarse-grained CA can be decidable even for universal original systems and coarse-graining transformations make a complexity hierarchy of CA rules. Finally we argue that the large scale dynamics of CA can have very small Kolmogorov complexity of the update rules, and moreover exhibits a novel scaling law. This makes finding coarse-grained descriptions of CA easier at coarser scales. We interpret this large scale simplicity as a pattern formation mechanism in which large scale patterns are forced upon the system by the simplicity of the rules that govern the large scale dynamics.
09.11.2011, Marek Wróbel	Complexity of Type Inference by Jerzy Tyszkiewicz
	The type inference problem may be stated as follows: given a term of untyped lambda calculus, decide whether it may be typed to a term of a first-order-typed lambda calculus. If it is possible, then find all possible typings for it (or at least one possible typing). We show that the type inference problem is PTIME-complete.
02.11.2011, Przemysław Jedynak	How common can be universality in cellular automata? by Guillaume Theyssier
	We address the problem of the density of intrinsically universal cellular automata among cellular automata or a subclass of cellular automata. We show that captive cellular automata are almost all intrinsically universal. We show however that intrinsic universality is undecidable for captive cellular automata. Finally, we show that almost all cellular automata have no non-trivial sub-automaton.
26.10.2011, Maciej Bendkowski	On Post correspondence problem for letter monotonic languages by Vesa Halava, Jarkko Kari, Yuri Matiyasevich
	We prove that for given morphisms g, h: { a_1, ..., a_n } \to B^{}, it is decidable whether or not there exists a word w in the regular language a_{1}^{}, ..., a_{n}^{*} such that g(w) = h(w). In other words, we prove that the Post Correspondence Problem is decidable if the solutions are restricted to be from this special language. This yields a nice example of an undecidable problem in integral matrices which cannot be directly proved undecidable using the traditional reduction from the Post Correspondence Problem.
19.10.2011, 12.10.2011, Robery Obryk	Dowodzenie w językach z typami zależnymi
	Celem systemów typów w językach programowania jest ułatwianie wnioskowania o poprawności kodu. Już języki używające systemu typów Hindleya-Milnera pozwalają wnioskować w ciekawy sposób o zachowaniu funkcji na podstawie ich typu. Języki z typami zależnymi pozwalają wyrażać za pomocą typu funkcji praktycznie arbitralne warunki na jej zachowanie. Na tym seminarium poznamy formalizm typów zależnych, sposób przeprowadzania izomorfizmu Curryego-Howarda w nim i przyjrzymy się jak typy zależne pozwalają dowodzić własności programu i pomagają w dowodzeniu własności stopu w języku Agda.
05.10.2011, Robert Obryk	Dowodzenie w językach z typami zależnymi
	Celem systemów typów w językach programowania jest ułatwianie wnioskowania o poprawności kodu. Już języki używające systemu typów Hindleya-Milnera pozwalają wnioskować w ciekawy sposób o zachowaniu funkcji na podstawie ich typu. Języki z typami zależnymi pozwalają wyrażać za pomocą typu funkcji praktycznie arbitralne warunki na jej zachowanie. Na tym seminarium poznamy formalizm typów zależnych, sposób przeprowadzania izomorfizmu Curryego-Howarda w nim i przyjrzymy się jak typy zależne pozwalają dowodzić własności programu i pomagają w dowodzeniu własności stopu w języku Agda. Tematy do nastęnych seminariów: "A Predicative Analysis of Structural Recursion" Abel, Altenkirch "The Size-Change Principle for Program Termination" Lee, Jones, Ben-Amran
01.06.2011, Małgorzata Kruszelnicka	Bisymulation on finite Kripke models
	The notion of bisimulation has been introduced to test whether two processes behave the same. Originally discovered in Computer Science, bisimulation nowadays is employed in many fields. Today it is used in a number of areas of Computer Science such as functional languages, data types, databases, program analysis, to name but a few. Growing interests in this notion led to the discovery of bisimulation in Modal Logic and Set Theory. Finally, the notion was introduced into first-order logic, and found a straightforward game-theoretical interpretation. We present the notion of bisimulation for intuitionistic logic. Our discussion focuses on two cases: the propositional and the first-order case. In both cases we present the theorem which states that bisimulation implies logical equivalence, and consider possible variants of the inverse implication. Further, we present our contribution to the research of the inverse theorem. References: Patterson, A.: \emph{Bisimulation and Propositional Intuitionistic Logic}, Proceedings of the 8th International Conference on Concurrency Theory, Springer-Verlag, 1997 Po{\l}acik, T.: \emph{Back and Forth Between First-Order Kripke Models}, Logic Journal of the IGPL 16 (4), 335--355, 2008 Visser, A.: \emph{Bisimulations, Model Descriptions and Propositional Quantifiers}, Logic Group Preprint Series 161, 1996
25.05.2011, Agnieszka Łupińska	A Universal Approach to Self-Referential Paradoxes, Incompleteness and Fixed Points, by Noson S. Yanofsky
	kontynuacja
	references:
18.05.2011, Agnieszka Łupińska	A Universal Approach to Self-Referential Paradoxes, Incompleteness and Fixed Points, by Noson S. Yanofsky
	Following F. William Lawvere, we show that many self-referential paradoxes, incompleteness theorems and fixed point theorems fall out of the same simple scheme. We demonstrate these similarities by showing how this simple scheme encompasses the semantic paradoxes, and how they arise as diagonal arguments and fixed point theorems in logic, computability theory, complexity theory and formal language theory.
11.05.2011, Robert Obryk	Algorithmic Information Theory 2, by Gregory. J. Chaitin

	references:
04.05.2011, Robert Obryk	Algorithmic Information Theory , by Gregory. J. Chaitin

27.04.2011, 20.04.2011, Marek Wróbel, Adam Zydroń	Mathematics for the Analysis of Algorithms - Asymptotic Analysis

13.04.2011, 06.04.2011, Maciej Bendkowski	Mathematics for the Analysis of Algorithms - Operator Methods

30.03.2011, Michał Masłowski, Tomasz Bińczycki	kontynuacja

23.03.2011, Anna Bień (UŚ)	Klasy grafów singularnych
	We consider simple graphs and their adjacency matrices. In [1] Rara gives graphs with singular adjacency matrix are called singular. In [1] Rara presented tools, which are useful in computing determinant of adjacency matrix of some simple graphs. Rara's methods allow to replace complicated algebraic calculations with operations performed on graphs. In some cases removing sets of edges or vertices does not change or changes the determinant of a graph in a specific way. We continue this subject matter and present general methods of reducing graphs. The most general is the method of identifying $P_3$ paths. Consequences of this theorem are the method of contracting $P_5$ path and a method which can be applied to graphs circumscribed on cycles. We apply these methods in computing determinant of adjacency matrix of certain classes of graphs. In particular we present a recursive formula for planar grids $P_n \times P_{n+1}$ $$det A(P_n \times P_{n+1})= (-1)^{(n+1)/2}$$ which is a main step in solution of the singularity problem for all planar grids. [1] H.M. Rara, Reduction procedures for calculating the determinant of the adjacency matrix of some graphs and the singularity of square planar grids, Discrete Mathematics 151, 213-219, Elsevier, 1996.
16.03.2011, 09.03.2011, Michał Masłowski	Mathematics for the Analysis of Algorithms - Recurrence Relations

02.03.2011, Tomasz Bińczycki	Mathematics for the Analysis of Algorithms - Binomial Identities

19.01.2011, Przemek Jedynak	Synthetic Differential Geometry - Chicago's pizza seminar notes.

12.01.2011, Tomasz Krakowiak	Complexity of Type Inference, paper by Jurek Tyszkiewicz
	The main result is the proof of PTIME-completeness of the type reconstruction problem for simply typed lambda calculus.
05.01.2011, Patryk Zaryjewski	Interaction properties of relational periods, paper by Vesa Halava and Tero Harju and Tomi K¨arkiy
	We consider relational periods where the relation is a compatibility relation on words induced by a relation on letters. We introduce three types of periods, namely global, external and local relational periods, and we compare their properties by proving variants of the theorem of Fine and Wilf for these periods.
15.12.2010, Jacek Bąkowski	On systems of word equations ..., paper by Elena Czeizler, and Wojciech Plandowski
	In this paper, we investigate the open question, formulated in 1983 by Culik II and Karhumäki, asking whether there exist independent systems of three word equations over three unknowns admitting non-periodic solutions. In particular, we answer negatively the above mentioned question for systems in which one of the unknowns occurs at most six times. That is, we show that such systems admit only periodic solutions or they are not independent.
08.12.2010, Hannes Diener (Univ. of Siegen, Germany)	Variations on a theme by Ishihara
	This will be a talk in two halves. The first will consist of a gentle introduction to the area of constructive analysis, especially focussing on continuity and completeness. In constructive mathematics one is interested in objects that one cannot only rule out the non-existence of, but those that one can (at least in theory) actually construct. This part of the talk should be accessible to anyone with a knowledge of basic analysis - no knowledge about constructivism is required. In the second half we will present results by Hajime Ishihara of 1991, which became known as ``Ishihara's tricks''. In these results decisions that, on first and maybe even second glance, seem algorithmically impossible are made. We will present new results, which extend Ishihara's ideas to a more general setting. Lastly, we will show how all of this can be used to give an axiomatic, concise, and clear proof of the well known phenomenon that in many constructive settings every real-valued function on the unit interval is continuos (``computability implies continuity'').
01.12.2010, Paweł Błasiak (IFJ -Kraków)	Combinatorial Models of Creation-Annihilation
	Quantum physics has revealed many interesting formal properties associated with the algebra of two operators, A and B, satisfying the partial commutation relation AB-BA=1. We surveys the relationships between classical combinatorial structures and the reduction to normal form of operator polynomials in such an algebra. The connection is achieved through suitable graphs, or ''diagrams'', that are composed of elementary ''gates''. In this way, many normal form evaluations can be systematically obtained, thanks to models that involve set partitions, permutations, increasing trees, etc. Reference: P. Blasiak and Ph. Flajolet "Combinatorial Models of Creation-Annihilation" arXiv:1010.0354 [math.CO]
24.11.2010, Michał Handzlik	Pseudotopological spaces and the Stone-Cech compactification.
	Our slogan is "topology is about convergence". The fact that so many aspects of topology can be captured by convergence naturally makes us wonder whether convergence could be taken to be more fundamental than open sets. It leads to the definition od pseudotopological space, where we focus on convergence properties only, without mentioning open sets. We present how Stone-Cech compactification translates into pseudotopological spaces.
17.11.2010, Jonasz Pamuła	Algorithms for learning regular expressions from positive data, paper by Henning Fernau
	We describe algorithms that directly infer very simple forms of 1-unambiguous regular expressions from positive data. Thus, we characterize the regular language classes that can be learned this way, both in terms of regular expressions and in terms of (not necessarily minimal) deterministic finite automata.
10.11.2010, Ola Piktus	Topology on words, paper by Cristian S. Calude, Helmut Jürgensen, Ludwig Staiger
	We investigate properties of topologies on sets of finite and infinite words over a finite alphabet. The guiding example is the topology generated by the prefix relation on the set of finite words, considered as a partial order. This partial order extends naturally to the set of infinite words; hence it generates a topology on the union of the sets of finite and infinite words. We consider several partial orders which have similar properties and identify general principles according to which the transition from finite to infinite words is natural. We provide a uniform topological framework for the set of finite and infinite words to handle limits in a general fashion.
03.11.2010, 27.10.2010, Kasia Grygiel	Asymptotically almost all lambda terms are strongly normalizing
	We present quantitative analysis of various (syntactic and behavioral) properties of random lambda terms. Our main results are that asymptotically all the terms are strongly normalizing and that any fixed closed term almost never appears in a random term. Surprisingly, in combinatory logic (the translation of the lambda calculus into combinators), the result is exactly opposite. We show that almost all terms are not strongly normalizing. This is due to the fact that any fixed combinator almost always appears in a random combinator.
20.10.2010, Piotr Faliszewski (AGH)	A 2-Approximation Algorithm for a Candidate Promotion Problem
	We are given an election E=(C,V), where C is a set of alternatives, and V is a collection of voters, and a preferred alternative p. Each voter is represented by a linear order over C. As part of a political campaign, we have the ability (at some cost) to shift p forward in some of the votes. In the shift-bribery problem we ask for the minimal cost of shifts that ensure our candidate's victory. We show that this problem is NP-complete (for Borda winner determination rule; an example of so-called scoring rules) and give a 2-approximation algortihm that works for all scoring rules, even if the votes are weighted.
13.10.2010, Kuba Kozik	Recent progress in best-choice problems for posets.

02.06.2010, Jan Hązła	Denotational semantics of T

26.05.2010, Maria Chmaj	Coherent Spaces

21.04.2010, Karol Kosiński	Sequent calculus, chapter 5 of Girard's book.

14.04.2010, Rafał Pajdzik	The Normalization Theorem, Chapter 4 of Girard's book.

07.04.2010, Leszek Horwath (Cedric)	Curry Howard Isomorphism. Chapter 3 of Girard's book.

24.03.2010, 10.03.2010, Szymon Borak	Fixed point theory for programs

28.01.2010, ZAJĘCIA W NOWYM SEMESTRZE	PROOFS AND TYPES
	Link do książki Girarda pt. Proofs and Types. List of chapter titles: 1. Sense, Denotation and Semantics 2. Natural Deduction 3. The Curry-Howard Isomorphism 4. The Normalisation Theorem 5. Sequent Calculus 6. Strong Normalisation Theorem 7. Gödel's system T 8. Coherence Spaces 9. Denotational Semantics of T 10. Sums in Natural Deduction 11. System F 12. Coherence Semantics of the Sum 13. Cut Elimination (Hauptsatz) 14. Strong Normalisation for F 15. Representation Theorem Appendices: A. Semantics of System F - by Paul Taylor B. What is Linear Logic? - by Yves Lafont
27.01.2010, Marek Wróbel	Program Analysis
	Ostatnia część książki Changa and Lee o dowodzeniu twierdzeń.
20.01.2010, Michał Handzlik	Procedury dowodowe oparte na twierdzeniu Herbranda
	Rozdział 9. książki Changa i Lee o automatycznym dowodzeniu twierdzeń.
06.01.2010, Maria Chmaj	Równość
	Rozdział 8. książki Changa i Lee o automatycznym dowodzeniu twierdzeń.
16.12.2009, Jan Hązła	Linear Resolution in FOL
	Rozdział 7. książki Changa & Lee.
02.12.2009, Adam Zydro	Semantic Resolution
	Rozdział 6. ksiązki Changa & Lee.
25.11.2009, Piotr Faliszewski	Distance Rationalizability of Voting Rules
	A voting rule is an algorithm for determining the winner in an election. One can easily come up with many different voting rules, but it is also important to justify why a given rule is natural/useful. There are several approaches that have been used to justify the proposed rules. One justification is to show that a rule satisfies a set of desirable axioms that uniquely identify it. Another is to show that the calculation that it performs is actually maximum likelihood estimation relative to a certain model of noise that affects voters (MLE approach). The third approach, which has been recently actively investigated, is the so-called distance rationalizability framework. In it, a voting rule is defined via a class of consensus elections (i.e., a class of elections that have a clear winner) and a distance function. A candidate c is a winner of an election E if c wins in one of the consensus elections that are closest to E relative to the given distance. In this talk, we show that essentially any voting rule is distance-rationalizable if we do not restrict the two ingredients of the rule: the consensus class and the distance. Thus distance rationalizability of a rule does not by itself guarantee that the voting rule has any desirable properties. However, we demonstrate that the distance used to rationalize a given rule may provide useful information about this rule's behavior. Specifically, we identify a large class of distances, which we call votewise distances, and show that if a rule is rationalized via a distance from this class, many important properties of this rule can be easily expressed in terms of the underlying distance. This enables us to provide a new characterization of scoring rules and to establish a connection with the MLE framework. We also give bounds on the computational complexity of the winner determination problem for distance-rationalizable rules.
18.11.2009, Sylwia Antoniuk	Rezolucja
	Rezolucja jako rewolucja, w relacji do rewelacji.
04.11.2009, Rafał Pajdzik, UJ	FOL
	Chapters 3,4 on First Order Logic from `Symbolic Logic and Mechanical Theorem Proving' by Chin-Liang Chang and Richard Char-Thung Lee.
28.10.2009, Marek Zaionc	Schwichtenberg style lambda definability is undecidable

21.10.2009, Mareusz Drewienkowski, UJ	Gry w wielomiany (Playing polynomials)
	We will hear about the process of reconstruction of polynomials from the finite number of examples. The talk is based on the 1997 paper by J. Małolepszy, M. Moczurad and M. Zaionc entitled "Schwichtenberg style lambda definability is undecidable" published in Lecture Notes in Computer Science 1210, pp. 267-283.
14.10.2009, Marek Zaionc	Two open problems on lambda definability
	We discus two open lambda definability problems. 1. It can be shown that any lambda definable operation on numbers can be synthesize from the finite number of examples. We will discuss the same problem for lambda definable word operations. 2. We address the problem of lambda definable tree operations. Is it true that the set of all lambda definable tree operations is NOT finitely generated.
03.06.2009, Jakub Kozik	Drzewa and/or - przegląd problemów

27.05.2009, Paweł Waszkiewicz	T^omega as a universal domain
	Following G. Plotkin [T^omega as a universal domain, J. of Comp. and System Sci. 17, 1978] We introduce a domain T^omega and a language LAMBDA, and show that LAMBDA-definability coincide with computability. Furthermore, we show that T^omega is universal, in the sense that every bounded-complete dcpo embeds in it. Finally, we demonstrate that every second-countable T_0 space topologically embeds in T^omega as an isochordal subspace.
13.05.2009, Wojciech Czarnecki	The Curry-Howard Isomorphism

06.05.2009, 29.04.2009, Michał Klasiński	Wśród typów nie ma arystokracji

22.04.2009, 15.04.2009, Sylwia Antoniuk	Basic Simple Type Theory

08.04.2009, 01.04.2009, Michał Handzlik	Higher-order Unificatrion and Matching

25.03.2009, 11.03.2009, Paweł Waszkiewicz	A Lazy Introduction to Goedel's Theorems
	See http://www.logicmatters.net/ for more info.
21.01.2009, Mateusz Kostanek	Regular Languages and Stone Duality
	We give a new account of the relationships among varieties of regular languages, varieties of finite semigroups, and their characterization in terms of "implicit identities." Our development, which is essentially topological in character, is based on the duality (established by Stone) between Boolean algebras and certain topological spaces (which are now called "Stone spaces"). This duality does not seem to have been recognized in the literature on regular languages, even though it is well known that the regular languages over a fixed alphabet form a Boolean algebra and that the "implicit operations" with a fixed number of operands form a Stone space. Na podstawie artykulu: N. Pippenger, Regular Languages and Stone Duality, Theory Comput. Systems30, 121-134 (1997).
07.01.2009, Michał Pokrywka	Algorytmy kolejkowania danych w sieciach komputerowych
	cd z poprzedniego roku.
17.12.2008, Michał Pokrywka	Algorytmy kolejkowania danych w sieciach komputerowych
	Przedstawię dwie publikacje godne uwagi opisujące modele matematyczne dwóch rozwiązań. Jedna dotyczy algorytmu RED (Random Early Detection) a druga HFSC (Hierarchical Fair Service Curve). Algorytm RED pozwala w sieciach wysokich prędkości na zapobieganie zdominowaniu pasma przez jeden strumień danych za pomocą losowego odrzucania pakietów (z prawdopodobieństwem ważonym). Algorytm HFSC pozwala dla kolejki danych zdefiniować parametry ,,krzywych usług'' (ang. service curves) do dynamicznego sprawiedliwego podziału pasma, zachowując parametry strumieni real-time.
29.10.2008, Mateusz Drewienkowski	Dualność Stone'a - cz.2.

22.10.2008, Mateusz Drewienkowski	Dualność Stone'a - cz.1.

15.10.2008, Jarosław Duda	Asymmetric numeral systems
	We will speak about new approaches to entropy encoding. We present various generalizations of standard numeral systems which are optimal for encoding sequences of equiprobable symbols as asymmetric numeral systems - optimal for freely chosen probability distributions of symbols. It has some similarities to Range Coding but instead of encoding a symbol in choosing a range, we spread these ranges uniformly over whole interval. This leads to a simpler en- coder - instead of using two states to define range, we need only one. This approach is truly universal - we can get from extremely precise encoding (ABS) to extremely fast with possibility to additionally encrypt the data (ANS). This encryption uses a key to initialize a random number generator, which is used to calculate the coding tables. Such preinitialized encryption has an additional advantage: it's resistant to brute force attack - in order to check a key we have to make the whole initialization. We will also show that using ANS we can get an error correction method which is resistant to pessimistic cases.
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: email = a@b, a=www-tcs, b=tcs.uj.edu.pl