Theoretical Computer Science flagPL flagEN
Faculty of Mathematics and Computer Science
Jagiellonian University
    informatyka analityczna  
UJ coat of arms
Foundations of Computer Science
Computer science foundations Seminar
Wednesday: 12:15 - 14:00, room 0174
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
Grzegorz Świrski
Near semi-rings and lambda calculus by Rick Statman
A connection between lambda calculus and the algebra of near semi-rings is discussed. Among the results is the following completeness theorem. A first-order equation in the language of binary associative distributive algebras is true in all such algebras if and only if the interpretations of the first order terms as lambda terms beta-eta convert to one another. A similar result holds for equations containing free variables.  
Radosław Smyrek
Best Response Analysis in Two Person Quantum Games by Azharuddin Shaik, Aden Ahmed
In this paper, we find particular use for a maximally entangled initial state that produces a quantized version of two player two strategy games. When applied to a variant of the well-known game of Chicken, our construction shows the existence of new Nash equilibria with the players receiving better payoffs than those found in literature.  
Bartłomiej Ryniec
In this paper we study generic complexity of undecidable problems. It turns out that some classical undecidable problems are, in fact, strongly undecidable, i.e., they are undecidable on every strongly generic subset of inputs. For instance, the classical Halting Problem is strongly undecidable. Moreover, we prove an analog of the Rice’s theorem for strongly undecidable problems, which provides plenty of examples of strongly undecidable problems. Then we show that there are natural super-undecidable problems, i.e., problem which are undecidable on every generic (not only strongly generic) subset of inputs. In particular, there are finitely presented semigroups with super-undecidable word problem. To construct strongly- and super-undecidable problems we introduce a method of generic amplification (an analog of the amplification in complexity theory). Finally, we construct absolutely undecidable problems, which stay undecidable on every non-negligible set of inputs. Their construction rests on generic immune sets.  
Bartosz Badura
Havannah and TwixT are pspace-complete by Édouard Bonnet, Florian Jamain, and Abdallah Saffidine
Numerous popular abstract strategy games ranging from hex and havannah to lines of action belong to the class of connection games. Still, very few complexity results on such games have been obtained since hex was proved pspace-complete in the early eighties. We study the complexity of two connection games among the most widely played. Namely, we prove that havannah and twixt are pspacecomplete. The proof for havannah involves a reduction from generalized geography and is based solely on ring-threats to represent the input graph. On the other hand, the reduction for twixt builds up on previous work as it is a straightforward encoding of hex.  

  • 06.05.2015,
    Leszek Jakub Kania
    Fast algorithm finding the shortest reset words by A. Kisielewicz J. Kowalski, and M. Szykuła
    In this paper we present a new fast algorithm finding minimal reset words for finite synchronizing automata. The problem is know to be computationally hard, and our algorithm is exponential. Yet, it is faster than the algorithms used so far and it works well in practice. The main idea is to use a bidirectional BFS and radix (Patricia) tries to store and compare resulted subsets. We give both theoretical and practical arguments showing that the branching factor is reduced efficiently. As a practical test we perform an experimental study of the length of the shortest reset word for random automata with n states and 2 input letters. We follow Skvorsov and Tipikin, who have performed such a study using a SAT solver and considering automata up to n = 100 states. With our algorithm we are able to consider much larger sample of automata with up to n = 300 states. In particular, we obtain a new more precise estimation of the expected length of the shortest reset word = 2.5 sqrt{n − 5}.  
    Marcin Kostrzewa
    A Short Note on Type-inhabitation: Formula-Trees vs. Game Semantics by S. Alves, S. Broda
    This short note compares two different methods for exploring type-inhabitation in the simply typed lambda-calculus, highlighting their similarities.  
    Agnieszka Łupińska
    The Converse principal Type Algorithm by Roger Hindley
    One chapter from the book Basic Simple Type Theory  
    Agnieszka Łupińska
    The principal Type Algorithm by Roger Hindley
    One chapter from the book Basic Simple Type Theory  
    Maciej Bendkowski
    Über Tautologien, in welchen keine Variable mehr als zweimal vorkommt von S. Jaśkowski
    Agnieszka Łupińska
    The principal Type Algorithm by Roger Hindley
    One chapter from the book Basic Simple Type Theory  
    Maciej Bendkowski
    Über Tautologien, in welchen keine Variable mehr als zweimal vorkommt von S. Jaśkowski
    H. Thiele hat im Jahre 1960 das Problem gestellt, das implikative Teilsystem des Aussagenkalküls mit dem Axiomen B,C,K zu untersuchen. Hier wird für dieses System und für ein anderes, in dem das letzte Axiom durch ein schwächeres, nämlich I ersetzt wird, ein Entscheidungsverfahren angegeben. Die Methode beruht auf einer Untersuchung von gewissen allgemeinen Eigenschaften der Ausdrücke, in welchen keine Satzvariable mehr als zweimal vorkommt. Dabei wird eine dreiwertige Matrix benutzt.  
    Radosław Smyrek
    Symmetry groups of boolean functions by Mariusz Grech, Andrzej Kisielewicz
    We prove that every abelian permutation group, but known exceptions, is the symmetry group of a boolean function. This solves the problem posed in the book by Clote and Kranakis. In fact, our result is proved for a larger class of permutation groups, namely, for all subgroups of direct sums of regular permutation groups.  
    Bartłomiej Ryniec
    Infinite time Turing machines with only one tape by Joel David Hamkins, Daniel Evan Seabold
    Infinite time Turing machines with only one tape are in many respects fully as powerful as their multi-tape cousins. In particular, the two models of machine give rise to the same class of decidable sets, the same degree structure and, at least for functions f:R → N, the same class of computable functions. Nevertheless, there are infinite time computable functions f:R→R that are not one-tape computable, and so the two models of infinitary computation are not equivalent. Surprisingly, the class of one-tape computable functions is not closed under composition; but closing it under composition yields the full class of all infinite time computable functions. Finally, every ordinal which is clockable by an infinite time Turing machine is clockable by a one-tape machine, except certain isolated ordinals that end gaps in the clockable ordinale  
    Michał Seweryn
    A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions by Chunhan Wu, Xingyuan Zhang, Christian Urban
    There are numerous textbooks on regular languages. Many of them focus on finite automata for proving properties. Unfortunately, automata are not so straightforward to formalise in theorem provers. The reason is that natural representations for automata are graphs, matrices or functions, none of which are inductive datatypes. Regular expressions can be defined straightforwardly as a datatype and a corresponding reasoning infrastructure comes for free in theorem provers. We show in this paper that a central result from formal language theory—the Myhill-Nerode Theorem—can be recreated using only regular expressions. From this theorem many closure properties of regular languages follow.  
    Agnieszka Łupińska
    Relevant Logic and the Philosophy of Mathematics by Edwin Mares
    This paper sets out three programmes that attempt to use relevant logic as the basis for a philosophy of mathematics. Although these three programmes do not exhaust the possible approaches to mathematics through relevant logic, they are fairly representative of the current state of the field. The three programmes are compared and their relative strengths and weaknesses set out. At the end of the paper I examine the consequences of adopting each programme for the realist debate about mathematical objects.  

  • 10.12.2014,
    Pierre Lescanne (l'École Normale Supérieure de Lyon)
    Boltzmann samplers
    Agnieszka Łupińska
    General information in relevant logic by Edwin D. Mares
    There are numerous textbooks on regular languages. Many of them focus on finite automata for proving properties. Unfortunately, automata are not so straightforward to formalise in theorem provers. The reason is that natural representations for automata are graphs, matrices or functions, none of which are inductive datatypes. Regular expressions can be defined straightforwardly as a datatype and a corresponding reasoning infrastructure comes for free in theorem provers. We show in this paper that a central result from formal language theory—the Myhill-Nerode Theorem—can be recreated using only regular expressions. From this theorem many closure properties of regular languages follow.  
    Konrad Witaszczyk
    Problems of Proof compexity by Jan Krajicek, Stephen A. Cook and Robert A. Reckhow
    The ultimate goal of proof complexity is to show that there is no universal propositional proof system allowing for efficient proofs of all tautologies. This is equivalent to showing that the computational complexity class NP is not closed under the complementation. By the universality propositional proof systems subsume methods from other parts of mathematics used for proving the non-existence statements. Because of this, even the partial results known at present (lower bounds for some specific proof systems) revealed interesting links of proof complexity to logic, algebra, combinatorics, computational complexity. We will explain some basic points of proof complexity and give few informal examples in order to motivate the main concepts and problems of proof complexity.  
    Bartosz Badura
    On the Complexity of Trick-Taking Card Games by Edouard Bonnet, Florian Jamain, and Abdallah Saffidine
    Determining the complexity of perfect information trick-taking card games is a long standing open problem. This question is worth addressing not only because of the popularity of these games among human players, e.g., DOUBLE DUMMY BRIDGE, but also because of its practical importance as a building block in state-of-the-art playing engines for CONTRACT BRIDGE, SKAT, HEARTS, and SPADES. We define a general class of perfect information twoplayer trick-taking card games dealing with arbitrary numbers of hands, suits, and suit lengths. We investigate the complexity of determining the winner in various fragments of this game class. Our main result is a proof of PSPACE-completeness for a fragment with bounded number of hands, through a reduction from Generalized Geography. Combining our results with W¨astlund’s tractability results gives further insight in the complexity landscape of trick-taking card games.  
    Bartłomiej Ryniec
    Social Networks with Competing Products by Krzysztof Apt and Evangelos Markakis
    We introduce a new threshold model of social networks, in which the nodes influenced by their neighbours can adopt one out of several alternatives. We characterize social networks for which adoption of a product by the whole network is possible (respectively necessary) and the ones for which a unique outcome is guaranteed. These characterizations directly yield polynomial time algorithms that allow us to determine whether a given social network satisfies one of the above properties. We also study algorithmic questions for networks without unique outcomes. We show that the problem of determining whether a final network exists in which all nodes adopted some product is NP-complete. In turn, we also resolve the complexity of the problems of determining whether a given node adopts some (respectively, a given) product in some (respectively, all) network(s). Further, we show that the problem of computing the minimum possible spread of a product is NP-hard to approximate with an approximation ratio better than W(n), in contrast to the maximum spread, which is efficiently computable. Finally, we clarify that some of the above problems can be solved in polynomial time when there are only two products.  
    Maciej Bendkowski
    We describe the basic theory of infinite time Turing machines and some recent developments, including the infinite time degree theory, infinite time complexity theory, and infinite time computable model theory. We focus particularly on the application of infinite time Turing machines to the analysis of the hierarchy of equivalence relations on the reals, in analogy with the theory arising from Borel reducibility. We define a notion of infinite time reducibility, which lifts much of the Borel theory into the class $Delta^1_2$ in a satisfying way.  
    Łukasz Lachowski
    Typed combinatory logic by Henk Barendregt
    Basic properties of typed combinatory logic  
    Łukasz Lachowski
    Combinatrory Logic by Henk Barendregt
    Basic properties of combinatory logic  
    Łukasz Lachowski
    Combinatrory Logic by Henk Barendregt
    Basic properties of combinatory logic  
    Gabriel Fortin
    "The safe lambda calculus" by William Blum and C.-H. Luke Ong.
    Safety is a syntactic condition of higher-order grammars that constrains occurrences of variables in the production rules according to their type-theoretic order. In this paper, we introduce the safe lambda calculus, which is obtained by transposing (and generalizing) the safety condition to the setting of the simply-typed lambda calculus. In contrast to the original definition of safety, our calculus does not constrain types (to be homogeneous). We show that in the safe lambda calculus, there is no need to rename bound variables when performing substitution, as variable capture is guaranteed not to happen. We also propose an adequate notion of β-reduction that preserves safety. In the same vein as Schwichtenberg’s 1976 characterization of the simply-typed lambda calculus, we show that the numeric functions representable in the safe lambda calculus are exactly the multivariate polynomials; thus conditional is not definable. We also give a characterization of representable word functions. We then study the complexity of deciding beta-eta equality of two safe simply-typed terms and show that this problem is PSPACE-hard. Finally we give a game-semantic analysis of safety: We show that safe terms are denoted by P-incrementally justified strategies. Consequently pointers in the game semantics of safe λ-terms are only necessary from order 4 onwards.  
    Maciej Bendkowski
    On the shortest combinatory logic term without weak normalisation.
    Combinatory logic is a formal notation for function abstraction, eliminating the notion of bound variables. In our presentation, we give proofs of non-normalization for two different S-terms, i.e. combinatory logic terms consisting of only one combinator S and term application, and present a computer-assisted proof of the least combinatory logic term without normal form. We will then discuss the decidability of normalization in the set of S-terms.  
    Radosław Smyrek
    A hierarchy of hereditarily finite sets by Laurence Kirby
    This article defines a hierarchy on the hereditarily finite sets which reflects the way sets are built up from the empty set by repeated adjunction, the addition to an already existing set of a single new element drawn from the already existing sets. The structure of the lowest levels of this hierarchy is examined, and some results are obtained about the cardinalities of levels of the hierarchy.  
    Konrad Witaszczyk
    On the classification of recursive languages by John Case, Efim Kinber, Arun Sharma, and Frank Stephanc.
    A one-sided classifier for a given class of languages converges to 1 on every language from the class and outputs 0 infinitely often on languages outside the class. A two-sided classifier, on the other hand, converges to 1 on languages from the class and converges to 0 on languages outside the class. The present paper investigates one-sided and two-sided classification for classes of recursive languages. Theorems are presented that help assess the classifiability of natural classes. The relationships of classification to inductive learning theory and to structural complexity theory in terms of Turing degrees are studied. Furthermore, the special case of classification from only positive data is also investigated.  
    Patryk Zaryjewski
    The partial derivative automaton is usually smaller than other nondeterministic finite automata constructed from a regular expression, and it can be seen as a quotient of the Glushkov automaton. By estimating the number of regular expressions that have \epsilon as a partial derivative, we compute a lower bound of the average number of mergings of states in A_pos and describe its asymptotic behaviour. This depends on the alphabet size, k, and for growing k’s its limit approaches half the number of states in Apos. The lower bound corresponds to consider the A_pd automaton for the marked version of the regular expression, i.e. where all its letters are made different. Experimental results suggest that the average number of states of this automaton, and of the A_pd automaton for the unmarked regular expression, are very close to each other.  
    Maciej Gawron
    Constructions of asymptotically shortest k-radius sequences by Jaromczyk, Zbigniew Lonc, Mirosław Truszczynski
    Let k be a positive integer. A sequence s over an n-element alphabet A is called a k-radius sequence if every two symbols from A occur in s at distance of at most k. Let f_k(n) denote the length of a shortest k-radius sequence over A. We provide constructions demonstrating that (1) for every fixed k and for every fixed ε > 0, f_k(n) = 1 / 2k n^2 + O(n^{1+ε}) and (2) for every k = n^α, where α is a fixed real such that 0 < α < 1, f_k(n) = 1/2k n^2 + O(n^β ), for some β < 2 − α. Since fk(n)  1/2k n^2 − n/2k , the constructions give asymptotically optimal k-radius sequences. Finally, (3) we construct optimal 2-radius sequences for a 2p-element alphabet, where p is a prime.  
    Bartłomiej Ryniec
    Multiparty communication complexity and very hard functions by Pavol Duriš
    A boolean function f(x_1, . . . , x_n) with x_i ∈ {0, 1}^m for each i is hard if its nondeterministic multiparty communication complexity (introduced in [in: Proceedings of the 30th IEEE FOCS, 1989, p. 428–433]), C(f), is at least nm. Note that C(f)  n*m for each f(x_1, . . . , x_n) with x_i ∈ {0, 1}^m for each i. A boolean function is very hard if it is hard and its complementary function is also hard. In this paper, we show that randomly chosen boolean function f(x_1, . . . , x_n) with x_i ∈ {0, 1}^m for each i is very hard with very high probability (for n  3 and m large enough). In [in: Proceedings of the 12th Symposium on Theoretical Aspects of Computer Science, LNCS 900, 1995, p. 350–360], it has been shown that if f(x_1, . . . , x_k , . . . , x_n) = f_1 (x_1, . . . , x_k ) · f_2(x_{k+1}, . . . , x_n), where C(f_1) > 0 and C(f_2) > 0, then C(f) = C(f1) + C(f2).We prove here an analogical result: If f(x_1, . . . , x_k , . . . , x_n) = f_1(x_1, . . . , x_k ) ⊕ f_2(x_{k+1}, . . . , x_n) then DC(f) = DC(f1) + DC(f2), where DC(g) denotes the deterministic multiparty communication complexity of the function g and “⊕” denotes the parity function.  
    Maciej Gazda Eindhoven University of Technology
    Zielonka's Recursive Algorithm for Parity Games
    Parity games are infinite duration, two player games played on a finite directed graph. Vertices of the graph are labelled with natural numbers (called priorities) and the winning condition is determined by the parity of the most significant (typically maximal) priority encountered inifnitely often. The games are memoryless determined, moreover, the problem of finding the winning partition of a given game belongs to both NP and coNP complexity classes. On the other hand, no polynomial algorithm solving parity games has been found (the best one due to Jurdziński, Paterson and Zwick has subexponential running time with sqrt(n) in the exponent). In my talk, I will give a brief introduction to this intriguing computational problem, and then focus on one of the earliest and simplest solving algorithms, namely Zielonka's recursive algorithm. Even though its worst-case running time is not particularly impressive as compared to more sophisticated solvers, the experimental study of Friedmann and Lange has shown that in practice it works very well. In order to understand why it is the case, in our recent work with Tim Willemse we have analysed the performance of two variants of the algorithm (standard and optimised) on certain subclasses of parity games (dull, weak, and solitaire). Moreover, we have provided a tighter lower bound on its worst-case running time.  
    Agnieszka Łupińska
    Efficient Bracket Abstraction Using Iconic Representations for Combinators by Antoni Diller
    Some fundamental properties of a new uni-variate bracket abstraction algorithm employing a string representation for combinators are established. In particular, if the input term has length n, where n > 1, the algorithm is called fewer than n times to produce the abstract. Furthermore, the space required to store the abstract, in the worst case, is of the order O(n). This algorithm also has a number of features that make it worthy of further attention. When it is used to abstract a variables from an input term of length n, where n > 1, fewer than an new combinators are introduced into the abstract. However, the total size of the string representations of these combinators grows quadratically in the number of variables abstracted and the space required to store the abstract, in the worst case, is of the order O(a^2 n). Fortunately, a closely related single-sweep, multi-variate algorithm exists, using an array representation for combinators, which produces an abstract whose storage requirement, in the worst case, is of the order O(an).  
    Aleksandra Piktus
    Improved constructions of quantum automata by Andris Ambainis, Nikolajs Nahimovs
    We present a simple construction of quantum automata which achieve an exponential advantage over classical finite automata. Our automata use 4/epsion log (2p) states to recognize a language that requires p states classically. The construction is both substantially simpler and achieves a better constant in the front of log p than the previously known construction. Our construction is by a probabilistic argument. We consider the possibility to derandomize it and present some results in this direction.  
    Łukasz Janiszewski
    Exploiting independent subformulas: A faster approximation scheme for #k-SAT by Manuel Schmitt , Rolf Wanka
    We present an improvement on Thurley’s recent randomized approximation scheme for #k-SAT where the task is to count the number of satisfying truth assignments of a Boolean function Φ given as an n-variable k-CNF. We introduce a novel way to identify independent substructures of Φ and can therefore reduce the size of the search space considerably. Our randomized algorithm works for any k. For #3-SAT, it runs in time O(ε−2 · 1.51426n), for #4-SAT, it runs in time O(ε−2 · 1.60816n), with error bound ε.  
    Michał Marczyk
    CAP theorem
    We will examine Gilbert and Lynch's proof of Brewer's conjecture. The latter states that it is impossible for a distributed service to be simultaneously consistent, available and partition-tolerant (for certain natural definitions of these terms). We will then consider the real-world impact of the theorem. Based on Gilbert, Lynch, "Brewer's Conjecture and the Feasibility of Consistent, Available, Partition-Tolerant Web Services".  
    Seminar cancelled
    Robert Obryk
    Cryptographic Accumulators
    A cryptographic accumulator is a less well-known cousin of a cryptographic hash function: it allows a digest of a multiset to be constructed one element at a time. One can also extend this notion in a few ways: allow removing elements already added to the digest, or provide witnesses that prove validity of operations on the digest without giving away what operations they were. This talk will present the basic notion of accumulators and their properties, give example implementations (secure under the typical assumptions) and hint at their possible uses.  
    Adam Polak
    Open problems for pattern languages
    A pattern is a string built of terminals and variables. A language generated by a given pattern consists of words produced by substituting variables with arbitrary strings of terminals. Of course every occurrence of the same variable has to be substituted with the same string. Pattern languages were first studied in the context of machine learning but soon attracted formal languages researchers. Despite their very simple definition they have numerous interesting properties. During the seminar we will discuss several intriguing computational and structural problems involving pattern languages and their relation to the Chomsky hierarchy. Some of them were recently solved and some remain open.

    Papers about pattern languages:  

    Maciej Bendkowski
    An upper bound for reduction sequences in the typed lambda-calculus by H. Schwichtenberg
    It is well known that the full reduction tree for any term of the typed λ–calculus is finite. However, it is not obvious how a reasonable estimate for its height might be obtained. Here we note that the head reduction tree has the property tha the number of its nodes with conversions bounds the length of any reduction sequence. The height of that tree, and hence also the number of its nodes, can be estimated using a technique due to Howard [3], which in turn is based on work of Sanchis [4] and Diller [1]. This gives the desired upper bound. The method of Gandy [2] can also be used to obtain a bound for the length of arbitrary reduction sequences; this is carried out in [5]. However, the bound derived here, apart from being more intelligible, is also better.  
    Konrad Witaszczyk
    Analytic aspects of the shuffle product by Marni Mishna, Mike Zabrocki
    There exist very lucid explanations of the combinatorial origins of rational and algebraic functions, in particular with respect to regular and context free languages. In the search to understand how to extend these natural correspondences, we find that the shuffle product models many key aspects of D-finite generating functions, a class which contains algebraic. We consider several different takes on the shuffle product, shuffle closure, and shuffle grammars, and give explicit generating function consequences. In the process, we define a grammar class that models D-finite generating functions.  
    Michał Bejda
    Generalized satisfability problems: minimal elements and phase transitions by Nadia Creignoua, Herve Daud
    We develop a probabilistic model on the generalized satisfability problems defned by Schaefer (in: Proceedings of the 10th STOC, San Diego, CA, USA, Association for Computing Machinery, New York, 1978, pp. 216–226) for which the arity of the constraints is fixed in order to study the associated phase transition. We establish new results on minimal elements associated with such generalized satis"ability problems. These results are the keys of the exploration we conduct on the location and on the nature of the phase transition for generalized satisfability. We first prove that the phase transition occurs at the same scale for every reasonable problem and we provide lower and upper bounds for the associated critical ratio. Our framework allows one to get these bounds in a uniform way, in particular, we obtain a lower bound proportional to the number of variables for k-SAT without analyzing any algorithm. Finally, we reveal the seed of coarseness for the phase transition of generalized satisfability: 2-XOR-SAT.  

  • 18.12.2013,
    Łukasz Janiszewski
    . Exploiting independent subformulas: A faster approximation scheme for #k-SAT by Manuel Schmitt , Rolf Wanka
    We present an improvement on Thurley’s recent randomized approximation scheme for #k-SAT where the task is to count the number of satisfying truth assignments of a Boolean function Φ given as an n-variable k-CNF. We introduce a novel way to identify independent substructures of Φ and can therefore reduce the size of the search space considerably. Our randomized algorithm works for any k. For #3-SAT, it runs in time O(ε−2 · 1.51426n), for #4-SAT, it runs in time O(ε−2 · 1.60816n), with error bound ε.  
    Michał Dyrek
    Boundary properties of the satisfiability problems by Vadim Lozin , Christopher Purcell
    The satisfiability problem is known to be NP-complete in general and for many restricted instances, such as CNF formulas with at most 3 variables per clause and at most 3 occurrences per variable, or planar formulas. The latter example refers to graphs representing satisfiability instances. These are bipartite graphs with vertices representing clauses and variables, and edges connecting variables to the clauses containing them. Finding the strongest possible restrictions under which the problem remains NP-complete is important for at least two reasons. First, this can make it easier to establish the NP completeness of new problems by allowing easier transformations. Second, this can help clarify the boundary between tractable and intractable instances of the problem. In this paper, we address the second issue and reveal the first boundary property of graphs representing satisfiability instances.  
    Przemysław Jedynak
    A Myhill-Nerode theorem for automata with advice by Alex Kruckman, Sasha Rubin, John Sheridan
    An automaton with advice is a finite state automaton which has access to an additional fixed infinite string called an advice tape. We refine the Myhill-Nerode theorem to characterize the languages of finite strings that are accepted by automata with advice. We do the same for tree automata with advice.  
    Adam Polak
    On the satisfiability threshold and clustering of solutions of random 3-SAT formulas, by Elitza Maneva, Alistair Sinclair
    We study the structure of satisfying assignments of a random 3-Sat formula. In particular, we show that a random formula of density  4:453 almost surely has no non-trivial ``core'' assignments. Core assignments are certain partial assignments that can be extended to satisfying assignments, and have been studied recently in connection with the Survey Propagation heuristic for random Sat. Their existence implies the presence of clusters of solutions, and they have been shown to exist with high probability below the satisfiability threshold for k-Sat with k  9 [D. Achlioptas, F. Ricci-Tersenghi, On the solution-space geometry of random constraint satisfaction problems, in: Proc. 38th ACM Symp. Theory of Computing, STOC, 2006, pp. 130139]. Our result implies that either this does not hold for 3-Sat, or the threshold density for satisfiability in 3-Sat lies below 4.453. The main technical tool that we use is a novel simple application of the first moment method.  
    Andrzej Dorobisz
    Regular Languages Accepted by Quantum Automata by Alberto Bertoni and Marco Carpentieri
    In this paper we analyze some features of the behaviour of quantum automata. In particular we prove that the class of languages recognized by quantum automata with isolated cut point is the class of reversible regular languages. As a more general result, we give a bound on the inverse error that implies the regularity of the language accepted by a quantum automaton  
    Kamil Jarosz
    On the strongly generic undecidability of the Halting Problem by Alexander Rybalov
    It has been shown in [J.D. Hamkins, A. Miasnikov, The halting problem is decidable on a set of asymptotic probability one, Notre Dame J. Formal Logic 47(4) (2006) 515–524] that the classical Halting Problem for Turing machines with one-way tape is decidable on a “large” set of Turing machines (a so-called generic set). However, here we prove that the Halting Problem remains undecidable when restricted to an arbitrary “very large” set of Turing machines (a so-called strongly generic set). Our proof is independent of a Turing machine model.  
    Michał Masłowski
    The Halting Problem Is Decidable on a Set of Asymptotic Probability One by Joel David Hamkins and Alexei Miasnikov
    The halting problem for Turing machines is decidable on a set of asymptotic probability one. The proof is sensitive to the particular computational models.  
    Agnieszka Łupińska
    Design and Implementation of a Parallel Priority Queue on Many-core Architectures by Xi He, Dinesh Agarwal, and Sushil K. Prasad
    An efficient parallel priority queue is at the core of the effort in parallelizing important non-numeric irregular computations such as discrete event simulation scheduling and branch-and-bound algorithms. GPGPUs can provide powerful computing platform for such non-numeric computations if an efficient parallel priority queue implementation is available. In this paper, aiming at fine-grained applications, we develop an efficient parallel heap system employing CUDA. To our knowledge, this is the first parallel priority queue implementation on manycore architectures, thus represents a breakthrough. By allowing wide heap nodes to enable thousands of simultaneous deletions of highest priority items and insertions of new items, and taking full advantage of CUDA’s data parallel SIMT architecture, we demonstrate up to 30-fold absolute speedup for relatively finegrained compute loads compared to optimized sequential priority queue implementation on fast multicores. Compared to this, our optimized multicore parallelization of parallel heap yields only 2-3 fold speedup for such fine-grained loads. This parallelization of a tree-based data structure on GPGPUs provides a roadmap for future parallelizations of other such data structures.  

  • 23.10.2013,
    Michał Marczyk
    Consistency in distributed systems, part II: avoiding synchronization with CRDTs (based on a paper by Shapiro, Preguiça, Baquero, Zawirski)
    In this closing part of a two-part series we will consider CRDTs, a systematic approach to eventual consistency. We will examine both the state-based and the operation-based approach, with some concrete examples. Finally, we will return to our motivating discussion from part I in considering how a system may incorporate both an eventually consistent data store and a limited dose of consensus to achieve excellent functional guarantees in a distributed setting. Key source: Shapiro, Preguiça, Baquero, Zawirski, "A comprehensive study of Convergent and Commutative Replicated Data Types",  
    Marek Markiewicz
    Cellular Automata on a Toeplitz Space.
    Toeplitz Space is a set of regular quasi-periodic bi-infinite words over a finite alphabet with at least two different letters endowed with a Besicovitch metric. It is an invariant set for every Cellular Automaton. During the talk I will present some properties of this space and I will discuss how CA behave on it. I will also present an idea of examining the continuity of evolution of a CA and show some very basic results in this topic.  

  • 13.10.2013,
    Michał Marczyk
    Consistency in distributed systems, part I: achieving consensus with Raft (presenting research by Ongaro & Ousterhout)
    In this opening part of a two-part series we will consider Raft, a new protocol for achieving consensus in a distributed system. Raft matches Paxos as far as efficiency is concerned, but is designed to be more readily understandable and more amenable to implementation without tweaks and additional optimizations. To motivate the discussion, we will briefly consider the concept of a distributed system and the circumstances in which such systems may or may not require consensus to make progress safely. Key source: Ongaro, Ousterhout, "In Search of an Understandable Consensus Algorithm" (draft, 2013-09-10),  
    Łukasz Janiszewski
    Tetris is Hard, Even to Approximate by Erik D. Demaine, Susan Hohenberger and David Liben-Nowell
    In the popular computer game of Tetris, the player is given a sequence of tetromino pieces and must pack them into a rectangular gameboard initially occupied by a given configuration of filled squares; any completely filled row of the gameboard is cleared and all pieces above it drop by one row. We prove that in the offline version of Tetris, it is NP-complete to maximize the number of cleared rows, maximize the number of tetrises (quadruples of rows simultaneously filled and cleared), minimize the maximum height of an occupied square, or maximize the number of pieces placed before the game ends. We furthermore show the extreme inapproximability of the first and last of these objectives to within a factor of p^{1−epsilon}, when given a sequence of p pieces, and the inapproximability of the third objective to within a factor of 2−epsilon, for any epsilon>0. Our results hold under several variations on the rules of Tetris, including different models of rotation, limitations on player agility, and restricted piece sets.  
    Aleksandra Piktus
    On the Additive Constant of the k-Server Work Function Algorithm' by Yuval Emek, Pierre Fraigniaud, Amos Korman i Adi Rosen
    We consider the Work Function Algorithm for the k-server problem (Chrobak andr Larmore, 1991; Koutsoupias and Papadimitriou, 1995). We show that if the Work Function Algorithm is c-competitive, then it is also strictly (2c)-competitive. As a consequence of (Koutsoupias and Papadimitriou, 1995) this also shows that the Work Function Algorithm is strictly (4k-2)-competitive.  
    Dawid Pustułka
    An alternate proof of Statman’s finite completeness theorem by B. Srivathsan, Igor Walukiewicz
    Statman’s finite completeness theorem says that for every pair of non-equivalent terms of simply-typed lambda-calculus there is a model that separates them. A direct method of constructing such a model is provided using a simple induction on the Böhm tree of the term.  
    Aneta Pawłowska
    TETRAVEX is NP-complete by Yasuhiko Takenaga and Toby Walsh
    Tetravex is a widely played one person computer game in which you are given n^2 unit tiles, each edge of which is labelled with a number. The objective is to place each tile within a n by n square such that all neighbouring edges are labelled with an identical number. Unfortunately, playing Tetravex is computationally hard. More precisely, we prove that deciding if there is a tiling of the Tetravex board given n^2 unit tiles is NP-complete. Deciding where to place the tiles is therefore NP-hard. This may help to explain why Tetravex is a good puzzle. This result compliments a number of similar results for one person games involving tiling. For example, NP-completeness results have been show for: the offline version of Tetris, KPlumber (which involves rotating tiles containing drawings of pipes to make a connected network), and shortest sliding puzzle problems. It raises a number of open questions. For example, is the infinite version Turing-complete? How do we generate Tetravex problems which are truly puzzling as random NP-complete problems are often surprising easy to solve? Can we observe phase transition behaviour? What about the complexity of the problem when it is guaranteed to have an unique solution? How do we generate puzzles with unique solutions?  
    Maria Chmaj
    Weight automata
    Monika Krupnik
    Inclusion problems for patterns with a bounded number of variables by Joachim Bremer, Dominik D. Freydenberger
    We study the inclusion problems for pattern languages that are generated by patterns with a bounded number of variables. This continues the work by Freydenberger and Reidenbach (Information and Computation 208 (2010)) by showing that restricting the inclusion problem to significantly more restricted classes of patterns preserves undecidability, at least for comparatively large bounds. For smaller bounds, we prove the existence of classes of patterns with complicated inclusion relations, and an open inclusion problem, that are related to the Collatz Conjecture. In addition to this, we give the first proof of the undecidability of the inclusion problem for NE-pattern languages that, in contrast to previous proofs, does not rely on the inclusion problem for E-pattern languages, and proves the undecidability of the inclusion problem for NE-pattern languages over binary and ternary alphabets.  
    Borg Łojasiewicz
    The state complexities of some basic operations on regular languages by Sheng Yu, Qingyu Zhuang and Kai Salomaa
    We consider the state complexities of some basic operations on regular languages. We show that the number of states that is sufficient and necessary in the worst case for a deterministic finite automaton DFA) to accept the catenation of an m-state DFA language and an n-state DFA language is exactly m2^n - 2^{n-1} for m,n> 1. The result of 2^{n-1}+2^{n-2} states is obtained for the star of an n-state DFA language, n>1. State complexities for other basic operations and for regular languages over a one-letter alphabet are also studied.  

  • 03.04.2013,
    Michał Bejda
    Subshifts, Languages and Logic by Emmanuel Jeandel and Guillaume Theyssier
    We study the Monadic Second Order (MSO) Hierarchy over infinite pictures, that is tilings. We give a characterization of existential MSO in terms of tilings and projections of tilings. Conversely, we characterise logic fragments corresponding to various classes of infinite pictures (subshifts of finite type, sofic subshifts).  
    Jacek Szmigiel
    Bad news on decision problems for patterns by Dominik D. Freydenberger, Daniel Reidenbach
    We study the inclusion problem for pattern languages, which—due to Jiang et al. [T. Jiang, A. Salomaa, K. Salomaa, S. Yu, Decision problems for patterns, Journal of Computer and System Sciences 50 (1995) 53–63]— is known to be undecidable. More precisely, Jiang et al. demonstrate that there is no effective procedure deciding the inclusion for the class of all pattern languages over all alphabets. Most applications of pattern languages, however, consider classes over fixed alphabets, and therefore it is practically more relevant to ask for the existence of alphabet-specific decision procedures. Our first main result states that, for all but very particular cases, this version of the inclusion problem is also undecidable. The second main part of our paper disproves the prevalent conjecture on the inclusion of so-called similar E-pattern languages, and it explains the devastating consequences of this result for the intensive previous research on the most prominent open decision problem for pattern languages, namely the equivalence problem for general E-pattern languages.  
    Marek Markiewicz
    Topology on words
    During the talk we will explore two types of topologies on the set of all infinite words over a finite alphabet with at least two different letters: the Cantor topology and its relative version U^\delta topology for an arbitrary languge U of finite words. We will describe close and open sets in both topologies and how they relate to each other. We will also explore the definitions of Chaitin and Martin-Löf random sequences and will prove their equivalence. Finally we will show that the set of Martin-Löf random sequences is co-nowhere dense in U^\delta topology for a special U. The talk is based on three papers: Topological characterization of random sequences by C. Calude, S. Marcus, L. Steiger; Weighted Finite Automata and Mertics in Cantor Space by L. Steiger and Exploring Randomness by G. Chaitin.  
    Marek Markiewicz
    Topology on words
    Adam Polak
    On the Complexity of the Equivalence Problem for Probabilistic Automata by Stefan Kiefer, Andrzej S. Murawski, Jo¨el Ouaknine, Bj¨orn Wachter1, and James Worrell
    Checking two probabilistic automata for equivalence has been shown to be a key problem for efficiently establishing various behavioural and anonymity properties of probabilistic systems. In recent experiments a randomised equivalence test based on polynomial identity testing outperformed deterministic algorithms. In this paper we show that polynomial identity testing yields efficient algorithms for various generalisations of the equivalence problem. First, we provide a randomized NC procedure that also outputs a counterexample trace in case of inequivalence. Second, we show how to check for equivalence two probabilistic automata with (cumulative) rewards. Our algorithm runs in deterministic polynomial time, if the number of reward counters is fixed. Finally we show that the equivalence problem for probabilistic visibly pushdown automata is logspace equivalent to the Arithmetic Circuit Identity Testing problem, which is to decide whether a polynomial represented by an arithmetic circuit is identically zero.  
    Paweł Wanat
    The Local Lemma is Tight for SAT by H. Gebauer
    We construct unsatisfiable k-CNF formulas where every clause has k distinct literals and every variable appears in at most (2/e + o(1))2^k/k clauses. The lopsided Local Lemma shows that our result is asymptotically best possible: every k-CNF formula where every variable appears in at most 2^(k+1)/e(k+1) 1 clauses is satisfiable. The determination of this extremal function is particularly important as it represents the value where the k-SAT problem exhibits its complexity hardness jump: from having every instance being a YESinstance it becomes NP-hard just by allowing each variable to occur in one more clause. The asymptotics of other related extremal functions are also determined. Let l(k) denote the maximum number, such that every k-CNF formula with each clause containing k distinct literals and each clause having a common variable with at most l(k) other clauses, is satisfiable. We establish that the bound on l(k) obtained from the Local Lemma is asymptotically optimal, i.e., l(k) = (1/e + o(1))2^k. The constructed formulas are all in the class MU(1) of minimal unsatisfiable formulas having one more clause than variables and thus they resolve these asymptotic questions within that class as well.  

  • 09.01.2013,
    Andrzej Dorobisz
    Functions definable by numerical set-expressions by IAN PRATT-HARTMANN and IVO DÜNTSCH
    A numerical set-expression is a term specifying a cascade of arithmetic and logical operations to be performed on sets of non-negative integers. If these operations are confined to the usual Boolean operations together with the result of lifting addition to the level of sets, we speak of additive circuits. If they are confined to the usual Boolean operations together with the result of lifting addition and multiplication to the level of sets, we speak of arithmetic circuits. In this article, we investigate the definability of sets and functions by means of additive and arithmetic circuits, occasionally augmented with additional operations.  

  • 19.12.2012,
    Przemysław Jedynak
    We investigate the number of occurrences of a word u as a (scattered) subword of a word w. The notion of a Parikh matrix, recently introduced, is a basic tool in this investigation. In general, several words are associated with a Parikh matrix. The ambiguity can be resolved by associating a unique word called the Lyndon image to each Parikh matrix. In this paper we will investigate properties of Lyndon images and the corresponding questions of ambiguity. We give an exhaustive characterization in the case of a binary alphabet. Our main results in the general case deal with the comparison of unambiguous words and Lyndon images, algorithms for constructing Lyndon images, as well as classes of words with the same Parikh matrix, obtained by circular variance.  
    Maciej Bendkowski
    Maciej Bendkowski
    Nondeterministic finite automata (NFAs) were introduced in [68], where their equivalence to deterministic finite automata was shown. Over the last 50 years, a vast literature documenting the importance of finite automata as an enormously valuable concept has been developed. In the present paper, we tour a fragment of this literature. Mostly, we discuss recent developments relevant to NFAs related problems like, for example, (i) simulation of and by several types of finite automata, (ii) minimization and approximation, (iii) size estimation of minimal NFAs, and (iv) state complexity of language operations. We thus come across descriptional and computational complexity issues of nondeterministic finite automata. We do not prove these results but we merely draw attention to the big picture and some of the main ideas involved.  
    Maciej Gawron
    Hilbert's tenth problem
    The question of finding an algorithm to determine whether a given Diophantine equation has an integer solution, was one of the famous Hilbert's problems, posed in 1900. It was finally answered (negatively) by Yuri Matiyasevich in 1970. We will show the proof of this fact. We will introduce the notion of Diophantine sets, relations and functions. We will prove that Diophantine sets are exactly computably enumerable sets. We will show that there exists an universal Diophantine equation, then using standard diagonal method we will prove that Hilbert's tenth problem is undecidable.  
    Arkadiusz Olek
    Verifiable secret sharing in a total of three rounds by Shashank Agrawal
    Verifiable secret sharing (VSS) is an important building block in the design of secure multiparty protocols, when some of the parties are under the control of a malicious adversary. Henceforth, its round complexity has been the subject of intense study. The best known unconditionally secure protocol takes 3 rounds in sharing phase, which is known to be optimal, and 1 round in reconstruction. Recently, by introducing a negligible probability of error in the definition of VSS, Patra et al. [CRYPTO 2009] have designed a novel protocol which takes only 2 rounds in sharing phase. However, the drawback of their protocol is that it takes 2 rounds in reconstruction as well. Hence, the total number of rounds required for VSS remains the same. In this paper, we present a VSS protocol which takes a total of 3 rounds only—2 rounds in sharing and 1 round in reconstruction.  
    Michał Marczyk
    Unification type of bounded distributive lattices
    We will present S. Ghilardi's proof of his unification type theorem for bounded distributive lattices. The focus will be on the main result; a high-level overview of the underlying methodology will be presented without detailed proofs of the individual results (which have been discussed in this seminar at an earlier date). The theorem as well as the methodology employed in establishing it have been presented in S. Ghilardi, "Unification through Projectivity", Journal of Logic and Computation (1997) 7.  
    Katarzyna Grygiel
    Finite lattices and their weighted double skeletons
    In 1973 Christian Herrmann introduced the notion of the skeleton of a finite lattice. The skeleton of a lattice, however, does not suffice to reconstruct the initial lattice uniquely. Even worse, it turns out that every finite lattice is the skeleton of infinitely many non-isomorphic distributive lattices. At this point a natural question arises whether one can stuff the skeleton with some additional data in order to restore the original lattice. During the talk I will focus on the so-called weighted double skeletons. These objects, not being lattices themselves, turn out to fully characterize a particular kind of lattices.  
    Michał Sapalski
    The non-uniform Bounded Degree Minimum Diameter Spanning Tree problem with an application in P2P networking by Jakarin Chawachat, Jittat Fakcharoenphol, Wattana Jindaluang
    This paper considers the Bounded Degree Minimum Diameter Spanning Tree problem (BDST problem) with non-uniform degree bounds. In this problem, we are given a metric length function  over a set V of n nodes and a degree bound Bv for each v ∈ V, and want to find a spanning tree with minimum diameter such that each node v has degree at most Bv . We present a simple extension of an O(logn ) -approximation algorithm for this problem with uniform degree bounds of Könemann, Levin, and Sinha [J. Könemann, A. Levin, A. Sinha, Approximating the degree-bounded minimum diameter spanning tree problem, in: Algorithmica, Springer, 2003, pp. 109–121] to work with nonuniform degree bounds. We also show that this problem has an application in the peerto- peer content distribution. More specifically, the Minimum Delay Mesh problem (MDM problem) introduced by Ren, Li and Chan [D. Ren, Y.-T. Li, S.-H. Chan, On reducing mesh delay for peer-to-peer live streaming, in: INFOCOM, 2008, pp. 1058–1066] under a natural assumption can be reduced to this non-uniform case of the BDST problem.  
    Agnieszka Łupińska
    On building minimal automaton for subset matching queries by Kimmo Fredriksson
    We address the problem of building an index for a set D of n strings, where each string location is a subset of some finite integer alphabet of size σ, so that we can answer efficiently if a given simple query string (where each string location is a single symbol) p occurs in the set. That is, we need to efficiently find a string d ∈ D such that p[i] ∈ d[i] for every i. We show how to build such index in O(nlogσ/(σ) log(n)) average time, where  is the average size of the subsets. Our methods have applications e.g. in computational biology (haplotype inference) and music information retrieval.  
    Michał Masłowski
    Regular patterns, regular languages and context-free languages by Sanjay Jain, Yuh Shin Ong, Frank Stephan
    In this paper we consider two questions. First we consider whether every pattern language which is regular can be generated by a regular pattern. We show that this is indeed the case for extended (erasing) pattern languages if alphabet size is at least four. In all other cases, we show that there are patterns generating a regular language which cannot be generated by a regular pattern. Next we consider whether there are pattern languages which are context-free but not regular. We show that, for alphabet size 2 and 3, there are both erasing and non-erasing pattern languages which are context-free but not regular. On the other hand, for alphabet size at least 4, every erasing pattern language which is context-free is also regular. It is open at present whether there exist non-erasing pattern languages which are context-free but not regular for alphabet size at least 4.  
    Piotr Wójcik
    Some results about decidability of sets of tautologies in first order languages.
    The fundamental question whether a set of first order tautologies is decidable was answered (negatively) by Church in 1936. By restricting the classes of considered sentences (e.g. by reducing the number of function symbols or the arity of predicates), we can produce some positive results. After exploring well-known languages, we will move on to study more complex systems, like first order monadic temporal logic. There, even without function symbols and equality, the set of tautologies is not recursively enumerable.  
    Mateusz Kostanek
    Reconciliation of elementary order and metric fixpoint theorems
    We prove two new fixed point theorems for generalized metric spaces and show that various fundamental fixed point principles, including: Banach Contraction Principle, Caristi fixed point theorem for metric spaces, Knaster-Tarski fixed point theorem for complete lattices, and the Bourbaki-Witt fixed point theorem for directed-complete orders, follow as corollaries of our results.  
    Michał Marczyk
    Persistent data structures
    Persistent data structures, that is data structures which are immutable and support efficient creation of slightly modified copies with no change to the complexity guarantees of the basic operations (both on the copy and on the original) are of key importance for the performance of programs written in the functional paradigm. We will examine in some detail a single example, namely a hash table offering logarithmic complexity of the basic operations with very good constants. The data structure in question is based on the mutable Hash Array Mapped Trie described in Phil Bagwell's paper "Ideal Hash Trees"

    [1] (see also Phil Bagwell, "Fast And Space Efficient Trie Searches" [2]). The persistent version was pioneered by Rich Hickey and is used in the Clojure programming language [3], [4], [5] ([4] -- the Java implementation used in Clojure; [5] -- the ClojureScript port of [4] used in ClojureScript).







  • 06.06.2012,
    Michał Handzlik
    Asymetric grammars
    Asymetric gramars are natural generalization of leftist grammars. Leftist grammars were introduced by Motwani as a tool useful to study accessibility problems in some protection systems. Since then, some interesting language-theoretical research has been carried out in this field. For example, the membership problem for leftist grammar is decidable. We propose a natural way to generalize the notion od leftist grammar. We study how this generalization affects the location of languages generated by those grammars within the Chomsky hierarchy. The main result states that membership problem for asymetric grammars is undecidable.  
    Marek Markiewicz
    A new class of hyper-bent Boolean functions in binomial forms by Baocheng Wang, Chunming Tang, Yanfeng Qi, Yixian Yang and Maozhi Xu
    Bent functions, which are maximally nonlinear Boolean functions with even numbers of variables and whose Hamming distance to the set of all affine functions equals 2^{n−1} ± 2^{n/2 −1}, were introduced by Rothaus in 1976 when he considered problems in combinatorics. Bent unctions have been extensively studied due to their applications in cryptography, such as S-box, block cipher and stream cipher. Further, they have been applied to coding theory, spread spectrum and combinatorial design. Hyper-bent functions, as a special class of bent functions, were introduced by Youssef and Gong in 2001, which have stronger properties and rarer elements. Many research focus on the construction of bent and hyper-bent functions.  
    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.  
    Piotr Zaborski
    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.  
    Maciej Gawron
    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 fi rst tabulation of this value.  
    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.  
    Michał Feret
    Optimal Stopping and Applications 5
    Chapter 6. Maximizing the Rate of Return.  
  • Thomas S. Ferguson, Optimal Stopping and Applications
  • 28.03.2012,
    Agnieszka Łupińska
    Optimal Stopping and Applications 4
    Chapter 5. Monotone Stopping Rule Problems.  
  • Thomas S. Ferguson, Optimal Stopping and Applications
  • 21.03.2012,
    Szymon Kałasz
    Optimal Stopping and Applications 3
  • Thomas S. Ferguson, Optimal Stopping and Applications
  • 14.03.2012,
    Paweł Wanat
    Optimal Stopping and Applications 2
    Chapter 4. Applications. Markov Models.  
  • 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.  
    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.  
    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.  
    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.  
    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.  
    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.  

    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.  
    Michał Handzlik
    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.  

    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.  
    Jakub Kozik
    Optimal stopping for covert expansion.
    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.  
    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.  
    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.  
    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.  
    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.  
    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  

    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.


    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  

    Agnieszka Łupińska
    A Universal Approach to Self-Referential Paradoxes, Incompleteness and Fixed Points, by Noson S. Yanofsky

  • 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.  
    Robert Obryk
    Algorithmic Information Theory 2, by Gregory. J. Chaitin

  • 04.05.2011,
    Robert Obryk
    Algorithmic Information Theory , by Gregory. J. Chaitin
    Marek Wróbel, Adam Zydroń
    Mathematics for the Analysis of Algorithms - Asymptotic Analysis
    Maciej Bendkowski
    Mathematics for the Analysis of Algorithms - Operator Methods
    Michał Masłowski, Tomasz Bińczycki
    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.  

    Michał Masłowski
    Mathematics for the Analysis of Algorithms - Recurrence Relations
    Tomasz Bińczycki
    Mathematics for the Analysis of Algorithms - Binomial Identities
    Przemek Jedynak
    Synthetic Differential Geometry - Chicago's pizza seminar notes.
    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.  
    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.  
    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.  
    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'').  

    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]  

    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.  
    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.  
    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.  
    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.  
    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.  
    Kuba Kozik
    Recent progress in best-choice problems for posets.
    Jan Hązła
    Denotational semantics of T
    Maria Chmaj
    Coherent Spaces
    Karol Kosiński
    Sequent calculus, chapter 5 of Girard's book.
    Rafał Pajdzik
    The Normalization Theorem, Chapter 4 of Girard's book.
    Leszek Horwath (Cedric)
    Curry Howard Isomorphism. Chapter 3 of Girard's book.
    Szymon Borak
    Fixed point theory for programs
    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


    A. Semantics of System F - by Paul Taylor
    B. What is Linear Logic? - by Yves Lafont  
    Marek Wróbel
    Program Analysis
    Ostatnia część książki Changa and Lee o dowodzeniu twierdzeń.  
    Michał Handzlik
    Procedury dowodowe oparte na twierdzeniu Herbranda
    Rozdział 9. książki Changa i Lee o automatycznym dowodzeniu twierdzeń.  
    Maria Chmaj
    Rozdział 8. książki Changa i Lee o automatycznym dowodzeniu twierdzeń.  
    Jan Hązła
    Linear Resolution in FOL
    Rozdział 7. książki Changa & Lee.  
    Adam Zydro
    Semantic Resolution
    Rozdział 6. ksiązki Changa & Lee.  
    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.  
    Sylwia Antoniuk
    Rezolucja jako rewolucja, w relacji do rewelacji.  
    Rafał Pajdzik, UJ
    Chapters 3,4 on First Order Logic from `Symbolic Logic and Mechanical Theorem Proving' by Chin-Liang Chang and Richard Char-Thung Lee.  
    Marek Zaionc
    Schwichtenberg style lambda definability is undecidable
    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.  
    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.  
    Jakub Kozik
    Drzewa and/or - przegląd problemów
    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.  
    Wojciech Czarnecki
    The Curry-Howard Isomorphism
    Michał Klasiński
    Wśród typów nie ma arystokracji
    Sylwia Antoniuk
    Basic Simple Type Theory
    Michał Handzlik
    Higher-order Unificatrion and Matching
    Paweł Waszkiewicz
    A Lazy Introduction to Goedel's Theorems
    See for more info.  
    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).  
    Michał Pokrywka
    Algorytmy kolejkowania danych w sieciach komputerowych
    cd z poprzedniego roku.  
    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.  
    Mateusz Drewienkowski
    Dualność Stone'a - cz.2.
    Mateusz Drewienkowski
    Dualność Stone'a - cz.1.
    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.  
    Mateusz Kostanek
    Quantale semantics of linear logic (2)
    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.  
    Mateusz Kostanek
    Quantale semantics for linear logic
    Jakub Kozik
    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.  
    Mateusz Juda
    Arytmetyka Heytinga
    Na podstawie skryptu Thomasa Streichera (patrz poprzednie referaty tego samego autora).  
    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.  
    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.  
    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 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.  
    Mateusz Juda
    Introduction to Constructive Logic and Mathematics (II)
    Omawiamy kolejne tematy ze skryptu Thomasa Streichera. Dzisiaj:
    - Constructive Arithmetic and Analysis
    - Constructive Real Numbers  
    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.  
    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)  
    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.  
    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.  
    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.  
    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.  
    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.  
    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.  
    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
    albo od razu tutaj .  
    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.  
    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.  
    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.  
    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.  
    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.  
    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,