View: session overviewtalk overview

09:00 | Quantitative semantics of the lambda calculus: some generalisations of the relational model SPEAKER: Luke Ong ABSTRACT. We present an overview of some recent work on the quantitative semantics of the λ-calculus. Our starting point is the fundamental degenerate model of linear logic, the |

10:30 | Constructive completeness for the linear-time mu-calculus SPEAKER: Amina Doumane ABSTRACT. Modal mu-calculus is one of the central logics for verification. In his seminal paper, Kozen proposed an axiomatization for this logic, which was proved to be complete, 13 years later, by Kaivola for the linear-time case and by Walukiewicz for the branching-time one. These proofs are based on complex, non-constructive arguments, yielding no reasonable algorithm to construct proofs for valid formulas. The problematic of constructiveness becomes central when we consider proofs as certificates, supporting the answers of verification tools. In our paper, we provide a new completeness argument for the linear-time mu-calculus which is constructive, i.e. it builds a proof for every valid formula. To achieve this, we decompose this difficult problem into several easier ones, taking advantage of the correspondence between the mu-calculus and automata theory. More precisely, we lift the well-known automata transformations (non-determinization for instance) to the logical level. To solve each of these smaller problems, we perform first a proof-search in a circular proof system, then we transform the obtained circular proofs into proofs in Kozen's axiomatization. This yields a constructive proof for the full linear-time mu-calculus. |

10:55 | Generalised Species of Rigid Resource Terms SPEAKER: unknown ABSTRACT. This paper introduces a variant of the resource calculus, the rigid resource calculus, in which a permutation of elements in a bag is distinct from but isomorphic to the original bag. It is designed so that the Taylor expansion within it coincides with the interpretation by generalised species of Fiore et al., which is a common generalisation of Girard’s normal functor and Joyal’s combinatorial species, and. As an application, we prove the commutation between computing B¨ohm trees and (standard) Taylor expansions for a particular nondeterministic calculus. |

11:20 | Infinitary Intersection Types as Sequences: a New Answer to Klop’s Problem SPEAKER: Pierre Vial ABSTRACT. We provide a type-theoretical characterization of weakly-normalizing terms in an infinitary lambda-calculus. We adapt for this purpose the standard quantitative (with non-idempotent intersections) type assignment system of the lambda-calculus to our infinite calculus. Our work provides a positive answer to a semi-open question known as Klop’s Problem, namely, finding out if there is a type system characterizing the hereditary head normalizing (HHN) lambda-terms. Tatsuta showed in 2007 that HHN could not be characterized by a finite type system. We prove that an infinitary type system endowed with a validity condition called approximability can achieve it. As it turns out, approximability cannot be expressed when intersection is represented by means of multisets. Multisets are then replaced coinductively by sequences of integers, thus defining a type system called System S. |

11:45 | Gödel Logic: From Natural Deduction to Parallel Computation SPEAKER: unknown ABSTRACT. Propositional Gödel logic G extends intuitionistic logic with the non-constructive principle of linearity (A->B) v (B->A). We introduce a Curry–Howard correspondence for G and show that a simple natural deduction calculus can be used as a typing system. The resulting functional language extends the simply typed λ-calculus via a syncronous communication mechanism between parallel processes, which increases its expressive power. The normalization proof employs original termination arguments and proof transformations implementing forms of code mobility. Our results provide a computational interpretation of G, thus proving A. Avron’s 1991 thesis. |

13:40 | The Weisfeiler-Leman dimension of planar graphs is at most 3 SPEAKER: unknown ABSTRACT. We prove that the Weisfeiler-Leman (WL) dimension of the class of all finite planar graphs is at most~$3$. In particular, every finite planar graph is definable in fixed-point logic with counting using at most~$4$ variables. The previously best known upper bounds for the dimension and number of variables were~$14$ and~$15$, respectively. First we show that, for dimension 3 and higher, the WL-algorithm correctly tests isomorphism of graphs in a minor-closed class whenever it determines the orbits of the automorphism group of any vertex-/arc-colored $3$-connected graph belonging to this class. Then we prove that, apart from several exceptional graphs (which have WL-dimension at most 2), the individualization of two correctly chosen vertices of a colored 3-connected planar graph followed by the 1-dimensional WL-algorithm produces the discrete vertex partition. This implies that the 3-dimensional WL-algorithm determines the orbits of a colored $3$-connected planar graph. As a byproduct of the proof, we get a classification of the 3-connected planar graphs with fixing number~$3$. |

14:05 | Uniform, Integral and Efficient Proofs for the Determinant Identities SPEAKER: unknown ABSTRACT. We give a uniform and integral version of the short propositional proofs for the determinant identities demonstrated over GF(2) in Hrubes-Tzameret [HT15]. Specifically, we show that the multiplicativity of the determinant function over the integers is provable in the bounded arithmetic theory VNC^2, which is a first-order theory corresponding to the complexity class NC2. This also establishes the existence of uniform polynomial-size and O(log^2 n)-depth Circuit-Frege (equivalently, Extended Frege) proofs over the integers, of the basic determinant identities (previous proofs hold only over GF(2)). In doing so, we give uniform NC2 algorithms for homogenizing algebraic circuits, balancing algebraic circuits (given as input an upper bound on the syntactic-degree of the circuit), and converting circuits with divisions into circuits with a single division gate—all (Σ^B_1-) definable in VNC2. This also implies a Σ^B_1-definable in VNC2 parallel algorithm for evaluating algebraic circuits of any depth. |

14:30 | Model-checking for successor-invariant first-order formulas on graph classes of bounded expansion SPEAKER: unknown ABSTRACT. A successor-invariant first-order formula is a formula that has access to an auxiliary successor relation on a structure's universe, but the model relation is independent of the particular interpretation of this relation. It is well known that successor-invariant formulas are more expressive on finite structures than plain first-order formulas without a successor relation. This naturally raises the question whether this increase in expressive power comes at an extra cost to solve the model-checking problem, that is, the problem to decide whether a given structure together with some (and hence every) successor relation is a model of a given formula. It was shown earlier that adding successor-invariance to first-order logic essentially comes at no extra cost for the model-checking problem on classes of finite structures whose underlying Gaifman graph is planar (Engelmann et al 2012), excludes a fixed minor (Eickmeyer et al 2013) or a fixed topological minor (Eickmeyer et al 2016, Kreutzer et al 2016). In this work we show that the model-checking problem for successor-invariant formulas is fixed-parameter tractable on any class of finite structures whose underlying Gaifman graphs form a class of bounded expansion. Our result generalizes all earlier results and comes close to the best tractability results on nowhere dense classes of graphs currently known for plain first-order logic. |

14:55 | A fine-grained hierarchy of hard problems in the separated fragment SPEAKER: Marco Voigt ABSTRACT. Recently, the separated fragment (SF) has been introduced and proved to be decidable [1]. Its defining principle is that universally and existentially quantified variables may not occur together in atoms. The known upper bound on the time required to decide SF's satisfiability problem is formulated in terms of quantifier alternations: Given an SF sentence $\exists z \forall x_1 \exists y_1 \ldots \forall x_n \exists y_n. \psi$ in which $\psi$ is quantifier free and the $z$, $x_i$, and $y_i$ stand for tuples of variables, satisfiability can be decided in nondeterministic $n$-fold exponential time. In the present paper, we conduct a more fine-grained analysis of the complexity of SF-satisfiability. We derive an upper and a lower bound in terms of the degree of interaction of existential variables (short: degree) --- a novel measure of how many separate existential quantifier blocks in a sentence are connected via joint occurrences of variables in atoms. Our main result is the $k$-NEXPTIME-completeness of the satisfiability problem for the set of all SF sentences that have degree $k$ or smaller. Consequently, we show that SF-satisfiability is non-elementary in general, since SF is defined without restrictions on the degree. Beyond trivial lower bounds, nothing has been known about the hardness of SF-satisfiability so far. [1] T. Sturm, M. Voigt, C. Weidenbach. Deciding First-Order Satisfiability when Universal and Existential Variables are Separated. In Logic in Computer Science (LICS'16), pages 86--95, 2016. |

15:50 | Foundations of Information Integration under Bag Semantics SPEAKER: unknown ABSTRACT. During the past several decades, the database theory community has successfully investigated several different facets of the principles of database systems, including the development of various data models, the systematic exploration of the expressive power of database query languages, and, more recently, the study of the foundations of information integration via schema mappings. For the most part, all these investigations have been carried out under set semantics. that is, both the database relations and the answers to database queries are sets. In contrast, SQL deploys bag (multiset) semantics and, as a result, theory and practice diverge at this crucial point. Our main goal in this paper is to embark on the development of the foundations of information integration under bag semantics, thus taking the first step towards bridging the gap between theory and practice in this area. Our first contribution is conceptual, namely, we give rigorous bag semantics to GLAV mappings and to the certain answers of conjunctive queries in the context of data exchange and data integration. In fact, we introduce and explore two different versions of bag semantics that, intuitively, correspond to the maximum-based union of bags and to the sum-based union of bags. After this, we establish a number of technical results, including results about the computational complexity of the certain answers of conjunctive queries under bag semantics and about the existence and computation of universal solutions under these two versions of bag semantics. Our results reveal that the adoption of more realistic semantics comes at a price, namely, algorithmic problems in data exchange and data integration that were tractable under set semantics become intractable under bag semantics. |

16:15 | The Logic of Counting Query Answers SPEAKER: unknown ABSTRACT. We consider the problem of counting the number of answers to a first-order formula on a finite structure. We present and study an extension of first-order logic in which algorithms for this counting problem can be naturally and conveniently expressed, in senses that are made precise and that are motivated by the wish to understand tractable cases of the counting problem. |

16:40 | Understanding the complexity of #SAT using knowledge compilation SPEAKER: Florent Capelli ABSTRACT. Two main techniques have been used so far to solve the #P-hard problem #SAT. The first one, used in practice, is based on an extension of DPLL for model counting called exhaustive DPLL. The second approach, more theoretical, exploits the structure of the input to compute the number of satisfying assignments by usually using a dynamic programming scheme on a decomposition of the formula. In this paper, we make a first step toward the separation of these two techniques by exhibiting a family of formulas that can be solved in polynomial time with the first technique but needs an exponential time with the second one. We show this by observing that both techniques implicitly construct a very specific boolean circuit equivalent to the input formula. We then show that every beta-acyclic formula can be represented by a polynomial size circuit corresponding to the first method and exhibit a family of beta-acyclic formulas which cannot be represented by polynomial size circuits corresponding to the second method. This result shed a new light on the complexity of #SAT and related problems on beta-acyclic formulas. As a byproduct, we give new handy tools to design algorithms on beta-acyclic hypergraphs. |

17:05 | Untwisting two-way transducers in elementary time SPEAKER: unknown ABSTRACT. Functional transductions realized by two-way transducers (equivalently, by streaming transducers and by MSO transductions) are the natural and standard notion of “regular“ mappings from words to words. It was shown recently (LICS'13) that it is decidable if such a transduction can be implemented by some one-way transducer, but the given algorithm has non-elementary complexity. We provide an algorithm of different flavor solving the above question, that has double exponential space complexity. We further apply our technique to decide whether the transduction realized by a two-way transducer can be implemented by a sweeping transducer, with either known or unknown number of passes. |

15:50 | Unrestricted Stone Duality for Markov Processes SPEAKER: unknown ABSTRACT. Stone duality relates logic, in the form of Boolean algebra, to spaces, and has been of great use in the study of modal logics. In previous work, the first four authors defined a Stone duality for a restricted class of Markov processes, in terms of a family of modal operators. The dual category was a new notion -- Aumann algebras -- which were defined to be Boolean algebras equipped with probabilistic modalities. In this article we change the definition of Aumann algebra in such a way that we can define a dual adjunction for Markov processes that is a duality for many measurable spaces occurring in practice. This extends a duality for measurable spaces due to Sikorski. In particular, we do not require that the probabilistic modalities preserve a chosen base of clopen sets, nor that morphisms of Markov processes do so. The extra generality allows us to give a perspicuous definition of event bisimulation on Aumann algebras. |

16:15 | Quantifiers on languages and codensity monads SPEAKER: unknown ABSTRACT. In this work we are interested in extending the tools of algebraic automata theory beyond the setting of regular languages, motivated by problems in Boolean circuit classes. The appropriate classes of languages on words can be described either as model classes of fragments of first- and higher-order logics, or via the properties of their topo-algebraic recognisers. The link between the two approaches is the existence of constructions on recognisers which correspond to the application of a quantifier on the logical side. In the setting of regular languages, two-sided semidirect products for topological monoids provide a flexible tool which yields recognisers corresponding to a wide variety of quantifiers such a existential and modular quantifiers. The recognisers of interest for regular languages are profinite monoids. Using Stone duality it has been shown that the appropriate generalisation in the study of non-regular languages are so-called Boolean spaces with internal monoids. In our recent work it was shown that a certain construction on Boolean spaces with internal monoids, which is similar to Schützenberger products of monoids and is based the Vietoris construction for Boolean spaces, corresponds to the application of the existential quantifier. In this paper we start from the observation that the Vietoris monad on Boolean spaces involved in this construction is the codensity monad for the functor mapping a finite join semilattice to the discrete Boolean space on its carrier set. We apply a category theoretic approach to systematically obtain constructions for Boolean spaces with internal monoids which correspond to the application of a wide class of operations on arbitrary languages, including existential and modular quantifiers. In the process we show, among other, that any finitary commutative monad on the category of sets can be extended in a canonical way to the category of Boolean spaces with internal monoids. Quantifiers such as the modular ones are obtained by instantiating this result to the free semimodule over a finite commutative semiring monad. In this case, we apply duality theoretic tools to obtain an intrinsic description of the extended monad which has a measure-theoretic flavour. |

16:40 | Riesz Modal Logic for Markov Processes SPEAKER: unknown ABSTRACT. We investigate a modal logic for expressing properties of Markov processes whose semantics is real-valued, rather than Boolean, and based on the mathematical theory of Riesz spaces. We use the duality theory of Riesz spaces to provide a junction between Markov processes and the logic. This takes the form of a duality between the category of coalgebras of the Radon monad (modeling Markov processes) and the category of a new class of algebras (algebraizing the logic) which we call modal Riesz spaces. As a result, we obtain a sound and complete axiomatization of the Riesz Modal logic. |

17:05 | Dual-Context Calculi for Modal Logic SPEAKER: G. A. Kavvos ABSTRACT. We show how to derive natural deduction systems for the necessity fragment of various constructive modal logics by exploiting a pattern found in sequent calculi. The resulting systems are dual-context systems, in the style pioneered by Girard, Barber, Plotkin, Pfenning, Davies, and others. This amounts to a full extension of the Curry-Howard-Lambek correspondence to the necessity fragments of a constructive variant of the modal logics \textsf{K}, \textsf{K4}, \textsf{GL}, \textsf{T}, and \textsf{S4}. We investigate the metatheory of these calculi, as well as their categorical semantics. Finally, we speculate on their computational interpretation. |