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 relational model MRel. We show that three quantitative semantics of the simply- typed λ-calculus are equivalent: the relational semantics, HO/N game semantics, and the Taylor expansion semantics. We then consider two recent generalisations of the relational model: first, R-weighted relational models where R is a complete commutative semiring, as studied by Laird et al.; secondly, generalised species of structures, as introduced by Fiore et al. In each case, we briefly discuss some applications to quantitative analysis of higher-order programs.

ABSTRACT. Data vectors generalise finite multisets: they are finitely supported functions into a commutative monoid. We study the question if a given data vector can be expressed as a finite sum of others, only assuming that 1) the domain is countable and 2) the given set of base vectors is finite up to permutations of the domain.

Based on a succinct representation of the involved permutations as integer linear constraints, we derive that positive instances can be witnessed in a bounded subset of the domain.

For data vectors over a group we moreover study when a data vector is reversible, that is, if its inverse is expressible using only nonnegative coefficients. We show that if all base vectors are reversible then the expressibility problem reduces to checking membership in finitely generated subgroups. Moreover, checking reversibility also reduces to such membership tests.

These questions naturally appear in the analysis of counter machines extended with unordered data: namely, for data vectors over $(\mathbb{Z}^d,+)$ expressibility directly corresponds to checking state equations for Coloured Petri nets where tokens can only be tested for equality. We derive that in this case, expressibility is in $NP$, and in $P$ for reversible instances. These upper bounds are tight: they match the lower bounds for standard integer vectors (over singleton domains).

ABSTRACT. We consider first-order logic on the subword ordering on finite words, where each word is available as a constant. Our first result is that the \Sigma_1 theory is undecidable (already over two letters). In particular, we settle the open question of how many letters are required to make the \Sigma_2 theory without constants undecidable: Two suffice.

We investigate the decidability border by considering fragments where all but a certain number of variables are alternation bounded, meaning that the variable can only be quantified relative to words with a bounded number of letter alternations. We prove that undecidability of the \Sigma_1 fragment holds already for three variables without alternation bound. For two variables without alternation bound, the fragment is decidable. The \Sigma_2 fragment is undecidable already for one variable without alternation bound. When all variables are alternation bounded, the entire first-order theory is decidable.

Furthermore, we obtain various complexity and expressiveness results regarding the decidable fragments.

ABSTRACT. We propose a novel automata model over the alphabet of rational numbers, which we call register automata over the rationals (RA-Q). It reads a sequence of rational numbers and outputs another rational number. RA-Q is an extension of the well-known register automata (RA) over infinite alphabets, which are finite automata equipped with a finite number of registers/variables for storing values. Like in the standard RA, the RA-Q model allows both equality and ordering tests between values. It, moreover, allows to perform linear arithmetic between certain variables. The model is quite expressive: in addition to the standard RA, it also generalizes other well-known models such as affine programs and arithmetic circuits.

The main feature of RA-Q is that despite the use of linear arithmetic, the so-called invariant problem---a generalization of the standard non-emptiness problem---is decidable. We also investigate other natural decision problems, namely, commutativity, equivalence, and reachability. For deterministic RA-Q, commutativity and equivalence are polynomial-time inter-reducible with the invariant problem.

ABSTRACT. We introduce a generalisation of weighted automata over a field, called polynomial automata, and we analyse the complexity of the Zeroness Problem in this model, that is, whether a given automaton outputs zero on all words. While this problem is non-primitive recursive in general, we highlight a subclass of polynomial automata for which the Zeroness Problem is primitive recursive. Refining further, we identify a subclass of affine VAS for which coverability is in 2EXPSPACE. We also use polynomial automata to obtain new proofs that equivalence of streaming string transducers is decidable, and that equivalence of copyless streaming string transducers is in PSPACE.

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.

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.

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.

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.

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

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.

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.

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.

ABSTRACT. We give a model of dependent type theory with one univalent universe and propositional truncation interpreting a type as a stack, generalising the groupoid model of type theory. As an application, we show that countable choice cannot be proved in dependent type theory with one univalent universe and propositional truncation.

ABSTRACT. We introduce a dependent type theory whose models are weak ω-categories. This definition of ω-categories is inspired of the one of Grothendieck and Maltsiniotis who define them as presheaves preserving globular colimits over a certain category, called a coherator, which encodes all operations required to be present in an ω-category. These operations correspond to compositions of pasting schemes as well as their coherences: one of our main contributions is to provide a canonical type-theoretical characterization of pasting schemes as contexts which can be derived from inference rules. Finally, we present an implementation of a corresponding proof system.

ABSTRACT. Homotopy type theory is a version of Martin-Löf type theory taking advantage of its homotopical models. In particular, we can use construct objects of homotopy theory and reason about them using higher inductive types. In this article we construct the real projective spaces, key players in homotopy theory, as certain higher inductive types in homotopy type theory. The classical definition of RPⁿ, as the quotient space identifying antipodal points of the n-sphere, does not translate directly to homotopy type theory. Instead, we define RPⁿ by induction on n simultaneously with its tautological bundle of 2-element sets. As the base case, we take RP⁻¹ to be the empty type. In the inductive step, we take RPⁿ⁺¹ to be the mapping cone of the projection map of the tautological bundle, and we use universal property and the univalence axiom to define the tautological bundle on RPⁿ⁺¹.

We retrieve the classical description of RPⁿ as RPⁿ⁻¹ with an n-disk attached to it. The infinite dimensional real projective space, defined as the sequential colimit of the RPⁿs with the canonical inclusion maps, is equivalent to the Eilenberg-MacLane space K(Z/2Z,1), which here arises as the subtype of the universe consisting of 2-element types. Indeed, the infinite dimensional projective space classifies the 0-sphere bundles, which one can think of as synthetic line bundles.

These constructions in homotopy type theory further illustrate the utility of homotopy type theory, through the interplay of type theoretic and homotopy theoretic ideas.

ABSTRACT. Recently (authors, POPL 2017), a notion of dimensionality for intersection types was introduced, and it was shown that the bounded-dimensional inhabitation problem is decidable under a nonidempotent interpretation of intersection and undecidable in the standard set theoretic model. In this paper we study the typability problem for bounded-dimensional intersection types and prove that the problem is decidable in both models. We establish a number of bounding principles depending on dimension. In particular, it is shown that dimensional bound on derivations gives rise to a bounded width property on types, which is related to a generalized subformula property for typings of arbitrary terms. Using the bounded width property we can construct a nondeterministic transformation of the typability problem to unification, and we prove that typability in the set theoretic model is PSPACE-complete, whereas it is in NP in the multiset model.

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.

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.

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.

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.

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.

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.

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.

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.