Podstawy Informatyki

prof. dr hab. Marek Zaionc
dr Katarzyna Grygiel

ś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.

19.01.2022 12:15
Daniel Barczyk
Narrow Proofs May Be Maximally Long by Albert Atserias and Massimo Lauria

We prove that there are 3-CNF formulas over n variables that can be refuted in resolution in width w but require resolution proofs of size $n^{\Omega (w)}$. This shows that the simple counting argument that any formula refutable in width w must have a proof in size  $n^{O (w)}$ is essentially tight. Moreover, our lower bound generalizes to polynomial calculus resolution (PCR) and Sherali-Adams, implying that the corresponding size upper bounds in terms of degree and rank are tight as well. The lower bound does not extend all the way to Lasserre, however, since we show that there the formulas we study have proofs of constant rank and size polynomial in both n and w.


26.01.2022 12:15
Jakub Fedak
Exact enumeration of satisfiable 2-SAT formulae by Sergey Dovgal, Elie de Panafeu and Vlady Ravelomanana

We obtain exact expressions counting the satisfiable 2-SAT formulae and describe the structure of associated implication digraphs. Our approach is based on generating function manipulations. To reject the combinatorial specificities of the implication digraphs, we introduce a new kind of generating function, the Implication generating function, inspired by the Graphic generating function used in digraph enumeration. Using the underlying recurrences, we make accurate numerical predictions of the phase transition curve of the 2-SAT problem inside the critical window. We expect these exact formulae to be amenable to rigorous asymptotic analysis using complex analytic tools, leading to a more detailed picture of the 2-SAT phase transition in the future.


Previous seminars

12.01.2022 12:15
Filip Synowiec
On Zero-One and Convergence Laws for Graphs Embeddable on a Fixed Surface by Albert Atserias, Stephan Kreutzer and Marc Noy

We show that for no surface except for the plane does monadic second-order logic (MSO) have a zero-one-law – and not even a convergence law – on the class of (connected) graphs embeddable on the surface. In addition we show that every rational in [0,1] is the limiting probability of some MSO formula. This strongly refutes a conjecture by Heinig et al. (2014) who proved a convergence law for planar graphs, and a zero-one law for connected planar graphs, and also identified the so-called gaps of [0,1]: the subintervals that are not limiting probabilities of any MSO formula. The proof relies on a combination of methods from structural graph theory, especially large face-width embeddings of graphs on surfaces, analytic combinatorics, and finite model theory, and several parts of the proof may be of independent interest. In particular, we identify precisely the properties that make the zero-one law work on planar graphs but fail for every other surface.


08.12.2021 12:15
Katarzyna Król
0-1 Laws for Maps by Edward A. Bender, Kevin J. Compton,and L. Bruce Richmond

A class of fnite structures has a 0-1 law with respect to a logic if every property expressible in the logic has a probability approaching a limit of 0 or 1 as the structure size grows. To formulate 0-1 laws for maps (i.e., embeddings of graphs in a surface), it is necessary to represent maps as logical structures. Three such representations are given,
the most general being the full cross representation based on Tutte's theory of combinatorial maps. The main result says that if a class of maps has two properties, richness and large representativity, then the corresponding class of full cross representations has a 0-1 law with respect to first-order logic. As a corollary the following classes of maps
on a surface of fixed type have a first-order 0-1 law: all maps, smooth maps, 2-connected maps, 3-connected maps, triangular maps, 2-connected triangular maps, and 3-connected triangular maps


01.12.2021 12:15
Ignacy Buczek
Definability on a Random 3-CNF Formula by Albert Atserias

We consider the question of certifying unsatisfiability of random 3-CNF formulas. At which densities can we hope for a simple sufficient condition for unsatisfiability that holds almost surely? We study this question from the point of view of definability theory. The main result is that first-order logic cannot express any sufficient condition that holds almost surely on random 3-CNF formulas with $n^{2-\alpha}$ clauses, for any irrational positive number \alpha. In contrast, it can when the number of clauses is $n^{2+\alpha}$, for any positive \alpha. As an intermediate step, our proof exploits the planted distribution for 3-CNF formulas in a new technical way. Moreover, the proof requires us to extend the methods of Shelah and Spencer for proving the zero-one law for sparse random graphs to arbitrary relational languages.


24.11.2021 12:15
Michał Woźny
Dance of the Starlings by Henk Barendregt, Jorg Endrullis, Jan Willem Klop, and Johannes Waldmann

In this birdwatching paper our binoculars are focused upon a particular bird from Smullyan's enchanted forest of combinatory birds, to wit the Starling. In the feathers of lambda-calculus this bird has the plumage \abc:ac(bc). This term is usually named S, reminiscent of its inventor Schonfinkel and also the  combinatory ornithologist Smullyan. The combinator S is important for a variety of reasons. First, it is part of the S, K -basis for Combinatory Logic (CL). Second, there are several interesting questions and observations around S, mostly referring to termination and word problems. Our paper collects known facts, but poses in addition several new questions. For some of these we provide solutions, but several tough open questions remain.


17.11.2021 12:15
Łukasz Selwa
An Inverse of the Evaluation Functional for Typed λ-calculus by U. Berger and Η. Schwichtenberg
In any model of typed lambda-calculus containing some basic arithmetic, a functional p ->e (procedure —> expression) will be defined which inverts the evaluation functional for typed lambda-terms. Combined with the evaluation functional, p->e yields an efficient normalization algorithm. The method is extended to lambda-calculi with constants and is used to normalize (the lambda-representations of) natural deduction proofs of (higher order) arithmetic. A consequence of theoretical interest is a strong completeness theorem for \beta \eta-reduction, generalizing results of Friedman and Statman. If two lambda-terms have the same value in some model containing
representations of the primitive recursive functions (of level 1) then they are provably equal in the \beta \eta-calculus.
03.11.2021 12:15
Juliusz Wajgelt
On Repetitive Right Application of B-Terms by Mirai Ikebuchi and Keisuke Nakano
B-terms are built from the B combinator alone defined by B \f.\g.\x.f (g x), which is well known as a function composition operator. This paper investigates an interesting property of B-terms, that is, whether repetitive right applications of a B-term cycles or not. We discuss conditions for B-terms to have and not to have the property through a sound and complete equational axiomatization. Specifically, we give examples of B-terms which have the property and show that there are infinitely many B-terms which do not have the property. Also, we introduce a canonical representation of B-terms that is useful to detect cycles, or equivalently, to prove the property, with an efficient algorithm.
27.10.2021 12:15
Jan Kościsz
Corrado Bohm once observed that if Y is any fixed point combinator (fpc), then Y (\yx:x(yx)) is again fpc. He thus discovered the first \fpc generating scheme" a generic way to build new fpcs from old. Continuing this idea, define an fpc generator to be any sequence of terms G_1, ..., G_n such that
                               Y is fpc then Y G_1...G_n is fpc:
In this contribution, we take first steps in studying the structure of (weak) fpc generators. We isolate several robust classes of such generators, by examining their elementary properties like injectivity and (weak) constancy. We provide sufficient conditions for existence of fixed points of a given generator (G_1, ..., G_n): an fpc Y such that Y = Y G_1 ... G_n. We conjecture that weak constancy is a necessary condition for existence of such (higher-order) fixed points. This statement generalizes Statman's conjecture on non-existence of "double fpcs": fixed points of the generator (G) = (\yx:x(yx)) discovered by Bohm. Finally, we define and make a few observations about the monoid of (weak) fpc generators. This enables us to formulate new conjectures about their structure.
20.01.2021 12:15
Weronika Loreńczyk
The Fractal Dimension of SAT Formulas by Carlos Ansotegui, Maria 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 process. It is believed that these techniques exploit the underlying structure of industrial instances. However, there is not a precise definition of the notion of structure. Recently, there have been some attempts to analyze this structure in terms of complex networks, with the long-term aim of explaining the success of SAT solving techniques, and possibly improving them. We study the fractal dimension of SAT instances with the aim of complementing the model that describes the structure of industrial instances. We show that many industrial families of formulas are self-similar, with a small fractal dimension. We also show how this dimension is affected by the addition of learnt clauses during the execution of SAT solvers.
13.01.2021 12:14
Maciej Nemś
Regular Matching and Inclusion on Compressed Tree Patterns with Context Variables by Iovka Boneva, Joachim Niehren, and Momar Sakho
We study the complexity of regular matching and inclusion for compressed tree patterns extended by context variables. The addition of context variables to tree patterns permits us to properly capture compressed string patterns but also compressed patterns for unranked trees with tree and hedge variables. Regular inclusion for the latter is relevant to certain query answering on Xml streams with references.
16.12.2020 12:15
Weronika Loreńczyk - canceled
The Fractal Dimension of SAT Formulas by Carlos Ansotegui, Maria 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 process. It is believed that these techniques exploit the underlying structure of industrial instances. However, there is not a precise definition of the notion of structure. Recently, there have been some attempts to analyze this structure in terms of complex networks, with the long-term aim of explaining the success of SAT solving techniques, and possibly improving them. We study the fractal dimension of SAT instances with the aim of complementing the model that describes the structure of industrial instances. We show that many industrial families of formulas are self-similar, with a small fractal dimension. We also show how this dimension is affected by the addition of learnt clauses during the execution of SAT solvers.
09.12.2020 12:14
Katarzyna Król
A Lower Bound of the Number of Rewrite Rules Obtained by Homological Methods by Mirai Ikebuchi
It is well-known that some equational theories such as groups or boolean algebras can be defined by fewer equational axioms than the original axioms. However, it is not easy to determine if a given set of axioms is the smallest or not. Malbos and Mimram investigated a general method to find a lower bound of the cardinality of the set of equational axioms (or rewrite rules) that is equivalent to a given equational theory (or term rewriting systems), using homological algebra. Their method is an analog of Squier’s homology theory on string rewriting systems. In this paper, we develop the homology theory for term rewriting systems more and provide a better lower bound under a stronger notion of equivalence than their equivalence. The author also implemented a program to compute the lower bounds.
02.12.2020 12:14
Wojciech Węgrzynek
The repetition threshold for binary rich words by James Currie, Lucas Mol and Narad Rampersad
A word of length n is rich if it contains n nonempty palindromic factors. An infinite word is rich if all of its finite factors are rich. Baranwal and Shallit produced an infinite binary rich word with critical exponent  $2 + \Sqrt{2}/2$ ( = 2.707) and conjectured that this was the least possible critical exponent for infinite binary rich words (i.e., that the repetition threshold for binary rich words is $2 + \Sqrt{2}/2$ ). In this article, we give a structure theorem for infinite binary rich words that avoid 14/5-powers (i.e., repetitions with exponent at least 2.8). As a consequence, we deduce that the repetition threshold for binary rich words is $2 + \Sqrt{2}/2$  , as conjectured by Baranwal and Shallit. This resolves an open problem of Vesti for the binary alphabet; the problem remains open for larger alphabets.


25.11.2020 12:14
Wojtek Grabis
(Optimal) Duplication is not Elementary Recursive by Andrea Asperti, Paolo Coppola and Simone Martini
In 1998 Asperti and Mairson proved that the cost of reducing a lambda-term using an optimal lambda-reducer (a la L´evy) cannot be bound by any elementary function in the number of shared-beta steps. We prove in this paper that an analogous result holds for Lamping’s abstract algorithm. That is, there is no elementary function in the number of shared beta steps bounding the number of duplication steps of the optimal reducer. This theorem vindicates the oracle of Lamping’s algorithm as the culprit for the negative result of Asperti and Mairson. The result is obtained using as a technical tool Elementary Affine Logic.
18.11.2020 12:14
Michał Zwonek
A Confluent Rewriting System Having No Computable, One-Step, Normalizing Strategy by JAKOB GRUE SIMONSEN
A full and finitely generated Church-Rosser term rewriting system is presented that has no computable onestep, normalizing strategy; the system is both left- and right-linear. The result provides a negative answer to a question posed by Kennaway in 1989: Number 10 on the List of Open Problems in Rewriting.
04.11.2020 12:14
Przemysław Simajchel
The paper gives a broad survey of recent results in Enumerative Combinatorics and their complexity aspects.
28.10.2020 12:14
The paper gives a broad survey of recent results in Enumerative Combinatorics and their complexity aspects.
21.10.2020 12:15
Piotr Mikołajczak
Asymptotic Approximation by Regular Languages by Ryoma Sin’ya
This paper investigates a new property of formal languages called REG-measurability where REG is the class of regular languages. Intuitively, a language L is REG-measurable if there exists an infinite sequence of regular languages that “converges” to L. A language without REG-measurability has a complex shape in some sense so that it can not be (asymptotically) approximated by regular languages. We show that several context-free languages are REG-measurable (including languages with transcendental generating function and transcendental density, in particular), while a certain  simple deterministic context-free language and the set of primitive words are REG-immeasurable in a strong sense.
14.10.2020 12:15
Jędrzej Hodor
Bijective link between Chapoton’s new intervals and bipartite planar maps by Wenjie Fang
In 2006, Chapoton defined a class of Tamari intervals called “new intervals” in his enumeration of Tamari intervals, and he found that these new intervals are equienumerated with bipartite planar maps. We present here a direct bijection between these two classes of objects using a new object called “degree tree”. Our bijection also gives an intuitive proof of an unpublished equi-distribution result of some statistics on new intervals given by Chapoton and Fusy.
10.06.2020 12:15
Wojciech Grabis
Decidability of regular language genus computation by Guillaume Bonfante and Florian L. Deloup
This article continues the study of the genus of regular languages that the authors introduced in a 2013 paper (published in 2018). In order to understand further the genus g(L) of a regular language L, we introduce the genus size of |L|_gen to be the minimal size of all finite deterministic automata of genus g(L) computing L.We show that the minimal finite deterministic automaton of a regular language can be arbitrarily far away from a finite deterministic automaton realizing the minimal genus and computing the same language, in terms of both the difference of genera and the difference in size. In particular, we show that the genus size |L|gen can grow at least exponentially in size |L|. We conjecture, however, the genus of every regular language to be computable. This conjecture implies in particular that the planarity of a regular language is decidable, a question asked in 1976 by R. V. Book and A. K. Chandra. We prove here the conjecture for a fairly generic class of regular languages having no short cycles. The methods developed for the proof are used to produce new genus-based hierarchies of regular languages and in particular, we show a new family of regular languages on a two-letter alphabet having arbitrary high genus.
03.06.2020 12:15
Ruslan Yevdokymov
Learnability can be undecidable by Shai Ben-David, Pavel Hrubes, Shay Moran, Amir Shpilka and Amir Yehudayoff
The mathematical foundations of machine learning play a key role in the development of the field. They improve our understanding and provide tools for designing new learning paradigms. The advantages of mathematics, however, sometimes come with a cost. Gödel and Cohen showed, in a nutshell, that not everything is provable. Here we show that machine learning shares this fate. We describe simple scenarios where learnability cannot be proved nor refuted using the standard axioms of mathematics. Our proof is based on the fact the continuum hypothesis cannot be proved nor refuted. We show that, in some cases, a solution to the ‘estimating the maximum’ problem is equivalent to the continuum hypothesis. The main idea is to prove an equivalence between learnability and compression.
27.05.2020 12:00
Szymaon Kapała
Searching for shortest and least programs by Cristian Caludea, Sanjay Jain, Wolfgang Merkle and Frank Stephan
The Kolmogorov complexity of a string x is defined as the length of a shortest program p of x for some appropriate universal machine U, that is, U(p) =x and p is a shortest string with this property. Neither the plain nor the prefix-free version of Kolmogorov complexity are recursive but for both versions it is well-known that there are recursive exact Solovay functions, that is, recursive upper bounds for Kolmogorov complexity that are infinitely often tight. Let a coding function for a machine M be a function f such that f(x) is always a program of x for M. From the existence of exact Solovay functions it follows easily that for every universal machine there is a recursive coding function that maps infinitely many strings to a shortest program. Extending a recent line of research, in what follows it is investigated in which situations there is a coding function for some universal machine that maps infinitely many strings to the length-lexicographically least program. The main results which hold in the plain as well as in the prefix-free setting are the following. For every universal machine there is a recursive coding function that maps infinitely many strings to their least programs. There is a partial recursive coding function (defined in the natural way) for some universal machine that for every set maps infinitely many prefixes of the set to their least programs. Exactly for every set that is Bennett shallow (not deep), there is a recursive coding function for some universal machine that maps all prefixes of the set to their least programs. Differences between the plain and the prefix-free frameworks are obtained by considering effective sequences I_1, I_2, ...of mutually disjoint finite sets and asking for a recursive coding function for some universal machine that maps at least one string in each set I_n to its least code. Such coding functions do not exist in the prefix-free setting but exist in the plain setting in case the sets I_n are not too small.
20.05.2020 12:15
Piotr Mikołajczyk
Lambda Calculus and Probabilistic Computation by Claudia Faggian and Simona Ronchi della Rocca
We introduce two extensions of the lambda -calculus with a probabilistic choice operators, modeling respectively call-by-value and call-by-name probabilistic computation. We prove that both enjoys confluence and standardization, in an extended way: we revisit these two fundamental notions to take into account the asymptotic behaviour of terms. The common root of the two calculi is a further calculus based on Linear Logic ! which allows us to develop a unified, modular approach.
13.05.2020 12:15
Przemysław Simajchel
Dance of the Starlings by Henk Barendregt, Jorg Endrullis, Jan Klop and Johannes Waldmann
In this birdwatching paper our binoculars are focused upon a particular bird from Smullyan's enchanted forest of combinatory birds, to wit the Starling. In the feathers of lambda -calculus this bird has the plumage \abc:ac(bc). This term is usually named S, reminiscent of its inventor Schonfinkel and also the combinatory ornithologist Smullyan. The combinator S is important for a variety of reasons. First, it is part of the \{ S, K\} basis for Combinatory Logic (CL). Second, there are several interesting questions and observations around S, mostly referring to termination and word problems. Our paper collects known facts, but poses in addition several new questions. For some of these we provide solutions, but several tough open questions remain.
06.05.2020 12:15
Bartłomiej Puget
Evidence Normalization in System FC by Dimitrios Vytiniotis and Simon Peyton Jones
System FC is an explicitly typed language that serves as the target language for Haskell source programs. System FC is based on System F with the addition of erasable but explicit type equality proof witnesses. Equality proof witnesses are generated from type inference performed on source Haskell programs. Such witnesses may be very large objects, which causes performance degradation in later stages of compilation, and makes it hard to debug the results of type inference and subsequent program transformations. In this paper, we present an equality proof simplification algorithm, implemented in GHC, which greatly reduces the size of the target System FC programs.
29.04.2020 12:15
Jakub Dyczek
On probabilistic term rewriting by Martin Avanzinia,Ugo Dal Lago and Akihisa Yamadac
We study the termination problem for probabilistic term rewrite systems. We prove that the interpretation method is sound and complete for a strengthening of positive almost sure termination, when abstract reduction systems and term rewrite systems are considered. Two instances of the interpretation method polynomial and matrix interpretations are analyzed and shown to capture interesting and nontrivial examples when automated. We capture probabilistic computation in a novel way by means of multidistribution reduction sequences, thus accounting for both the nondeterminism in the choice of the redex and the probabilism intrinsic in firing each rule.
22.04.2020 12:15
Jan Kościsz
Fast Synchronization of Random Automata by Cyril Nicaud
A synchronizing word for an automaton is a word that brings that automaton into one and the same state, regardless of the starting position. Cerný conjectured in 1964 that if a n-state deterministic automaton has a synchronizing word, then it has a synchronizing word of length at most (n − 1)^2. Berlinkov recently made a breakthrough in the probabilistic analysis of synchronization: he proved that, for the uniform distribution on deterministic automata with n states, an automaton admits a synchronizing word with high probability. In this article, we are interested in the typical length of the smallest synchronizing word, when such a word exists: we prove that a random automaton admits a synchronizing word of length O(n log^3 n) with high probability. As a consequence, this proves that most automata satisfy the Cerný conjecture.
15.04.2020 12:15
Magdalena Proszewska
Singular value automata and approximate minimization by Borja Balle, Prakash Panangaden and Doina Precup
The present paper uses spectral theory of linear operators to construct approximately minimal realizations of weighted languages. Our new contributions are: (i) a new algorithm for the singular value decomposition (SVD) decomposition of finite-rank infinite Hankel matrices based on their representation in terms of weighted automata, (ii) a new canonical form for weighted automata arising from the SVD of its corresponding Hankelmatrix, and (iii) an algorithm to construct approximate minimizations of given weighted automata by truncating the canonical form. We give bounds on the quality of our approximation.
08.04.2020 12:15
Jacek Kurek
Complexity of translations from resolution to sequent calculus by GISELLE REIS and BRUNO PALEO
Resolution and sequent calculus are two well-known formal proof systems. Their differences make them suitable for distinct tasks. Resolution and its variants are very efficient for automated reasoning and are in fact the theoretical basis of many theorem provers. However, being intentionally machine oriented, the resolution calculus is not as natural for human beings and the input problem needs to be pre-processed to clause normal form. Sequent calculus, on the other hand, is a modular formalism that is useful for analysing meta-properties of various logics and is, therefore, popular among proof theorists. The input problem does not need to be pre-processed, and proofs are more detailed. However, proofs also tend to be larger and more verbose. When the worlds of proof theory and automated theorem proving meet, translations between resolution and sequent calculus are often necessary. In this paper, we compare three translation methods and analyse their complexity.
01.04.2020 12:15
Rafał Byczek
Bijection between oriented maps and weighted non-oriented maps by Agnieszka Czyzewska-Jankowska and Piotr Śniady
We consider bicolored maps, i.e. graphs which are drawn on surfaces, and construct a bijection between (i) oriented maps with arbitrary face structure, and (ii) (weighted) non-oriented maps with exactly one face. Above, each non oriented map is counted with a multiplicity which is based on the concept of the orientability generating series and the measure of orientability of a map. This bijection has the
remarkable property of preserving the underlying bicolored graph. Our bijection shows equivalence between two explicit formulas for the top-degree of Jack characters, i.e. (suitably normalized) coefficients in the expansion of Jack symmetric functions in the basis of power-sum symmetric functions.
25.03.2020 12:15
Michał Zwonek
FUNCTIONAL PEARL How to find a fake coin by RICHARD BIRD

The aim of this pearl is to solve the following well-known problem that appears in many puzzle books, for example Levitin & Levitin (2011) and Bellos (2016), usually for the particular case n=12.

There are n coins, all identical in appearance, one of which may be fake. The fake coin, if it exists, is either lighter or heavier than the fair coins, but it is not known which, nor by how much. Given is a balance with two pans but no weights. Equal number of coins can be placed on each pan and weighed. There are three possible outcomes: the left-hand pan may be lighter than the right-hand pan, or of equal weight, or heavier. Design a recipe for determining the minimum number of weighings guaranteed to determine the fake coin, if it exists, and whether it is lighter or heavier than the others.

18.03.2020 12:15
Mateusz Tokarz, wyniki własne, kontynuacja
The largest fixed point in iterative programs
We study the smallest ordinal number α such that every Prologue program will reach its greatest fixed point after α downward iterations. Firstly, we show that the continuity of Prologue’s resolution function does not help with this matter. Then, due to the embedding of the recursive functions in Prologue, we get that α is at least Church-Kleene Omega. Using recursive linear order presented in “On the Forms of the Predicates in the Theory of Constructive Ordinals“ (Kleene, 1944) we construct a Prologue’s program requiring at least C-K Omega steps to achieve its greatest fixed point. To get the upper bound on α we use clockable ordinals introduced in “Infinite Time Turing Machines” (Joel David Hamkins, Andy Lewis, 1998).
11.03.2020 12:15
Mateusz Tokarz wyniki własne
The largest fixed point in iterative programs
We study the smallest ordinal number α such that every Prologue program will reach its greatest fixed point after α downward iterations. Firstly, we show that the continuity of Prologue’s resolution function does not help with this matter. Then, due to the embedding of the recursive functions in Prologue, we get that α is at least Church-Kleene Omega. Using recursive linear order presented in “On the Forms of the Predicates in the Theory of Constructive Ordinals“ (Kleene, 1944) we construct a Prologue’s program requiring at least C-K Omega steps to achieve its greatest fixed point. To get the upper bound on α we use clockable ordinals introduced in “Infinite Time Turing Machines” (Joel David Hamkins, Andy Lewis, 1998).
22.01.2020 12:15
Weronika Grzybowska i Mateusz Tokarz
On two subclasses of Motzkin paths and their relation to ternary trees by Helmut Prodinger, Sarah J. Selkirk and Stephan Wagner
Two subclasses of Motzkin paths, S-Motzkin and T-Motzkin paths, are introduced. We provide bijections between S-Motzkin paths and ternary trees, S-Motzkin paths and non-crossing trees, and T-Motzkin paths and ordered pairs of ternary trees. Symbolic equations for both paths, and thus generating functions for the paths, are provided. Using these, various parameters involving the two paths are analyzed.
15.01.2020 12:15
Wojciech Grabis
Ant colony optimization theory: A survey by Marco Dorigoa and Christian Blumb
Research on a new metaheuristic for optimization is often initially focused on proof-of-concept applications. It is only after experimental work has shown the practical interest of the method that researchers try to deepen their understanding of the method’s functioning not only through more and more sophisticated experiments but also by means of an effort to build a theory. Tackling questions such as “how and why the method works’’ is important, because finding an answer may help in improving its applicability. Ant colony optimization, which was introduced in the early 1990s as a novel technique for solving hard combinatorial optimization problems, finds itself currently at this point of its life cycle. With this article we provide a survey on theoretical results on ant colony optimization. First, we reviewsome convergence results. Then we discuss relations between ant colony optimization algorithms and other approximate methods for optimization. Finally, we focus on some research efforts directed at gaining a deeper understanding of the behavior of ant colony optimization algorithms. Throughout the paper we identify some open questions with a certain interest of being solved in the near future.
08.01.2020 12:15
Piotr Gaiński
How Similar Are Two Elections by Piotr Faliszewski, Piotr Skowron, Arkadii Slinko, Stanisław Szufa and Nimrod Talmon
We introduce the ELECTION ISOMORPHISM problem and a family of its approximate variants, which we refer to as d-ISOMORPHISM DISTANCE (d-ID) problems (where d is a metric between preference orders). We show that ELECTION ISOMORPHISM is polynomial-time solvable, and that the d-ISOMORPHISM DISTANCE problems generalize various classic rank-aggregation methods (e.g., those of Kemeny and Litvak). We establish the complexity of our problems (including their inapproximability) and provide initial experiments regarding the ability to solve them in practice.
18.12.2019 12:15
Bartosz Podkanowicz
Riordan arrays and combinatorial sums by Renzo Sprugnoli
The concept of a Riordan array is used in a constructive way to find the generating function of many combinatorial sums. The generating function can then help us to obtain the closed form of the sum or its asymptotic value. Some examples of sums involving binomial coefficients and Stirling numbers are examined, together with an application of Riordan arrays to some walk problems.
11.12.2019 12:15
Mateusz Górski
A Modal Characterization Theorem for a Probabilistic Fuzzy Description Logic by Paul Wild, Lutz Schroder, Dirk Pattinson and Barbara Konig.
The fuzzy modality probably is interpreted over probabilistic type spaces by taking expected truth values. The arising probabilistic fuzzy description logic is invariant under probabilistic bisimilarity; more informatively, it is non-expansive wrt. a suitable notion of behavioural distance. In the present paper, we provide a characterization of the expressive power of this logic based on this observation: We prove a probabilistic analogue of the classical van Benthem theorem, which states that modal logic is precisely the bisimulation-invariant fragment of first-order logic. Specifically, we show that every formula in probabilistic fuzzy first-order logic that is non-expansive wrt. behavioural distance can be approximated by concepts of bounded rank in probabilistic fuzzy description logic.
04.12.2019 12:15
Michał Zwonek
Probably Half True: Probabilistic Satisfability over Lukasiewicz Infnitely-valued Logic by Marcelo Finger and Sandro Preto
We study probabilistic-logic reasoning in a context that allows for "partial truths", focusing on computational and algorithmic properties of non-classical Lukasiewicz In nitely-valued Probabilistic Logic. In particular, we study the satis ability of joint probabilistic assignments, which we call LIPSAT. Although the search space is initially in nite, we provide linear algebraic methods that guarantee polynomial  size witnesses, placing LIPSAT complexity in the NP-complete class. An exact satis ability decision algorithm is presented which employs, as a subroutine, the decision problem for Lukasiewicz In nitely-valued (non probabilistic) logic, that is also an NP-complete problem. We develop implementations of the algorithms described and discuss the empirical presence of a phase transition behavior for those implementations.
27.11.2019 12:15
Piotr Mikołajczyk
Satisfiability in Strategy Logic can be Easier than Model Checking by Erman Acar, Massimo Benerecetti and Fabio Mogavero.

In the design of complex systems, model-checking and satisfiability arise as two prominent decision problems. While
model-checking requires the designed system to be provided in advance, satisfiability allows to check if such a system even exists. With very few exceptions, the second problem turns out to be harder than the first one from a complexity-theoretic standpoint. In this paper, we investigate the connection between the two problems for a non-trivial fragment of Strategy Logic (SL, for short). SL extends LTL with first-order quantifications over strategies, thus allowing to explicitly reason about the strategic abilities of agents in a multi-agent system. Satisfiability for the full logic is known to be highly undecidable, while model-checking is non-elementary.

The SL fragment we consider is obtained by preventing strategic quantifications within the scope of temporal operators. The resulting logic is quite powerful, still allowing to express important game-theoretic properties of multi-agent systems, such as existence of Nash and immune equilibria, as well as to formalize the rational synthesis problem. We show that satisfiability for such a fragment is PSPACE-COMPLETE, while its model-checking complexity is 2EXPTIME-HARD. The result is obtained by means of an elegant encoding of the problem into the satisfiability of conjunctive-binding first-order logic, a recently discovered decidable fragment of first-order logic.

20.11.2019 12:15
Edyta Garbarz
Unifying Logical and Statistical AI Pedro by Domingos, Daniel Lowd, Stanley Kok, Aniruddh Nath, Hoifung Poon Matthew Richardson and Parag Singla
Intelligent agents must be able to handle the complexity and uncertainty of the real world. Logical AI has focused mainly on the former, and statistical AI on the latter. Markov logic combines the two by attaching weights to first-order formulas and viewing them as templates for features of Markov networks. Inference algorithms for Markov logic draw on ideas from satisfiability, Markov chain Monte Carlo and knowledge-based model construction. Learning algorithms are based on the voted perceptron, pseudo-likelihood and inductive logic programming. Markov logic has been successfully applied to a wide variety of problems in natural language understanding, vision, computational biology, social networks and others, and is the basis of the open-source Alchemy system.
13.11.2019 12:15
Jan Kościsz
Bohm's Theorem, Church's Delta, Numeral Systems, and Ershov Morphisms by Richard Statman and Henk Barendregt
In this note we work with untyped lambda terms under beta-conversion and consider the possibility of extending Bohm's theorem to infnite RE (recursively enumerable) sets. Bohm's theorem fails in general for such sets V even if it holds for all fnite subsets of it. It turns out that generalizing Bohm's theorem to infnite sets involves three other superfcially unrelated notions; namely, Church's delta, numeral systems, and Ershov morphisms. Our principal result is that Bohm's theorem holds for an infnite RE set V closed under beta conversion iff V can be endowed with the structure of a numeral system with predecessor iff there is a Church delta (conditional) for V iff every Ershov morphism with domain V can be represented by a lambda term
06.11.2019 12:15
Rafał Burczyński
Compaction of Church Numerals by Isamu Furuya and Takuya Kida
In this study, we address the problem of compaction of Church numerals. Church numerals are unary representations of natural numbers on the scheme of lambda terms. We propose a novel decomposition scheme from a given natural number into an arithmetic expression using tetration, which enables us to obtain a compact representation of lambda terms that leads to the Church numeral of the natural number. For natural number n, we prove that the size of the lambda term obtained by the proposed method is O((s log2n)^(log n/ (log log n))). Moreover, we experimentally confirmed that the proposed method outperforms binary representation of Church numerals on average, when n is less than approximately 10,000 .
30.10.2019 12:15
Jan Mełech
On compressing and indexing repetitive sequences by Sebastian Kreft and Gonzalo Navarro
We introduce LZ-End, a new member of the Lempel–Ziv family of text compressors, which achieves compression ratios close to those of LZ77 but is much faster at extracting arbitrary text substrings. We then build the first self-index based on LZ77 (or LZ-End) compression, which in addition to text extraction offers fast indexed searches on the compressed text. This self-index is particularly effective for representing highly repetitive sequence collections, which arise for example when storing versioned documents, software repositories, periodic publications, and biological sequence databases.
23.10.2019 12:15
Rafał Byczek
Suffix array and Lyndon factorization of a text by Sabrina Mantaci, Antonio Restivo, Giovanna Rosone and Marinella Sciortino
The main goal ofthis paper is to highlight the relationship between the suffix array of a text and its Lyndon factorization. It is proved in [15]that one can obtain the Lyndon factorization of a text from its suffix array. Conversely, here we show a new method for constructing the suffix array of a text that takes advantage of its Lyndon factorization. The surprising consequence of our results is that, in order to construct the suffix array, the local suffixes inside each Lyndon factor can be separately processed, allowing different implementative scenarios, such as online, external and internal memory, or parallel implementations. Based on our results, the algorithm that we propose sorts the suffixes by starting from the leftmost Lyndon factors, even if the whole text or the complete Lyndon factorization are not yet available.
16.10.2019 12:14
Maciej Nemś
Generating Random Well-Typed Featherweight Java Programs Using Quick Check by Samuel da Silva Feitosaa, Rodrigo Geraldo Ribeirob and Andre Rauber Du Bois
Currently, Java is one of the most used programming language, being adopted in many large projects, where applications reach a level of complexity for which manual testing and human inspection are not enough to guarantee quality in software development. Even when using automated unit tests, such tests rarely cover all interesting cases of code, which means that a bug could never be discovered, once the code is tested against the same set of rules over and over again. This paper addresses the problem of generating random well-typed programs in the context of Featherweight Java, a well-known object-oriented calculus, using QuickCheck, a Haskell library for property-based testing.
09.10.2019 12:15
Jacek Kurek
The halting problem is undecidable but can it be solved for "most" inputs? This natural question was considered in a number of papers, in diferent settings. We revisit their results and show that most of them can be easily proven in a natural framework of optimal machines (considered in algorithmic information theory) using the notion of Kolmogorov complexity. We also consider some related questions about this framework and about asymptotic properties of the halting problem. In particular, we show that the fraction of terminating programs cannot have a limit, and all limit points are Martin-Lof random reals. We then consider mass problems of finding an approximate solution of halting problem and probabilistic algorithms for them, proving both positive and negative results. We consider the fraction of terminating programs that require a long time for termination, and describe this fraction using the busy beaver function. We also consider approximate versions of separation problems, and revisit Schnorr's results about optimal numberings showing how they can be generalized.
05.06.2019 12:14
Szymon Stankiewicz
Bohm's Theorem, Church's Delta, Numeral Systems, and Ershov Morphisms by Richard Statman and Henk Barendregt
In this note we work with untyped lambda terms under beta-conversion and consider the possibility of extending Bohm's theorem to in¯nite RE (recursively enumerable) sets. Bohm's theorem fails in general for such sets V even if it holds for all finite subsets of it. It turns out that generalizing Bohm's theorem to infnite sets involves three other superfcially unrelated notions; namely, Church's delta, numeral systems, and Ershov morphisms. Our principal result is that Bohm's theorem holds for an infnite RE set V closed under beta conversion iff V can be endowed with the structure of a numeral system withc predecessor iff there is a Church delta (conditional) for V iff every Ershov morphism with domain V can be represented by a lambda term.
29.05.2019 12:14
Bartłomiej Puget
Solving the Rubik’s Cube Optimally is NP-complete by Erik D. Demaine and Sarah Eisenstat
In this paper, we prove that optimally solving an n × n × n Rubik’s Cube is NP-complete by reducing from the Hamiltonian Cycle problem in square grid graphs. This improves the previous result that optimally solving an n×n×n Rubik’s Cube with missing stickers is NP-complete. We prove this result first for the simpler case of the Rubik’s Square – an n × n × 1 generalization of the Rubik’s Cube – and then proceed with a similar but more complicated proof for the Rubik’s Cube case. Our results hold both when the goal is make the sides monochromatic and when the goal is to put each sticker into a specific location.
22.05.2019 12:14
Maciej Czerwiński
Automata Theoretic Account of Proof Search by Aleksy Schubert, Wil Dekkers and Henk P. Barendregt
Techniques from automata theory are developed that handle search for inhabitants in the simply typed lambda calculus. The resulting method for inhabitant search, which can be viewed as proof search by the Curry-Howard isomorphism, is proven to be adequate by a reduction of the inhabitant existence problem to the emptiness problem for appropriately defined automata. To strengthen the claim, it is demonstrated that the latter has the same complexity as the former. We also discuss the basic closure properties of the automata.
15.05.2019 12:14
Przemysław Rutka (Lublin)
Wybrane algorytmiczne zastosowania klasycznych wielomianów ortogonalnych
Klasyczne wielomiany ortogonalne, odpowiadające im klasyczne funkcje wagowe oraz ich własności znajdują wiele zastosowań w takich chociażby obszarach jak tomografia, mechanika kwantowa, kombinatoryka, przetwarzanie obrazów i sygnałów, kompresja danych oraz zwiększanie wydajności algorytmów. W tym ostatnim zakresie cały czas uzyskuje się wiele ciekawych wyników, pozwalających na efektywne numeryczne rozwiązywanie różnych problemów. Można do tych problemów w szczególności zaliczyć barycentryczne interpolacje Fejéra, Hermite'a i Lagrange'a oraz problemy ekstremalne typu Szegő i Markowa-Bernsteina. W pierwszym przypadku, gdy interpolowanych jest n wartości w węzłach, będących zerami klasycznych wielomianów ortogonalnych, możliwa jest poprawa złożoności obliczeniowej algorytmów, obliczających wartości wielomianów interpolacyjnych w oparciu o wzory barycentryczne, z O(n^2) do O(n). Wymagane jest w tym celu zastosowanie odpowiednich jawnych wzorów na wagi barycentryczne lub wzorów wiążących wagi barycentryczne z wagami i węzłami kwadratur Gaussa. Z kolei w drugim przypadku, jak się okazuje powiązanym z pierwszym, daje się sformułować wzory, pozwalające bezpośrednio obliczać na komputerze najlepsze stałe, występujące w nierównościach typu Szegő i Markowa-Bernsteina oraz wartości wielomianów ekstremalnych, dla których te nierówności stają się równościami. Nierówności te związane są z iterowanymi klasycznymi funkcjami wagowymi i można je wykorzystać do szacowania wartości lub norm pochodnych D^{k}p lub różnic progresywnych Δ^{k}p wielomianów p(x), odpowiednio w przypadku ciągłym lub dyskretnym.
     Inne tego typu rezultaty, korzystające z klasycznych wag i/lub klasycznych wielomianów ortogonalnych, można otrzymać także dla problemu typu izoperymetrycznego w klasie płaskich, zamkniętych krzywych wielomianowych, problemu równowagi elektrostatycznej układu ładunków, problemu efektywnej, stabilnej i najbardziej ekonomicznej interpolacji oraz problemu dwustronnych oszacowań aproksymacyjnych a priori typu Chernoffa.
08.05.2019 12:14
Weronika Grzybowska
A Mesh of Automata by Sabine Broda, Markus Holzer, Eva Maia, Nelma Moreira, Rogerio Reis
We contribute new relations to the taxonomy of di erent conversions from regular expressions to equivalent nite automata. In particular, we are interested in transformations that construct automata such as, the follow automaton, the partial derivative automaton, the prefix automaton, the automata based on pointed expressions recently introduced and studied, and last but not least the position, or Glushkov automaton (A_POS), and their double reversed construction counterparts. We deepen the understanding of these constructions and show that with the artefacts used to construct the Glushkov automaton one is able to capture most of them. As a byproduct we define a dual version of the position automaton which plays a similar role as A_POS but now for the reverse expression. Moreover, it turns out that the prefix automaton A_Pre is central to reverse expressions, because the determinisation of the double reversal of A_Pre (first reverse the expression, construct the automaton A_Pre, and then reverse the automaton) can be represented as a quotient of any of the considered deterministic automata that we consider in this investigation. This shows that although the conversion of regular expressions and reversal of regular expressions to nite automata seems quite similar, there are signifcant differences.
17.04.2019 12:14
Dawid Tracz
Regular Matching and Inclusion on Compressed Tree Patterns with Context Variables by Iovka Boneva, Joachim Niehren, and Momar Sakho
We study the complexity of regular matching and inclusion for compressed tree patterns extended by context variables. The addition of context variables to tree patterns permits us to properly capture compressed string patterns but also compressed patterns for unranked trees with tree and hedge variables. Regular inclusion for the latter is relevant to certain query answering on Xml streams with references.
10.04.2019 12:14
Jan Derbisz
What Percentage of Programs Halt? by Laurent Laurent Bienvenu, Damien Desfontaines and Alexander Shen
Fix an optimal Turing machine U and for each n consider the ratio \rho^U_n of the number of halting programs of length at most n by the total number of such programs. Does this quantity have a limit value? In this paper, we show that it is not the case, and further characterise the reals which can be the limsup of such a sequence \rho^U_n . We also study, for a given optimal machine U, how hard it is to approximate the domain of U from the point of view of coarse and generic computability.
20.03.2019 12:14
Rafał Byczek
Improving the Upper Bound on the Length of the Shortest Reset Words by Marek Szykula
We improve the best known upper bound on the length of the shortest reset words of synchronizing automata. The new bound is slightly better than 114n^3 / 685+O(n^2). The Cerny conjecture states that (n−1)^2 is an upper bound. So far, the best general upper bound was (n^3−n)/6−1 obtained by J.-E. Pin and P. Frankl in 1982. Despite a number of efforts, it remained unchanged for about 35 years.
To obtain the new upper bound we utilize avoiding words. A word is avoiding for a state q if after reading the word the automaton cannot be in q. We obtain upper bounds on the length of the shortest avoiding words, and using the approach of Trahtman from 2011 combined with the well-known Frankl theorem from 1982, we improve the general upper bound on the length of the shortest reset words. For all the bounds, there exist polynomial algorithms finding a word of length not exceeding the bound.
13.03.2019 12:14
Vladyslav Hlembotskyi
Upper Bounds for Standardizations and an Application by Hongwei Xi
We present a new proof for the standardization theorem in lambda-calculus, which is largely built upon a structural induction on lambda-terms. We then extract some bounds for the number of beta-reduction steps in the standard beta-reduction sequence obtained from transforming a given beta-reduction sequence, sharpening the standardization theorem. As an application, we establish a super exponential bound for the lengths of beta-reduction sequences from any given simply typed A
06.03.2019 12:14
Jan Derbisz, Pola Kyzioł, Krzysztof Maziarz, Jakub Nowak, Grzegorz Juzrdziński
Prezentacje prac magisterskich

Jan Derbisz, Promotor: dr hab. Tomasz Krawczyk
Wykorzystanie matroidów w algorytmach.

Pola Kyzioł, Promotor: dr hab. Tomasz Krawczyk
Cut & Count technique and its application to NP.-compelete graph problems that require connectivity

Krzysztof Maziarz, Promotor: prof. dr hab. Jacek Tabor
Evolutionary-Neural Hybrid Agents for Architecture Search

Jakub Nowak, Promotor: prof. dr hab. Jacek Tabor
Application of functional image representation

Grzegorz Jurdziński, Promotor: dr Piotr Micek
Głębokie sieci neuronowe w rozpoznawaniu mowy

23.01.2019 12:14

16.01.2019 12:14
Rafał Byczek i Paweł Mader
A theory of linear typings as flows on 3-valent graphs by Noam Zeilberger
Building on recently established enumerative connections between lambda calculus and the theory of embedded graphs (or “maps”), this paper develops an analogy between typing (of lambda terms) and coloring (of maps). Our starting point is the classical notion of an abelian group-valued “flow” on an abstract graph (Tutte, 1954). Typing a linear lambda term may be naturally seen as constructing a flow (on an embedded 3-valent graph with boundary) valued in a more general algebraic structure consisting of a preordered set equipped with an “implication” operation and unit satisfying composition, identity, and unit laws. Interesting questions and results from the theory of flows (such as the existence of nowhere-zero flows) may then be re-examined from the standpoint of lambda calculus and logic. For example, we give a characterization of when the local flow relations (across vertices) may be categorically lifted to a global flow relation (across the boundary), proving that this holds just in case the underlying map has the orientation of a lambda term. We also develop a basic theory of rewriting of flows that suggests topological meanings for classical completeness results in combinatory logic, and introduce a polarized notion of flow, which draws connections to the theory of proof-nets in linear logic and to bidirectional typing. 
09.01.2019 12:14
Krzysztof Turowski
Purdue University, USA
Compression of Dynamic Graphs Generated by a Duplication Model

One of the important topics in the information theory of non-sequential random data structures such as trees, sets, and graphs is the question of entropy: how many bits on average are needed to describe the structure. Here we consider dynamic graphs generated by a duplication model in which a new vertex selects an existing vertex and copies all of its neighbors. We provide asymptotic formulas for entopies for both labeled and unlabeled versions of such graphs and construct compression algorithms matching these bounds up to two bits. Moreover, as a side result, we were able to derive asymptotic expansions of expected value of f(X) for functions of polynomial growth, when X has beta-binomial distribution - which in turn allowed to obtain e.g. asymptotic formula the entropy for a Dirichlet-multinomial distribution.

19.12.2018 12:14
Jakub Łabaj i Gabriela Czarska
Programming Languages Capturing Complexity Classes by LARS KRISTIANSEN and PAUL J. VODA
We investigate an imperative and a functional programming language. The computational power of fragments of these languages induce two hierarchies of complexity classes. Our first main theorem says that these hierarchies match, level by level, a complexity-theoretic alternating space-time hierarchy known from the literature. Our second main theorems says that a slightly different complexity-theoretic hierarchy (the Goerdt-Seidl hierarchy) also can be captured by hierarchies induced by fragments of the programming languages. Well known complexity classes like LOGSPACE, LINSPACE, P, PSPACE  etc., occur in the hierarchies.
12.12.2018 12:14
Dominik Gryboś
Characterizing Polynomial and Exponential Complexity Classes in Elementary Lambda-Calculus by Patrick Baillot, Erika De Benedetti, Simona Ronchi Della Rocca
In this paper an implicit characterization of the complexity classes k-EXP and k-FEXP, for k \geq 0, is given, by a type assignment system for a stratified lambda - calculus, where types for programs are witnesses of the corresponding complexity class. Types are formulae of Elementary Linear Logic (ELL), and the hierarchy of complexity classes k-EXP is characterized by a hierarchy of types. 
05.12.2018 12:14
Bartłomiej Puget
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 beta-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 lambda terms are only necessary from order 4 onwards. 
28.11.2018 12:14
Jacek Kurek i Bruno Pitrus
The subject of enumerative combinatorics is both classical and modern. It is classical, as the basic counting questions go back millennia; yet it is modern in the use of a large variety of the latest ideas and technical tools from across many areas of mathematics. The remarkable successes from the last few decades have been widely publicized; yet they come at a price, as one wonders if there is anything left to explore. In fact, are there enumerative problems that cannot be resolved with existing technology? In this paper we present many challenges in the field from the computational complexity point of view, and describe how recent results fit into the story. 
21.11.2018 12:14
Marcin Briański
On the compressibility of finite languages and formal proofs by Sebastian Eberhard and Stefan Hetzl
We consider the minimal number of productions needed for a grammar to cover a finite language L as the grammatical complexity of L. We study this measure for several types of word and tree grammars and show that it is closely connected to well-known measures for the complexity of formal proofs in first-order predicate logic. We construct an incompressible sequence of finite word languages and transfer this and several other results about the complexity of word and tree languages to formal proofs
14.11.2018 12:14
Mateusz Tokarz
Enumerating Proofs of Positive Formulae by GILLES DOWEK AND YING JIANG
We provide a semi-grammatical description of the set of normal proofs of positive formulae in minimal predicate logic, i.e. a grammar that generates a set of schemes, from each of which we can produce a finite number of normal proofs. This method is complete in the sense that each normal proof-term of the formula is produced by some scheme generated by the grammar. As a corollary, we get a similar description of the set of normal proofs of positive formulae for a large class of theories including simple type theory and System F.
07.11.2018 12:14
Paweł Palenica
On Randomised Strategies in the λ-Calculus by Ugo Dal Lago and Gabriele Vanoni
In this work we introduce randomized reduction strategies - a notion already studied in the context of abstract reduction systems - for the lambda-calculus. We develop a simple framework that allows us to prove if a probabilistic strategy is positive almost-surely normalizing. Then we propose a simple example of probabilistic strategy for the lambda-calculus that has such a property and we show why it is non-trivial with respect to classical deterministic strategies such as leftmost-outermost or rightmostinnermost. We conclude studying this strategy for two classical sub- lambda calculi, namely those duplication and erasure are syntactically forbidden.
31.10.2018 12:14
Rafał Burczyński
A Hitchhiker’s Guide to descriptional complexity through analytic combinatorics by Sabine Broda, António Machiavelo, Nelma Moreira and Rogério Reis
Nowadays, increasing attention is being given to the study of the descriptional complexity in the average case. Although the underlying theory for such a study seems intimidating, one can obtain interesting results in this area without too much effort. In this gentle introduction we take the reader on a journey through the basic analytical tools of that theory, giving some illustrative examples using regular expressions. Additionally, new asymptotic average-case results for several $\epsilon-NFA$ constructions are presented, in a unified framework. It turns out that, asymptotically, and in the average case, the complexity gap between the several constructions is significantly larger than in the worst case. Furthermore, one of the $\epsilon-NFA$ constructions approaches the corresponding $\epsilon-free NFA$ construction, asymptotically and on average.
24.10.2018 12:14
Szymon Stankiewicz
Encoding Turing Machines into the Deterministic Lambda Calculus by Ugo Dal Lago and Beniamino Accattoli

This note is about encoding Turing machines into the lambda -calculus. The encoding we show is interesting for two reasons:

1. Weakly strategy independent : the image of the encoding is a very small fragment of the lambda - calculus, that we call the deterministic lambda -calculus det. Essentially, it is the CPS (continuation-passing style) lambda -calculus restricted to weak evaluation (i.e., not under abstractions). In det every term has at most one redex, and so all weak strategies collapse into a single deterministic evaluation strategy, because there are no choices between redexes to be made. The important consequence of this property is that every weak evaluation strategy then allows to simulate Turing machines,as well as any strong strategy reducing weak head redexes (or even only weak head redexes) first.

2. Linear overhead: the simulation is very efficient, when taking the number of beta-steps as the time cost model for the deterministic lambda -calculus. The simulation in det indeed requires a number of beta-steps that is linear in the number of transitions of the encoded Turing machine, which is the best possible overhead. Therefore, not only all weak strategies simulate Turing
machines, but they all do it efficiently.

17.10.2018 12:14
Vladyslav Hlembotskyi
Limited Automata and Regular Languages by Giovanni Pighizzini and Andrea Pisoni

Limited automata are one-tape Turing machines that are allowed to rewrite the content of any tape cell only in the first d visits, for a fixed constant d. In the case d = 1, namely, when a rewriting is possible only during the first visit to a cell, these models have the same power of finite state automata. We prove state upper and lower bounds for the conversion of 1-limited automata into finite state automata. In particular, we prove a double exponential state gap between nondeterministic 1-limited automata and one-way deterministic finite automata. The gap reduces to single exponential in the case of deterministic 1-limited automata. This also implies an exponential state gap between nondeterministic and deterministic 1-limited automata. Another consequence is that 1-limited automata can have less states than equivalent two-way nondeterministic finite automata. We show that this is true even if we restrict to the case of the one-letter input alphabet. For each d \geq 2, d-limited automata are known to characterize the class of context-free languages. Using the Chomsky-Schutzenberger representation for context-free languages,
we present a new conversion from context-free languages into 2-limited automata.


10.10.2018 12:14
Michał Zieliński
Lambda Theories allowing Terms with a Finite Number of Fixed Points by BENEDETTO INTRIGILA and RICHARD STATMAN
A natural question in the lambda calculus asks what is the possible number of fixed points of a combinator (closed term). A complete answer to this question is still missing (Problem 25 of TLCA Open Problems List) and we investigate the related question about the number of fixed points of a combinator in lambda-theories. We show the existence of a recursively enumerable lambda theory where the number is always one or infinite. We also show that there are lambda-theories such that some terms have only two fixed points. In a first example, this is obtained by means of a non-constructive (more precisely non-r.e.) lambda-theory where the range property is violated. A second, more complex example of a non-r.e. Lambda-theory (with a higher unsolvability degree) shows that some terms can have only two fixed points while the range property holds for every term.
03.10.2018 12:14
Jarosław Duda
Instytut Informatyki UJ
Krótkie wprowadzenie do ANS, MERW i pól Markova
Na seminarium spróbuję zainteresować kilkoma z tematów, którymi się zajmowałem, np. kodowaniem Asymmetric Numeral Systems, które jest obecnie używane w produktach m.in. Apple, Facebook, Google. Opowiem też o Maximal Entropy Random Walk, czyli jak optymalnie wybierać błądzenie przypadkowe na grafie - z perspektywy zastosowań m.in. do maksymalizacji ilości przechowywanej informacji, zrozumienia i naprawienia rozbieżności między dyfuzją a mechaniką kwantową, analizy obrazów, sieci społecznych, czy rekonstrukcji traktów nerwowych. Tematem łączącym powyższe będą pola Markova, czyli wielowymiarowe uogólnienie procesów Markova, o których też krótko opowiem z przykładem zastosowania do poprawienia pojemności dysków twardych. Slajdy do seminarium można znaleźć na: http://tiny.cc/2jpiyy
13.06.2018 12:14
Marcin Briański

A coarse description of a set A \subset \omega  is a set D \subset \omega such that the symmetric difference of A and D has asymptotic density 0. We study the extent to which noncomputable information can be effectively recovered from all coarse descriptions of a given set A, especially when A is effectively random in some sense. We show that if A is 1-random and B is computable from every coarse description D of A, then B is K-trivial, which implies that if A is in fact weakly 2-random then B is computable. Our main tool is a kind of compactness theorem for cone-avoiding descriptions, which also allows us to prove the same result for 1- genericity in place of weak 2-randomness. In the other direction, we show that if A \leq_T \emptyset is a 1-random set, then there is a noncomputable c.e. set computable from every coarse description of A, but that not all K-trivial sets are computable from every coarse description of some 1-random set.


06.06.2018 12:14
Bruno Pitrus
Linear lambda terms as invariants of rooted trivalent maps by Noam Zeilberger

The main aim of the article is to give a simple and conceptual account for the correspondence (originally described by Bodini, Gardy, and Jacquot) between \alpha equivalence classes of closed linear lambda terms and isomorphism classes of rooted trivalent maps on compact oriented surfaces without boundary, as an instance of a more general correspondence between linear lambda terms with a context of free variables and rooted trivalent maps with a boundary of free edges. We begin by recalling a familiar diagrammatic representation for linear lambda terms, while at the same time explaining how such diagrams may be read formally as a notation for endomorphisms of a reflexive object in a symmetric monoidal closed (bi)category. From there, the “easy” direction of the correspondence is a simple forgetful operation which erases annotations on the diagram of a linear lambda term to produce a rooted trivalent map. The other direction views linear lambda terms as complete invariants of their underlying rooted trivalent maps, reconstructing the missing information through a Tutte-style topological recurrence on maps with free edges. As an application in combinatorics, we use this analysis to enumerate bridgeless rooted trivalent maps as linear lambda terms containing no closed proper subterms, and conclude by giving a natural reformulation of the Four Color Theorem as a statement about typing in lambda calculus.



30.05.2018 12:14
Bartłomiej Puget

In the Simply Typed lambda calculus Statman investigates the reducibility relation between types: for types freely generated using \arrow and a single ground type 0, define A \leq B if there exists a lambda definable injection from the closed terms of type A into those of type B. Unexpectedly, the induced partial order is the (linear) well-ordering (of order type) \omega + 4.


23.05.2018 12:14

16.05.2018 12:14
Maciej Czerwiński
On Type Inference in the Intersection Type Discipline by Gerard Boudol and Pascal Zimmer
We introduce a new unification procedure for the type inference problem in the intersection type discipline. We show that unification exactly corresponds to reduction in an extended  lambda calculus, where one never erases arguments that would be discarded by ordinary β-reduction. We show that our notion of unification allows us to compute a principal typing for any strongly normalizing lambda expression.
09.05.2018 12:14
Dominika Salawa
The Hiring Problem and Permutations by Margaret Archibald and Conrado Martínez

The hiring problem has been recently introduced by Broder et al. in last year’s ACM-SIAM Symp. on Discrete Algorithms (SODA 2008), as a simple model for decision making under uncertainty. Candidates are interviewed in a sequential fashion, each one endowed with a quality score, and decisions to hire or discard them must be taken on the fly. The goal is to maintain a good rate of hiring while improving the “average” quality of the hired staff. We provide here an alternative formulation of the hiring problem in combinatorial terms. This combinatorial model allows us the systematic use of techniques from combinatorial analysis, e. g., generating functions, to study the problem.

25.04.2018 12:00
Rafał Burczyński
How to select a loser
Consider the following game: everyone from a group of n people flips a coin with result either 0 or 1, both equally probable; if no one gets a 0, the round is repeated, otherwise people with 1's are considered "winners" and the game continues only with participants who got 0's. The process continues until there is one person left, who is called "loser". We can picture this process as a binary tree and analyze some of its properties in average case. The analysis is not completely trivial, in particular one may find application for tools such as Mellin transform.
18.04.2018 12:00
Rafał Burczyński
Mellin transforms and asymptotics
We will introduce Mellin transform, which may be used for the asymptotic analysis of a particular class of sums. I will start with basic properties and then present fundamental correspondence between the asymptotic expansion of a function at 0 or infinity and singularities of its transform. Finally we will show some combinatorial applications of the transform.
11.04.2018 12:14
Weronika Grzybowska
Average complexity of Moore’s and Hopcroft’s algorithms by Julien David
In this paper we prove that for the uniform distribution on complete deterministic automata, the average time complexity of Moore’s state minimization algorithm is O(n log (log n)),  where n is the number of states in the input automata and the number of letters in the alphabet is fixed. Then, an unusual family of implementations of Hopcroft’s algorithm is characterized, for which the algorithm will be proved to be always faster than Moore’s algorithm. Finally, we present experimental results on the usual implementations of Hopcroft’s algorithm.
04.04.2018 12:14
Vladyslav Hlembotskyi
A graph theoretic approach to automata minimality by Antonio Restivo and Roberto Vaglica
The paper presents a graph-theoretic approach to test the minimality of a deterministic automaton. In particular, we focus on problems concerning the dependence of the minimality of an automaton on the choice of the set F of final states or on the cardinality of the set F . We introduce different minimality conditions of an automaton and show that such conditions can be characterized in graph-theoretic terms.
28.03.2018 12:00
Szymon Stankiewicz
Introduction to Higher-Order Categorical Logic - continuation
21.03.2018 12:00
Szymon Stankiewicz
Introduction to Higher-Order Categorical Logic by Lambec and Scott
14.03.2018 12:14
Dawid Pyczek i Jakub Rówiński
Asymptotic Density and the Theory of Computability by CARL JOCKUSCH AND PAUL SCHUPP
The purpose of this paper is to survey recent work on how classical asymptotic density interacts with the theory of computability. We have tried to make the survey accessible to those who are not specialists in computability theory and we mainly state results without proof, but we include a few
easy proofs to illustrate the flavor of the subject. In complexity theory, classes such as P and NP are defined by using worst-case measures. That is, a problem belongs to the class if there is an algorithm solving it which has a suitable bound on its running time over all instances of the problem. Similarly, in computability theory, a problem is classified as computable if there is a single algorithm which solves all instances of the given problem. There is now a general awareness that worst-case measures may not give a good picture of a particular algorithm or problem since hard instances may be very sparse. The paradigm case is Dantzig’s Simplex Algorithm for linear programming problems. This algorithm runs many hundreds of times every day for scheduling and transportation problems, almost always very quickly. There are clever examples of Klee and Minty showing that there exist instances for which the Simplex Algorithm must take exponential time, but such examples are not encountered in practice. Observations of this type led to the development of average-case complexity by Gurevich and by Levin independently. There are different approaches to the average-case complexity, but they all involve computing the expected value of the running time of an algorithm with respect to some measure on the set of inputs. Thus the problem must be decidable and one still needs to know the worst-case complexity. Another example of hard instances being sparse is the behavior of algorithms for decision problems in group theory used in computer algebra packages. There is often some kind of an easy “fast check” algorithm which quickly produces a solution for “most” inputs of the problem. This is true even if the worst-case complexity of the particular problem is very high or the problem is even unsolvable. Thus many group-theoretic decision problems have a very large set of inputs where the (usually negative) answer can be obtained easily and quickly.
20.06.2018 12:15
Wojciech Szpankowski
Purdue University USA
Analytic Information Theory: From Shannon to Knuth and Back
07.03.2018 12:14
Jarosław Duda
Instytut Informatyki UJ
Some nonstandard approaches to hard computational problems

I will talk about nonstandard approaches to some problems for which there is not known polynomial time classical algorithm.  I will start with briefly explaining mechanism used in Shor algorithm, compressed sensing, and the problem with global optimization formulations used in adiabatic
quantum computers. Then show some perspectives on the subset-sum NP complete problem, like geometric, integration and divergence formulations. Then show how Grassmann variables would be useful for the Hamilton cycle problem.  Finally discuss the difficulty of the graph isomorphism problem
on the most problematic cases: strongly regular graphs, geometric perspective on this problem, and some new approach to rotation invariants for this purpose.


Slides: https://tinyurl.com/y74nx2t6

17.01.2018 12:00
Bartłomiej Puget i Dominika Salawa
Chapters 8.5 - 8.9 of AN INTRODUCTION TO THE ANALYSIS OF ALGORITHMS by Robert Sedgewick, Philippe Flajolet
10.01.2018 12:00
Kamil Rajtar
Chapters 8.1 - 8.4 of AN INTRODUCTION TO THE ANALYSIS OF ALGORITHMS by Robert Sedgewick, Philippe Flajolet
03.01.2018 12:00
Dawid Pyczek i Jakub Rowiński
Chapters 7.6 - 7.9 of AN INTRODUCTION TO THE ANALYSIS OF ALGORITHMS by Robert Sedgewick, Philippe Flajolet
20.12.2017 12:00
Rafał Burczyński
Chapters 7.1 - 7.5 of AN INTRODUCTION TO THE ANALYSIS OF ALGORITHMS by Robert Sedgewick, Philippe Flajolet
13.12.2017 12:00
Katarzyna Grzybowska
Chapters 6.12 - 6.15 of AN INTRODUCTION TO THE ANALYSIS OF ALGORITHMS by Robert Sedgewick, Philippe Flajolet
06.12.2017 12:00
Katarzyna Bułat
Chapter 6.8 - 6.11 of AN INTRODUCTION TO THE ANALYSIS OF ALGORITHMS by Robert Sedgewick, Philippe Flajolet
29.11.2017 12:00
Filip Bartodziej
Chapter 6.1 - 6.7 of AN INTRODUCTION TO THE ANALYSIS OF ALGORITHMS by Robert Sedgewick, Philippe Flajolet
22.11.2017 12:00
Michał Ziobro
Chapter 5 of AN INTRODUCTION TO THE ANALYSIS OF ALGORITHMS by Robert Sedgewick, Philippe Flajolet
15.11.2017 12:00
Hanna Palianytsia i Agnieszka Rabiej
Chapter 4.5 - 4.9 of AN INTRODUCTION TO THE ANALYSIS OF ALGORITHMS by Robert Sedgewick, Philippe Flajolet
08.11.2017 12:00
Miron Ficek
Chapter 4 of AN INTRODUCTION TO THE ANALYSIS OF ALGORITHMS by Robert Sedgewick, Philippe Flajolet
25.10.2017 12:00
Jakub Czarnowicz
Chapter 3 of AN INTRODUCTION TO THE ANALYSIS OF ALGORITHMS by Robert Sedgewick, Philippe Flajolet
18.10.2017 12:00
Piotr Wójcik
Chapter 4 of Flajolet book "Complex Analysis, Rational and Meromorphic Asymptotic".
11.10.2017 12:00
Tomasz Kisielewski
Logic of Provability by George Boolosa
Short presentantion of the book Logic of Provability by George Boolos.
04.10.2017 12:15
Tomasz Kisielewski
Logic of Provability by George Boolosa

Short presentantion of the book Logic of Provability by George Boolos.


07.06.2017 12:15
Jakub Nowak
Generic Complexity of Presburger Arithmetic by Alexander N. Rybalov
Fischer and Rabin proved in that the decision problem for Presburger Arithmetic has at least double exponential worst-case complexity (for deterministic and nondeterministic Turing machines). In paper 4  a theory of generic-case complexity was developed, where algorithmic problems are studied on "most" inputs instead of set of all inputs. An interesting question rises about existing of more efcient (say, polynomial) generic algorithm deciding Presburger Arithmetic on some set of closed formulas of
asymptotic density 1 (so-called generic set). We prove, however, that there is not even an exponential generic algorithm working correctly on a set of inputs which (so-called strongly generic set).
31.05.2017 12:15
Grzegorz Bukowiec
The Undecidability of the Generalized Collatz Problem by Stuart A. Kurtz and Janos Simon
The Collatz problem, widely known as the 3x + 1 problem, asks whether or not a certain simple iterative process halts on all inputs. In this paper, we build on work of J. H. Conway to show that a natural generalization of the Collatz problem is $PI^0_2$ complete.
24.05.2017 12:15
Piotr Wójcik
Random-bit optimal uniform sampling for rooted planar trees with given sequence of degrees and Applications by O.Bodini, J. David, and Ph. Marchal
In this paper, we redesign and simplify an algorithm due to Remy et al. for the generation of rooted planar trees that satisfies a given partition of degrees. This new version is now optimal in terms of
random bit complexity, up to a multiplicative constant. We then apply a natural process “simulate-guess-and-proof” to analyze the height of a random Motzkin in function of its frequency of unary nodes. When the number of unary nodes dominates, we prove some unconventional height
10.05.2017 12:15
Maciej Bendkowski
Analytic combinatorics: an introduction
In our talk we outline the main concepts and techniques of analytic combinatorics used to investigate properties of large random algebraic structures. We discuss the central interpretation of generating functions as functions analytic at the origin allowing to relate their analytic properties with the quantitative properties of studied structures. Finally, we briefly excerpt the techniques of singularity analysis allowing us to access the asymptotic form of corresponding counting sequences or investigate the probability distribution of interesting combinatorial parameters.
26.04.2017 12:15
Konrad Kalita
Java Generics are Turing Complete by Radu Grigore
This paper describes a reduction from the halting problem of Turing machines to subtype checking in Java. It follows that subtype checking in Java is undecidable, which answers a question posed by
Kennedy and Pierce in 2007. It also follows that Java’s type checker can recognize any recursive language, which improves a result of Gil and Levy from 2016. The latter point is illustrated by a parser
generator for fluent interfaces.
12.04.2017 12:15
Jarek Duda
Boundaries for hashing problem, or how many bits ones individuality costs
I will talk about information-theoretic boundaries for the hashing problem, the Bloom filter, and generally about informational content of structures like trees and graphs. While the label size has to grow like logarithm of the population size, neglecting information about the order (lg(n!) bits), we get a linear growth of entropy of population, allowing to bound 'the cost of individuality' asymptotically to ~2.33275 bits per object.
05.04.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.

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.