Abstracts

We show that it is NP-hard to distinguish CNF formulas that have Resolution refutations of almost linear length from CNF formulas that do not even have weakly exponentially long ones. It follows from this that Resolution is not automatable in polynomial time unless P = NP, or in weakly exponential time unless ETH fails. The proof of this is simple enough that all its ideas can be explained in a talk. Along the way, I will try to explain the process of discovery that led us to the result. This is joint work with Moritz Müller.

String-to-string transducers can be described using automata, monadic second-order logic, regular expressions, etc. In my talk, I will focus on an approach that uses functional programming. In this approach, transducers are constructed from certain basic functions (such as head, tail, or string reversal), by using combinators (such as map, flatmap, or function composition).

The notion of a difference hierarchy, first introduced by Hausdorff, plays an important role in many areas of mathematics, logic and theoretical computer science such as descriptive set theory, complexity theory, and the theory of regular languages and automata. By studying difference hierarchies of the lattice of closed upsets of Priestley spaces, we will see an elementary proof of the fact that a regular language is given by a Boolean combination of purely universal sentences using arbitrary numerical predicates if and only if it is given by a Boolean combination of purely universal sentences using only regular numerical predicates. This is one of Straubing's conjectures, which was originally proved by Maciel, Péladeau, and Thérien, via a combination of semigroup and Ramsey theory. This is based on joint work with Gehrke, Krebs and Straubing.

Hella's k-pebble n-bijective is a long-studied generalisation of the k-pebble bijection game. While the latter captures equivalence of relational structures up to k-variable first-order logic extendended with fixed-point and counting quantifiers, Hella's game (for n>1) captures equivalence in the much more powerful extension of FO with all n-ary generalised quantifiers. In this talk, I'll present a new contruction that Anuj Dawar and I have been working on which extends Abramsky, Dawar and Wang's pebbling comonad to deal with generalised quantifiers.       

Traditionally, in categorical logic, first-order quantifiers are encoded as adjoints to the inclusion maps of the algebra of formulas in n free variables into the algebra of formulas in n+1 free variables. Hence, quantifiers correspond to a property of the inclusion maps. We depart from this standpoint and propose viewing quantification as a "construction". We discuss how, from this perspective, quantification can be dually understood as a space-of-measures construction. To illustrate these ideas, we draw from recent results obtained in collaboration with Mai Gehrke and Daniela Petrisan where the viewpoint of quantifiers as measures has been successfully applied in logic on words and finite model theory.

The talk is divided into two parts, one presented by Tomas Jakl and the other by Luca Reggio.

The correspondence of regular languages and monadic second-order logic relies on the fact that the class of regular languages is closed under images of surjective letter-to-letter homomorphisms. This closure property holds for finite words, but also for infinite words, finite or infinite trees, and more generally for a wide range of monads. However, it does not hold always, and a structural characterization of those monads for which it does hold seems elusive. I will focus on a few examples to illustrate how subtle the condition can be.

The talk will outline the main theme of my PhD project. I will propose a resource theory of side-information for physical theories described by symmetric monoidal categories in which the monoidal unit is a terminal object. I will discuss and re-cast the phenomenon of “quantum self-testing” within this framework. This is work in progress.

We report on work in progress, joint with Mai Gehrke, that revisits Samson Abramsky’s duality theoretic analysis of the Cartesian closed category of bifinite domains (Abramsky, 1991). The form and point of view is that of distributive lattices and their dual Stone-Priestley spaces as applied in many parts of propositional logic. This allows us to draw connections between Abramsky's construction of the domain of Scott continuous functions and the theory of algebraic normal forms in free Heyting algebras, as was developed in (Ghilardi 1995, Bezhanishvili and Gehrke, 2011).

References: S. Abramsky, Domain theory in logical form, Ann. Pure and Appl. Logic 51, 1-77 (1991). S. Ghilardi, An algebraic theory of normal forms, Ann. Pure and Appl. Logic 71, 189-245 (1995). N. Bezhanishvili and M. Gehrke, Finitely generated free Heyting algebras via Birkhoff duality and coalgebra, Log. Methods in Comp. Sci. 7(2) (2011).

Over 50 years ago, Lovász proved that two graphs are isomorphic if and only if they admit the same number of homomorphisms from any graph [Acta Math. Hungar. 18 (1967), pp. 321--328]. In this work we prove that two graphs are quantum isomorphic (in the commuting operator framework) if and only if they admit the same number of homomorphisms from any planar graph. As there exist pairs of non-isomorphic graphs that are quantum isomorphic, this implies that homomorphism counts from planar graphs do not determine a graph up to isomorphism. Another immediate consequence is that determining whether there exists some planar graph that has a different number of homomorphisms to two given graphs is an undecidable problem, since quantum isomorphism is known to be undecidable. Our characterization of quantum isomorphism is proven via a combinatorial characterization of the intertwiner spaces of the quantum automorphism group of a graph based on counting homomorphisms from planar graphs. This result inspires the definition of "graph categories" which are analogous to, and a generalization of, partition categories that are the basis of the definition of easy quantum groups. Thus we introduce a new class of "graph-theoretic quantum groups" whose intertwiner spaces are spanned by maps associated to (bi-labeled) graphs. This talk is based on a joint work with David Roberson.

In this talk we shall describe recent work at Oxford, developing a structural understanding of bisimulation games for various guarded fragments of first order logic. Intuitively, these guarded logics are wide generalisations of conventional modal logics, gaining superior expressive power, whilst retaining attractive computational characteristics. Our eventual aim is to identify the structural reasons why these logics have such desirable computational and model theoretic properties.

Our analysis builds upon the earlier work of Abramsky, Dawar, Wang and Shah exhibiting an exciting connection between two apparently disparate fields:

* The study of the power of computational methods, as typified by finite model theory and descriptive complexity
* The investigation of the structure of computational phenomena, characteristic of program semantics and particularly categorical methods

The divide is bridged by a novel comonadic perspective on model comparison games such as the pebbling and Ehrenfeuct-Fraisse games. The framework also has quantitative aspects, via natural gradings that capture resource theoretic aspects on the phenomena involved. It is these techniques that we aim extend to the guarded setting in our new work.

The talk will aim to be reasonably self contained. We shall provide an introduction to the comonadic approach to model comparison games, and background on the various logical fragments of interest.

This is work in progress, jointly with Samson Abramsky, Tom Paine, and Nihil Shah at Oxford

In our recent work on template games, we explore the idea that sequential and concurrent games should be defined as categories of positions and trajectories, regulated by a specific synchronization template. In this talk, we will bring the idea one dimension up and advocate the benefits of defining template games not just as categories, but as 2-categories of positions, trajectories and reshufflings. To that purpose, we take very seriously the analogy between asynchrony in concurrent games and the Gray tensor product of 2-categories. One technical difficulty is that the category 2-Cat of small 2-categories equipped with the Gray tensor product is symmetric monoidal, and not cartesian. This prompts us to extend the original framework of template games to a situation informed by quantum algebra, where the original surrounding category S with finite limits is replaced by a nice monoidal category with equalizers. Putting all together, we construct a 2-dimensional concurrent template game model of multiplicative additive linear logic (MALL) where every formula and proof of the logic is interpreted as a labelled 2-category equipped, respectively, with the structure of a Gray comonoid (for concurrent games) and of a Gray bicomodule (for concurrent strategies).

In this talk I will discuss the finite rank fragments of the pebbling comonad introduced by Abrasmsky, Dawar and Wang. These can be used analogously to the ‘n-cores’ used in the proof of Rossmans equirank homomorphism preservation theorem, with an aim to also preserve the number of variables used in a formula. I will give a proof of some simple cases and indicate what would be needed to prove the full result.

Combining probabilistic and non-deterministic choice is a long standing problem in denotational semantics. From a category theory perspective, the problem stems from the absence of a distributive law of the powerset monad over the distribution monad. In this talk we show the existence of a weak distributive law between these monads and we discuss applications to the semantics of probabilistic automata. This is joint work with Alexandre Goy.

We prove MSO-transductions of graphs of bounded treewidth have decidable equivalence modulo fractional isomorphism with real coefficients (not necessarily nonnegative). The main goal of this talk is to present a new approach to equivalence problem of MSO-transductions of graphs of bounded treewidth. This approach relies on associating to a graph a list of polynomials or generating functions which can be updated by a polynomial function after join and forget operation of sourced graphs.

This is joint work with Mikołaj Bojańczyk.

This talk will be about ongoing work on a subcomonad of the pebbling comonad. This subcomona captures a restriction of k-variable logic that imposes a restriction on conjunctions in a formula. In analogy with the characterization of tree-width as the coalgebra number, I will show that this subcomonad characterizes path-width. As a bonus, I will discuss ongoing work on clique-width and other graph parameters.

An old dream of concurrency theory and programming language semantics has been to uncover the fundamental synchronization mechanisms which regulate situations as different as game semantics for higher-order programs, and Hoare logic for concurrent programs with shared memory and locks. In this work, we establish a deep and unexpected connection between two recent lines of work on concurrent separation logic (CSL) and on template game semantics for differential linear logic (DiLL). Thanks to this connection, we reformulate in the purely conceptual style of template games for DiLL our asynchronous and interactive interpretation of CSL [1]. We believe that the analysis reveals something important about the secret anatomy of CSL, and more specifically about the subtle interplay, of a categorical nature, between sequential composition, parallel product, errors and locks. Joint work with Paul-André Melliès.

[1] An Asynchronous Soundness Theorem for Concurrent Separation Logic, Mellies and Stefanesco

In this talk, we define the single-use restriction for register automata over infinite alphabets (Kaminski & Francez style). It says that every register is emptied immediately after being used. We argue that under this single-use restriction, the theory of register automata becomes much more robust. In particular, one-way and two-way single-use register automata recognise the same class of languages. Motivated by this, we study the class of functions recognised by two-way single-use register transducers and show that it is very well-behaved. This is joint work with Mikołaj Bojańczyk.

Clifford circuits are defined in terms of quantum gates but their computational complexity is classical. Simulating these circuits is a complete problem for the complexity class parity-L. A rank-2 logic formula is a first-order formula possibly using an operator for computing the rank of a matrix over a two-element field. We show that evaluation of a Clifford circuit is expressible in this rank-2 logic.