Podstawy Informatyki

środa: 12:15 - 14:00, sala 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.

29.03.2017 12:15
Szymon Stankiewicz

A packing polynomial is a polynomial that maps the set N^2 of lattice points with nonnegative coordinates bijectively onto N. Cantor constructed two quadratic packing polynomials, and Fueter and Polya proved analytically that the Cantor polynomials are the only quadratic packing polynomials.
The purpose of this paper is to present a beautiful elementary proof of Vsemirnov of the Fueter-Polya theorem. It is a century-old conjecture that the Cantor polynomials are the only packing polynomials on N^2.

Poprzednie referaty

15.03.2017 12:15
Łukasz Lachowski
Impossibility of Distributed Consensus with One Faulty Process by MICHAEL J. FISCHER, NANCY A. LYNCH AND MICHAEL S. PATERSO
The consensus problem involves a asynchronous system of processes, some of which may be unreliable.The problem is for the reliable processes to agree on a binary value. In this paper, it is shown that every protocol for this problem has the possibility of nontermination, even with only one faulty process. By way of contrast, solutions are known for the synchronous case, the “Byzantine Generals” problem.
08.03.2017 12:15
Maciej Bendkowski
Boltzmann samplers: random generation of combinatorial structures with an application to lambda calculus
In their seminal paper, Duchon et al. proposed a surprisingly simple, general-purpose framework of Boltzmann samplers meant for random generation of combinatorial structures. In this talk we revisit their method and discuss its elegant relation with analytic combinatorics as well as important practical implementation details. Finally, we discuss the application of Boltzmann samplers to the random generation of lambda terms used, e.g. in testing functional programming compilers.
01.03.2017 12:15
Michał Zwonek
Wielomianowe kodowania

Rozważany będzie problem istnienia wielomianowej bijekcji, najniższego stopnia, między N^k, a N. Przedstawione będą także problemy otwarte związane z tą tematyką.

Materiały do wystąpienia:

1) Elementarny dowód Twierdzenie Feuter-Polya (jedyny kwadratowy i bijektywny wielomian N^2->N to funkcja cantore'a) https://arxiv.org/abs/1512.08261

2) Praca, w której autorzy pokazują nieistnienie wielomianów 3 i 4 stopnia.  http://www.sciencedirect.com/science/article/pii/0022314X78900367

3) Praca podobnie tematyczna odnosząca się do problemu istnienia wielomianów bijektywnych z pewnego sektora N^2 w N. (To o czym wspomniałem na koniec, opis tego problemu jest też pod koniec w 1) ). Pod koniec pracy jest opisane 6 problemów otwartych związanych z tą tematyką. https://arxiv.org/abs/1305.2538

4) W podobnej tematyce. http://www.sciencedirect.com/science/article/pii/0022314X78900355


25.01.2017 12:00
Sylwester Klocek
Incompleteness, Undecidability and Automated Proofs by Cristian S. Calude and Declan Thompson
Incompleteness and undecidability have been used for many years as arguments against automatising the practice of mathematics. The advent of powerful computers and proof-assistants – programs that assist the development of formal proofs by human-machine collaboration – has revived the interest in formal proofs and diminished considerably the value of these arguments. In this paper we discuss some challenges proof-assistants face in handling undecidable problems – the very results cited above – using for illustrations the generic proof-assistant Isabelle.
18.01.2017 12:00
Michał Ziobro
Inhabitation in Simply-Typed Lambda-Calculus through a Lambda-Calculus for Proof Search by Jose Espırito Santo, Ralph Matthes, Luıs Pinto
Kontynuacja seminarium z 23.11.2016
11.01.2017 12:00
Patryk Mikos
We give asymptotic estimates and some explicit computations for both the number of distinct languages and the number of distinct finite languages over a k-letter alphabet that are accepted by deterministic finite automata (resp. nondeterministic finite automata) with n states.
04.01.2017 12:00
Konrad Kalita
We establish that several classical context-free languages are inherently ambiguous by proving that their counting generating functions, when considered as analytic functions, exhibit some characteristic form of transcendental behaviour. To that purpose, we survey some general results on elementary analytic properties and enumerative uses of algebraic functions in relation to formal languages In particular, the paper contains a general density theorem for unambiguous context-free languages.
14.12.2016 12:00
Piotr Wójcik
Enumeration and random generation of accessible automata by Frederique Bassino and Cyril Nicaud
We present a bijection between the A_n of deterministic and accessible automata with n states on a k-letters alphabet and some diagrams, which can themselves be represented as partitions of a set of kn + 1 elements into n non-empty subsets. This combinatorial construction shows that the asymptotic order of the cardinality of A_n is related to the Stirling number. Our bijective approach also yields an efficient random sampler, for the uniform distribution, of automata with n states, its complexity is O(n^3/2), using the framework of Boltzmann samplers.
07.12.2016 12:00
Jakub Brzeski
We survey recent results on the enumeration of formal languages. In particular, we consider enumeration of regular languages accepted by deterministic
and nondeterministic finite automata with n states, regular languages generated by regular expressions of a fixed length, and !-regular languages accepted by Müller automata. We also survey the uncomputability of enumeration of context-free languages and more general structures.
30.11.2016 12:00
Yauheni Ananchuk
Binary Constraint Problems have traditionally been considered as Network Satisfaction Problems over some relation algebra. A constraint network is satisfable if its nodes can be mapped into some representation of the relation algebra in such a way that the constraints are preserved. A qualitative representation is like an ordinary representation, but instead of requiring (a ; b) = a j b , as we do for ordinary representations, we only require that. A constraint network is qualitatively satisfable if its nodes can be mapped to elements of a qualitative representation, preserving the constraints. If a constraint network is satisfable then it is clearly qualitatively satisfable, but the converse can fail.
However, for a wide range of relation algebras including the point algebra, the Allen Interval Algebra, RCC8 and many others, a network is satisfable if and only if it is qualitatively satisfable. Unlike ordinary composition, the weak composition arising from qualitative representations need not be associative, so we can generalise by considering network satisfaction problems over non-associative algebras. We prove that computationally, qualitative representations have many advantages over
ordinary representations: whereas many finite relation algebras have only infnite representations, every finite qualitatively representable algebra has a finite qualitative representation; the representability problem for (the atom structures of) finite non-associative algebras is NP-complete; the network satisfaction problem over a finite qualitatively representable algebra is always ; the validity of equations over qualitative representations is co-NP-complete. On the other hand we prove that there is no finite axiomatisation of the class of qualitatively representable algebra
Michał Ziobro
Inhabitation in Simply-Typed Lambda-Calculus through a Lambda-Calculus for Proof Search by Jos´e Espırito Santo, Ralph Matthes, Luıs Pinto
A new, comprehensive approach to inhabitation problems in simply-typed lambda-calculus is shown, dealing with both decision and counting problems. This approach works by exploiting a representation of the search space generated by a given inhabitation problem, which is in terms of a lambda-calculus for proof search that the authors developed recently. The representation may be seen as extending the Curry-Howard representation of proofs by lambda-terms, staying within the methods of lambda-calculus and type systems. Our methodology reveals inductive descriptions of the decision problems, driven by the syntax of the proof-search expressions, and the end products are simple, recursive decision procedures and counting functions.
Michał Zieliński
Most programs stop quickly or never halt by Cristian S. Calude and Michael A. Stay
The aim of this paper is to provide a probabilistic, but non-quantum, analysis of the Halting Problem. Our approach is to have the probability space extend over both space and time and to consider the probability that a random N-bit program has halted by a random time.We postulate an a priori computable probability distribution on all possible runtimes and we prove that given an integer k >0, we can effectively compute a time bound T such that the probability that an N-bit program will eventually halt given that it has not halted by T is smaller than 2^{−k}. We also show that the set of halting programs (which is computably enumerable, but not computable) can be written as a disjoint union of a computable set and a set of effectively vanishing probability. Finally, we show that “long” runtimes are effectively rare. More formally, the set of times at which an N-bit program can stop after the time 2^{N+constant} has effectively zero density.
Wojciech Kruk
On the generic undecidability of the Halting Problem for normalized Turing machines by Alexander Rybalov
Hamkins and Miasnikov presented in 2004 a generic algorithm deciding the classical Halting Problem for Turing machines with one-way tape on a set of asymptotic probability one (on a so-called generic set). Rybalov in 2007 showed that there is no generic algorithm deciding this problem on strongly generic sets of inputs (some subclass of generic sets). In this paper we prove that there is no generic algorithm deciding the Halting Problem for normalized Turing machines on generic sets of inputs. Normalized Turing machines have programs with the following natural restriction: internal states with large indices
are not allowed at the beginning of the program. This condition does not reduce the class of computable functions because for every Turing machine there exists a normalized Turing machine which computes the same function. Our proof holds for machines with one-way and two-way tape. It also implies that the Hamkins-Miasnikov algorithm is not generic for normalized Turing machines.
Wojciech Łopata
Universality and Almost Decidability by Cristian S. Calude and Damien Desfontaines
We present and study new definitions of universal and programmable universal unary functions and consider a new simplicity criterion: almost decidability of the halting set. A set of positive integers S is almost decidable if there exists a decidable and generic (i.e. a set of natural density one) set whose intersection with S is decidable. Every decidable set is almost decidable, but the converse implication is false. We prove the existence of infinitely many universal functions whose halting sets are generic (negligible, i.e. have density zero) and (not) almost decidable. One result—namely, the existence of infinitely many universal functions whose halting sets are generic (negligible) and not almost decidable—solves an open problem in [9]. We conclude with some open problems.
Pola Kyzioł
The domino problem for self-similar structures by Sebastian Barbieri and Mathieu Sablik
We defne the domino problem for tilings over self-similar structures of $Z^d$ given by forbidden patterns. In this setting we exhibit non-trivial families of subsets with decidable and undecidable domino problem.
Tomasz Kisielewski
Programy które są w stanie przeprowadzać rozumowania o swoich własnościach
Proving properties of programs within their language

Przedstawię wstępną wersję swojego programu badawczego, mającego
na celu umożliwienie dowodzenia własności programów w języku, w
którym są napisane. Zacznę od motywacji, opierającej się o pewne
rozwiązanie zmodyfikowanego dylematu więźnia, w której graczami
są programy mające dostęp do kodu źródłowego drugiego gracza.
Następnie przybliżę obecny stan automatycznego dowodzenia faktów
o programach, ze szczególnym uwzględnieniem silnie typowanych
języków funkcyjnych. Na koniec przedstawię dalekosiężne cele i
największe trudności, których należy się spodziewać przy
implementacji efektywnych funkcji dowodzących fakty o programach.


I will present an initial version of my research program, whose

main goal is to enable proving properties about programs within
the language they are written in. My motivation is based on a
specific solution to the open-source prisoner's dilemma, where
the players are programs with access to the other player's source
code. After explaining the motivation I will shortly present the
current state of automatic proving of programs' properties, with
emphasis on strongly typed functional languages. Finally, I will
introduce my long term goals and the main challenges one should
expect to face when implementing an effective function for
proving facts about programs.

Piotr Kawałek i Teodor Jerzak
Generalised and Quotient Models for Random And/Or Trees and Application to Satisfiability by Antoine Genitrini and Cécile Mailler:

This article is motivated by the following satisfiability question: pick uniformly at random an and/or Boolean expression of length n, built on a set of k_n Boolean variables. What is the probability that this expression is satisfiable? asymptotically when n tends to infinity? The model of random Boolean expressions developed in the present paper is the model of Boolean Catalan trees, already extensively studied in the literature for a constant sequence. The fundamental breakthrough of this paper is to generalise the previous results for any (reasonable) sequence of integers which enables us, in particular, to solve the above satisfiability question. We also analyse the effect of introducing a natural equivalence relation on the set of Boolean expressions. This new quotient model happens to exhibit a very interesting threshold (or saturation) phenomena.



Kamil Pietruszka
Regular Combinators for String Transformations by Rajeev Alur Adam Freilich Mukund Raghothaman

We focus on (partial) functions that map input strings to a monoid such as the set of integers with addition and the set of output strings with concatenation. The notion of regularity for such functions has been defined using two-way finite-state transducers, (one-way) cost register automata, and MSO-definable graph transformations. In this paper, we give an algebraic and machine-independent characterization of this class analogous to the definition of regular languages by regular expressions. When the monoid is commutative, we prove that every regular function can be constructed from constant functions using the combinators of choice, split sum, and iterated sum, that are analogs of union, concatenation, and Kleene *, respectively, but enforce unique (or unambiguous) parsing. Our main result is for the general case of non-commutative monoids, which is of particular interest for capturing regular string-to-string transformations for document processing. We prove that the following additional combinators suffice for constructing all regular functions:

(1) the left-additive versions of split sum and iterated sum, which allow transformations such as string reversal;

(2) sum of functions, which allows transformations such as copying of strings; and

(3) function composition, or alternatively, a new concept of chained sum, which allows output values from adjacent blocks to mix.

Piotr Bejda

Let F \subset S_k be a finite set of permutations and let C_n (F) denote the number of permutations  avoiding the set of patterns F.
The Noonan Zeilberger conjecture states that the sequence Cn(F) is P-recursive. We disprove this conjecture. The proof uses Computability Theory and builds on our earlier work [GP1]. We also give two applications of our approach to complexity of computing C_n(F).


Pola Kyzioł
NP-Completeness of a Combinator Optimization Problem by M. S. Joy and V. J. Rayward-Smith

We consider a deterministic rewrite system for combinatory logic over combinators $S,K,I,B,C,S',B'$, and $C'$.
Terms will be represented by graphs so that reduction of a duplicator will cause the duplicated expression to be "shared" rather than copied. To each normalizing term we assign a weighting which is the number of reduction steps necessary to reduce the expression to normal form. A lambda-expression may be represented by several distinct expressions in combinatory logic, and two combinatory logic expressions are considered equivalent if they represent the same lambda-expression (up to $\beta $-$\eta $-equivalence). The problem of minimizing the number of reduction steps over equivalent combinator expressions (i.e., the problem of finding the "fastest running" combinator representation for a specific lambda-expression) is proved to be NP-complete by reduction from the "Hitting Set" problem.

Michał Zieliński
Beta Reduction is Invariant, Indeed by Beniamino Accattoli and Ugo Dal Lago

Slot and van Emde Boas weak invariance thesis states that reasonable machines can simulate each other within a polynomially overhead in time.Is lambda  calculus a reasonable machine? Is there a way to measure the computational complexity of a lambda term? This paper presents the first complete positive answer to this longstanding problem. Moreover, our answer is completely machineindependent and based over a standard notion in the theory of lambda calculus: the length of a leftmost-outermost derivation to normal form is an invariant cost model. Such a theorem cannot be proved by directly relating lambda calculus with Turing machines or random access machines, because of the size explosion problem: there are terms that in a linear number of steps produce an exponentially long output. The first step towards the solution is to shift to a notion of evaluation for which the length and the size of the output are linearly related. This is done by adopting the linear substitution calculus (LSC), a calculus of explicit substitutions modelled after linear logic proof nets and admitting a decomposition of leftmostoutermost
derivations with the desired property. Thus, the LSC is invariant with respect to, say, random access machines. The second step is to show that LSC is invariant with respect to the lambda calculus. The size explosion problem seems to imply that this is not possible:having the same notions of normal form, evaluation in the LSC is exponentially longer than in the lambda calculus. We solve such an impasse by introducing a new form of shared normal form and shared reduction, deemed useful. Useful evaluation avoids those steps that only unshare the output without contributing to bata redexes, i.e. the steps that cause the blow-up in size. The main technical contribution of the paper is indeed the definition of useful reductions and the thorough analysis of their properties.

Wojciech Kruk
On the equivalence of different presentations of Turner's bracket abstraction algorithm by Lukasz Czajka

Turner's bracket abstraction algorithm is perhaps the most well-known improvement on simple bracket abstraction algorithms. It is also one of the most studied bracket abstraction algorithms. The definition of the algorithm in Turner's original paper is slightly ambiguous
and it has been subject to different interpretations. It has been erroneously claimed in some papers that certain formulations of Turner's algorithm are equivalent. In this note we clarify the relationship between various presentations of Turner's algorithm and we show that some of them are in fact equivalent for translating lambda-terms in beta-normal form.

Katarzyna Janocha
On the Computing Power of +, -, and x by Marcello Mamino

Modify the Blum-Shub-Smale model of computation replacing the permitted computational primitives (the real field operations) with any finite set B of real functions semialgebraic over the rationals. Consider the class of Boolean decision problems that can be solved
in polynomial time in the new model by machines with no machine constants. How does this class depend on B? We prove that it
is always contained in the class obtained for B = {+, - , x}. Moreover, if B is a set of continuous semialgebraic functions containing + and -, and such that arbitrarily small numbers can be computed using B, then we have the following dichotomy: either our class is P or it coincides with the class obtained for B = {+ , - x} .

Maciej Poleski
The Fractal Dimension of SAT Formulas by Carlos Ansotegui, Maria Luisa Bonet, Jesus Giraldez-Cru and Jordi Levy

Modern SAT solvers have experienced a remarkable progress on solving industrial instances. Most of the techniques have been developed
after an intensive experimental testing process. Recently, there have been some attempts to analyze the structure of these formulas in terms of complex networks, with the long-term aim of explaining the success of these SAT solving techniques, and possibly improving them. We study the fractal dimension of SAT formulas, and show that most industrial families of formulas are self-similar, with a small fractal dimension. We also show that this dimension is not affected by the addition of learnt clauses. We explore how the dimension of a formula, together with other graph properties can be used to characterize SAT instances. Finally, we give empirical evidence that these graph properties can be used in state-of-the-art portfolios.

Magdalena Wiercioch
Principal types of BCK-lambda-termss by Sachio Hirokawa

BCK-lambda-terms are the I-terms in which each variable occurs at most once. The principal type of a lambda-term is the most general type of the term. In this paper we prove that if two BCK-lambda-terms in beta-normal form have the same principal type then they are identical. This solves the following problem (Y. Komori, 1987) in more general form: if two closed beta eta-normal form BCK-lambda-terms are assigned to the same minimal BCK-formula, are they identical? A minimal BCK-formula is the most general formula among BCK-provable formulas with respect to substitutions for type variables. To analyze type assignment, the notion of "connection" is introduced. A connection is a series of occurrences of a type. in a type assignment figure. Connected occurrences of a type have the same
meaning. The occurrences of the type in distinct connection classes can be rewritten separately; as a result, we have more general type assignment. By "formulae-as-types" correspondence, the result implies the uniqueness of the normal proof
figure for principal BCK-formulas. The result is valid for BCI-logic or implicational fragment of
linear logic as well.

Agnieszka Łupińska

The talk is about the parallel approach to the standard translation between Lambda Calculus and Combinatory Logic. Let L be a lambda-term and C be a combinator produced from L by the standard translation. Each lambda abstraction occurring in L, causes the linear expansion of some paths in the tree of the C combinator. We will show that the tree expansion can be performed parallel in logarithmic time on the path length. We will also discuss whether this procedure can be performed in the constant time.

Piotr Wójcik
Asymptotic properties of first order logic with one binary predicat symbol (wyniki własne)

Wyniki własne

Zygmunt Łenyk
Minimum Propositional Proof Length is NP-Hard to Linearly Approximate (by Michael Alekhnovich, Sam Buss, Shlomo Morany and Toniann Pitassi)

We prove that the problem of determining the minimum propositional proof length is NP-hard to approximate within a factor of 2^log^{1-o(1)} n. These results are very robust in that they hold for almost all natural proof systems, including: Frege systems, extended Frege systems, resolution, Horn resolution, the polynomial calculus, the sequent calculus, the cut-free sequent calculus, as well as the polynomial calculus. Our hardness of approximation results usually apply to proof length measured either by number of symbols or by number of inferences, for tree-like or dag-like proofs. We introduce the Monotone Minimum (Circuit) Satisfying Assignment problem and reduce it to the problems of approximation of the length of proofs.

Wiktor Tendera
Some Remarks on Lengths of Propositional Proofs (by Samuel R. Buss)

We survey the best known lower bounds on symbols and lines in Frege and extended Frege proofs. We prove that in minimum length sequent calculus proofs, no formula is generated twice or used twice on any single branch of the proof. We prove that the number of distinct subformulas in a minimum length Frege proof is linearly  bounded by the number of lines. Depth d Frege proofs of m lines can be transformed into depth d proofs of O(m^{d+1}) symbols. We show that renaming Frege proof systems are p-equivalent to extended Frege systems. Some open problems in propositional proof length and in logical flow graphs are discussed.

Marcin Zieliński
A correspondence between rooted planar maps and normal planar lambda terms (by Noam Zeilberger and Alain Giorgetti)

A rooted planar map is a connected graph embedded in the plane, with one edge marked and assigned an orientation. A term of the pure lambda calculus is said to be \beta normal if it is fully reduced, and planar if it uses all of its variables exactly once and in last-in, first-out order. We exhibit a bijection between rooted planar maps and normal planar lambda terms (with one free variable), by explaining how Tutte decomposition of rooted planar maps (into vertex maps, maps with an isthmic root, and maps with a non-isthmic root) may be naturally replayed in lambda calculus.

Krzysztof Barański

Fix a finite set S \suset GL(k, Z). Denote by a_n the number of products of matrices in S of length n that are equal to 1. We show that the sequence a_n is not always P-recursive. This answers a question of Kontsevich.

Magdalena Wiercioch
A Probabilistic Forest-to-String Model for Language Generation from Typed Lambda Calculus Expressions (by Wei Lu and Hwee Tou Ng)

This paper describes a novel probabilistic approach for generating natural language sentences from their underlying semantics in the form of typed lambda calculus. The approach is built on top of a novel reduction based weighted synchronous context free grammar formalism, which facilitates the transformation process from typed lambda calculus into natural language sentences. Sentences can then be generated based on such grammar rules with a log linear model. To acquire such grammar rules automatically in an unsupervised manner, we also propose a novel approach with a generative model, which maps from subexpressions of logical forms to word sequences in natural language sentences. Experiments on benchmark datasets for both English and Chinese generation tasks yield significant improvements over results obtained by two state of the art machine translation models, in terms of both automatic metrics and human evaluation.

Grzegorz Bukowiec
A \lambda to CL translation for strong normalization (by Yohji AKAMA)

We introduce a simple translation from \lambda-calculus to combinatory logic (CL) such that: A is an SN \lambda-term iff the translation result of A is an SN term of CL (the reductions are \beta-reduction in \lambda-calculus and weak reduction in CL). None of the conventional translations from \lambda-calculus to CL satisfy the above property. Our translation provides a simpler SN proof of Godel's \lambda-calculus by the ordinal number assignment method. By using our translation, we construct a homomorphism from a conditionally partial combinatory algebra which arises over SN \lambda-terms to a partial combinatory algebra which arises over SN CL-terms.

Grzegorz Bukowiec
A \lambda to CL translation for strong normalization (by Yohji AKAMA)

We introduce a simple translation from \lambda-calculus to combinatory logic (CL) such that: A is an SN \lambda-term iff the translation result of A is an SN term of CL (the reductions are \beta-reduction in \lambda-calculus and weak reduction in CL). None of the conventional translations from \lambda-calculus to CL satisfy the above property. Our translation provides a simpler SN proof of Godel's \lambda-calculus by the ordinal number assignment method. By using our translation, we construct a homomorphism from a conditionally partial combinatory algebra which arises over SN \lambda-terms to a partial combinatory algebra which arises over SN CL-terms.

Marcin Kostrzewa
Counting a type's prinipal inhabitants (by Broda and Damas)

We present a Counting Algorithm that computes the number of lambda-terms in \beta-normal form that have a given type as a principal type and produces a list of these terms. The design of the algorithm follows the lines of Ben-Yelles algorithm for counting normal (not neessarily principal) inhabitants of a type.

Bartłomiej Poleszak
Card-Based Protocols for Any Boolean Function (by Takuya Nishida, Yu-ichi Hayashi, Takaaki Mizuki, and Hideaki Sone )

Card-based protocols that are based on a deck of physical cards achieve secure multi-party computation with information-theoretic secrecy. Using existing AND, XOR, NOT, and copy protocols, one can naively construct a secure computation protocol for any given (multivariable) Boolean function as long as there are plenty of additional cards. However, an explicit sufficient number of cards for computing any function has not been revealed thus far. In this paper, we propose a general approach to constructing an efficient protocol so that six additional cards are sufficient for any function to be securely computed. Further, we prove that two additional cards are sufficient for any symmetric function.

Zbigniew Gołębiewski (PWr)
On the number of lambda terms with prescribed size of their De Bruijn representation

John Tromp introduced the so-called 'binary lambda calculus' as a way to encode lambda terms in terms of binary words. Later, Grygiel and Lescanne conjectured that the number of binary lambda terms with m free indices and of size n (encoded as binary words of length n) is o( n^−3/2 \tau^−n ) for \tau ≈ 1.963448 .  We generalize the proposed notion of size and show that for several classes of lambda terms, including binary lambda terms with m free indices, the number of terms of size n is \Theta ( n^−3/2 \rho^−n ) with some class dependent constant \rho, which in particular disproves the above mentioned conjecture. A way to obtain lower and upper bounds
for the constant near the leading term is presented and numerical results for a few previously introduced classes of lambda terms are given.

Maciej Poleski
On the Recursive Enumerability of Fixed-Point Combinators (by Mayer Goldberg)

We show that the set of fixed-point combinators forms a recursively enumerable subset of a larger set of terms we call non-standard fixedpoint combinators. These terms are observationally equivalent to fixedpoint combinators in any computable context, but the set of non-standard fixed-point combinators is not recursively enumerable.

Łukasz Lachowski
On the Complexity of the standard translation from Lambda Calculus to Combinatory Logic (wyniki własne)


Łukasz Lachowski
On the Complexity of the standard translation from Lambda Calculus to Combinatory Logic (wyniki własne)

We investigate the complexity of the standard translation between
terms of Lambda Calculus and Combinatory Logic. The main result
of this paper states that the asymptotic growth rate of the size of a
term produced using this translation is (n^3) in worst-case, where n
denotes size of the input term. This work is motivated by research
focused on establishing the lower bound asymptotic complexity for all
possible such translations.

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.  
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
SeminariumPI 25.03.2015
Agnieszka Łupińska
The principal Type Algorithm by Roger Hindley
One chapter from the book Basic Simple Type Theory  
SeminariumPI 11.03.2015
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.  
21.01.2015,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.  
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
SeminariumPI 12.03.2014
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.  
Ł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. 130 139]. 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.  
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", http://hal.inria.fr/inria-00555588/  
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.  

SeminariumPI 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), https://ramcloud.stanford.edu/wiki/download/attachments/11370504/raft.pdf  
Ł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.  
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.  
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.  
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).

[1] http://lampwww.epfl.ch/papers/idealhashtrees.pdf

[2] http://lampwww.epfl.ch/papers/triesearches.pdf.gz

[3] http://clojure.org/

[4] PersistentHashMap.java

[5] src/cljs/cljs/core

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 first 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.  
Agnieszka Łupińska
Optimal Stopping and Applications 4
Chapter 5. Monotone Stopping Rule Problems.  
Szymon Kałasz
Optimal Stopping and Applications 3
Paweł Wanat
Optimal Stopping and Applications 2
Chapter 4. Applications. Markov Models.  
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.  
12.10.2011,Robery Obryk
Dowodzenie w językach z typami zależnymi
Celem systemów typów w językach programowania jest ułatwianie wnioskowania o poprawności kodu. Już języki używające systemu typów Hindleya-Milnera pozwalają wnioskować w ciekawy sposób o zachowaniu funkcji na podstawie ich typu. Języki z typami zależnymi pozwalają wyrażać za pomocą typu funkcji praktycznie arbitralne warunki na jej zachowanie. Na tym seminarium poznamy formalizm typów zależnych, sposób przeprowadzania izomorfizmu Curryego-Howarda w nim i przyjrzymy się jak typy zależne pozwalają dowodzić własności programu i pomagają w dowodzeniu własności stopu w języku Agda.  
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
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
Robert Obryk
Algorithmic Information Theory , by Gregory. J. Chaitin
20.04.2011,Marek Wróbel, Adam Zydroń
Mathematics for the Analysis of Algorithms - Asymptotic Analysis
06.04.2011,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.  

09.03.2011,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.  
27.10.2010,Kasia Grygiel
Asymptotically almost all lambda terms are strongly normalizing
We present quantitative analysis of various (syntactic and behavioral) properties of random lambda terms. Our main results are that asymptotically all the terms are strongly normalizing and that any fixed closed term almost never appears in a random term. Surprisingly, in combinatory logic (the translation of the lambda calculus into combinators), the result is exactly opposite. We show that almost all terms are not strongly normalizing. This is due to the fact that any fixed combinator almost always appears in a random combinator.  
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.
10.03.2010,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
29.04.2009,Michał Klasiński
Wśród typów nie ma arystokracji
29.04.2009, Michał Klasiński
Basic Simple Type Theory
01.04.2009,Michał Handzlik
Higher-order Unificatrion and Matching
11.03.2009,Paweł Waszkiewicz
A Lazy Introduction to Goedel's Theorems
See http://www.logicmatters.net/ 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 m.in. fakt, iż w takim świecie prosta rzeczywista R jest prawdziwym continuum, tzn. nie można z niej wydzielić żadnego nietrywialnego podzbioru. (Podzbiór U wydziela się z R, jeśli dla każdego x z R albo x należy do U, albo x nie należy do U.)

Wykład przygotowałem na podstawie: J.L.Bell, A Primer on Infinitesimal Analysis, Cambridge Univ. Press, 1998. Google: ,,John L. Bell''. Warto.  
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.  
24.10.2007,Mariusz Łusiak
On learning monotone Boolean functions under the uniform distribution
We prove two general theorems on monotone Boolean functions which are useful for constructing a learning algorithm for monotone Boolean functions under the uniform distribution. The first result is that a single variable function f(x) = x­_i has the minimum correlation with majority function among all fair monotone functions. The second result is on the relationship between the influences and the average sensitivity of a monotone Boolean function. The talk is based on a paper by Kazuyuki Amano and Akira Maruoka.  
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.