LICS '24: Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science

Game logic with sabotage (GL_s) is introduced as a simple and natural extension of Parikh's game logic with a single additional primitive, which allows players to lay traps for the opponent. GL_s can be used to model infinite sabotage games, in which players can change the rules during game play. In contrast to game logic, which is strictly less expressive, GL_s is exactly as expressive as the modal μ-calculus. This reveals a close connection between the entangled nested recursion inherent in modal fixpoint logics and adversarial dynamic rule changes characteristic for sabotage games. A natural Hilbert-style proof calculus for GL_s is presented and proved complete using syntactic equiexpressiveness reductions. The completeness of a simple extension of Parikh's calculus for game logic follows.

We propose a local, past-oriented fragment of propositional dynamic logic to reason about concurrent scenarios modelled as Mazurkiewicz traces, and prove it to be expressively complete with respect to regular trace languages. Because of locality, specifications in this logic are efficiently translated into asynchronous automata, in a way that reflects the structure of formulas. In particular, we obtain a new proof of Zielonka's fundamental theorem and we prove that any regular trace language can be implemented by a cascade product of localized asynchronous automata, which essentially operate on a single process.

These results refine earlier results by Adsul et al. which involved a larger fragment of past propositional dynamic logic and used Mukund and Sohoni's gossip automaton. Our new results avoid using this automaton, or Zielonka's timestamping mechanism and, in particular, they show how to implement a gossip automaton as a cascade product.

I introduce the falsifier calculus, a new deep-inference proof system for first-order predicate logic in the language of Hilbert's epsilon-calculus. It uses a new inference rule, the falsifier rule, to introduce epsilon-terms into a proof, distinct from the critical axioms of the traditional epsilon-calculus. The falsifier rule is a generalisation of one of the quantifier-shifts, inference rules for shifting quantifiers inside and outside of formulae. Like the epsilon-calculus and proof systems which include quantifier-shifts, the falsifier calculus admits non-elementarily shorter cut-free proofs of certain first-order theorems than the sequent calculus.

Analogous to the way in which Herbrand's Theorem decomposes a proof into a first-order and a propositional part, connected by a Herbrand disjunction as an intermediate formula, I prove a decomposition theorem for the falsifier calculus which gives rise to a new notion of intermediate formula in the epsilon-calculus, falsifier disjunctions. I then prove that certain first-order theorems admit non-elementarily smaller falsifier disjunctions than Herbrand disjunctions.

Well-structured transition systems (WSTS) are an abstract family of systems that encompasses a vast landscape of infinite-state systems. By requiring a well-quasi-ordering (wqo) on the set of states, a WSTS enables generic algorithms for classic verification tasks such as coverability and termination. However, even for systems that are WSTS like vector addition systems (VAS), the framework is notoriously ill-equipped to analyse reachability (as opposed to coverability). Moreover, some important types of infinite-state systems fall out of WSTS' scope entirely, such as pushdown systems (PDS).

Inspired by recent algorithmic techniques on VAS, we propose an abstract notion of systems where the set of runs is equipped with a wqo and supports amalgamation of runs. We show that it subsumes a large class of infinite-state systems, including (reachability languages of) VAS and PDS, and even all systems from the abstract framework of valence systems, except for those already known to be Turing-complete.

Moreover, this abstract setting enables simple and general algorithmic solutions to unboundedness problems, which have received much attention in recent years. We present algorithms for the (i) simultaneous unboundedness problem (which implies computability of downward closures and decidability of separability by piecewise testable languages), (ii) computing priority downward closures, (iii) deciding whether a language is bounded, meaning included in w_l^* ··· w_k^* for some words w_l, …, w_k, and (iv) effective regularity of unary languages. This leads to either drastically simpler proofs or new decidability results for a rich variety of systems.

A fundamental issue in the λ-calculus is to find appropriate notions for meaningfulness. It is well-known that in the call-by-name λ-calculus (CbN) the meaningful terms can be identified with the solvable ones, and that this notion is not appropriate in the call-by-value λ-calculus (CbV). This paper validates the challenging claim that yet another notion, previously introduced in the literature as potential valuability (and later renamed scrutability), appropriately represents meaningfulness in CbV. Akin to CbN, this claim is corroborated by proving two essential properties. The first one is genericity, stating that meaningless subterms have no bearing on evaluating normalizing terms. To prove this (which was an open problem), we use a novel approach based on stratified reduction, indifferently applicable to CbN and CbV, and in a quantitative way. The second property concerns consistency of the smallest congruence relation resulting from equating all meaningless terms. While the consistency result is not new, we provide the first direct operational proof of it. We also show that such a congruence has a unique consistent and maximal extension, which coincides with a well-known notion of observational equivalence. Our results thus supply the formal concepts and tools that validate the informal notion of meaningfulness underlying CbN and CbV.

Turn-based discounted-sum games are two-player zero-sum games played on finite directed graphs. The vertices of the graph are partitioned between player 1 and player 2. Plays are infinite walks on the graph where the next vertex is decided by a player that owns the current vertex. Each edge is assigned an integer weight and the payoff of a play is the discounted-sum of the weights of the play. The goal of player 1 is to maximize the discounted-sum payoff against the adversarial player 2. These games lie in NP ∩ coNP and are among the rare combinatorial problems that belong to this complexity class and the existence of a polynomial-time algorithm is a major open question. Since breaking the general exponential barrier has been a challenging problem, faster parameterized algorithms have been considered. If the discount factor is expressed in unary, then discounted-sum games can be solved in polynomial time. However, if the discount factor is arbitrary (or expressed in binary), but the weights are in unary, none of the existing approaches yield a sub-exponential bound. Our main result is a new analysis technique for a classical algorithm (namely, the strategy iteration algorithm) that present a new runtime bound which is [EQUATION] for game graphs with n vertices and absolute weights of at most W. In particular, our result yields a deterministic sub-exponential bound for games with weights that are constant or represented in unary.

Vector addition system with states (VASS) is a popular model for the verification of concurrent systems. VASS consists of finitely many control states and a set of counters which can be incremented and decremented, but not tested for zero. VASS is a relatively well-studied model of computation and many results regarding the decidability of decision problems for VASS are well-known. Given that the complexity of solving almost all problems for VASS is very high, various tractable over-approximations of the reachability relation of VASS have been proposed in the literature. One such tractable over-approximation is the so-called continuous VASS, in which counters are allowed to have non-negative rational values and whenever an update is performed, the update is first scaled by an arbitrary non-zero fraction.

In this paper, we consider affine continuous VASS, which extend continuous VASS by allowing integer affine operations. Affine continuous VASS serve as an over-approximation to the model of affine VASS, in the same way that continuous VASS over-approximates the reachability relation of VASS. We investigate the tractability of affine continuous VASS with respect to the reachability, coverability and state-reachability problems for different classes of affine operations and we prove an almost-complete classification of the decidability of these problems. Namely, except for the coverability problem for a single family of classes of affine operations, we completely determine the decidability status of these problems for all classes. Furthermore, except for this single family, we also complement all of our decidability results with tight complexity-theoretic upper and lower bounds.

We present a template for the Promise Constraint Satisfaction Problem (PCSP) which is NP-hard but does not satisfy the current state-of-the-art hardness condition [ACMTCT'21]. We introduce a new "injective" condition based on the smooth version of the layered PCP Theorem and use this new condition to confirm that the problem is indeed NP-hard.

In the second part of the article, we establish a dichotomy for Boolean PCSPs defined by templates with polymorphisms in the set of linear threshold functions. The reasoning relies on the new injective condition.

This paper presents the Relational Machine Calculus (RMC): a simple, foundational model of first-order relational programming. The RMC originates from the Functional Machine Calculus (FMC), which generalizes the lambda-calculus and its standard call-by-name stack machine in two directions. One, "locations", introduces multiple stacks, which enable effect operators to be encoded into the abstraction and application constructs. The second, "sequencing", introduces the imperative notions of "skip" and "sequence", similar to kappa-calculus and concatenative programming languages.

The key observation of the RMC is that the first-order fragment of the FMC exhibits a latent duality which, given a simple decomposition of the relevant constructors, can be concretely expressed as an involution on syntax. Semantically, this gives rise to a sound and complete calculus for string diagrams of Frobenius monoids.

We consider unification as the corresponding symmetric generalization of beta-reduction. By further including standard operators of Kleene algebra, the RMC embeds a range of computational models: the kappa-calculus, logic programming, automata, Interaction Nets, and Petri Nets, among others. These embeddings preserve operational semantics, which for the RMC is again given by a generalization of the standard stack machine for the lambda-calculus. The equational theory of the RMC (which supports reasoning about its operational semantics) is conservative over both the first-order lambda-calculus and Kleene algebra, and can be oriented to give a confluent reduction relation.

Following the success of the so-called algebraic approach to the study of decision constraint satisfaction problems (CSPs), exact optimization of valued CSPs, and most recently promise CSPs, we propose an algebraic framework for valued promise CSPs.

To every valued promise CSP we associate an algebraic object, its so-called valued minion. Our main result shows that the existence of a homomorphism between the associated valued minions implies a polynomial-time reduction between the original CSPs. We also show that this general reduction theorem includes important inapproximability results, for instance, the inapproximability of almost solvable systems of linear equations beyond the random assignment threshold.

We investigate the decidability of the monadic second-order (MSO) theory of the structure (N; <, P₁,…,P_k), for various unary predicates P₁,…,P_k ⊆ N. We focus in particular on 'arithmetic' predicates arising in the study of linear recurrence sequences, such as fixed-base powers Pow_k = {kⁿ : n ∈ N}, k-th powers N_k = {n^k : n ∈ N}, and the set of terms of the Fibonacci sequence Fib = {0, 1, 2, 3, 5, 8, 13,…} (and similarly for other linear recurrence sequences having a single, non-repeated, dominant characteristic root). We obtain several new unconditional and conditional decidability results, a select sample of which are the following:

• The MSO theory of (N; <, Pow₂, Fib) is decidable;

• The MSO theory of (N; <, Pow₂, Pow₃, Pow₆) is decidable;

• The MSO theory of (N; <, Pow₂, Pow₃, Pow₅) is decidable assuming Schanuel's conjecture;

• The MSO theory of (N; <, Pow₄, N₂) is decidable;

• The MSO theory of (N; <, Pow₂, N₂) is Turing-equivalent to the MSO theory of (N; <, S), where S is the predicate corresponding to the binary expansion of [EQUATION]. (As the binary expansion of [EQUATION] is widely believed to be normal, the corresponding MSO theory is in turn expected to be decidable.)

These results are obtained by exploiting and combining techniques from dynamical systems, number theory, and automata theory.

The full version of this paper can be found in [8].

An "element-free" probability distribution is what remains of a probability distribution after we forget the elements to which the probabilities were assigned. These objects naturally arise in Bayesian statistics, in situations where elements are used as labels and their specific identity is not important.

This paper develops the structural theory of element-free distributions, using multisets and category theory. We give operations for moving between element-free and ordinary distributions, and we show that these operations commute with multinomial sampling.

We then exploit this theory to prove two representation theorems. These theorems show that element-free distributions provide a natural representation for key random structures in Bayesian nonparametric clustering: exchangeable random partitions, and random distributions parametrized by a base measure.

Workflow nets are a well-established variant of Petri nets for the modeling of process activities such as business processes. The standard correctness notion of workflow nets is soundness, which comes in several variants. Their decidability was shown decades ago, but their complexity was only identified recently. In this work, we are primarily interested in two popular variants: 1-soundness and generalised soundness.

Workflow nets have been extended with resets to model workflows that can, e.g., cancel actions. It has been known for a while that, for this extension, all variants of soundness, except possibly generalised soundness, are undecidable.

We complete the picture by showing that generalised soundness is also undecidable for reset workflow nets. We then blur this undecidability landscape by identifying a property, coined "1-in-between soundness", which lies between 1-soundness and generalised soundness. It reveals an unusual non-monotonic complexity behaviour: a decidable soundness property is in between two undecidable ones. This can be valuable in the algorithmic analysis of reset workflow nets, as our procedure yields an output of the form "1-sound" or "not generalised sound" which is always correct.

Valued constraint satisfaction problems (VCSPs) constitute a large class of computational optimisation problems. It was shown recently that, over finite domains, every VCSP is in P or NP-complete, depending on the admitted cost functions. In this article, we study cost functions over countably infinite domains whose automorphisms form an oligomorphic permutation group. Our results include a hardness condition based on a generalisation of pp-constructability as known from classical CSPs and a polynomial-time tractability condition based on the concept of fractional polymorphisms. We then observe that the resilience problem for unions of conjunctive queries (UCQs) studied in database theory, under bag semantics, may be viewed as a special case of the VCSPs that we consider. We obtain a complexity dichotomy for the case of incidence-acyclic UCQs and exemplarily use our methods to determine the complexity of a query that had remained open in the literature. Further, we conjecture that our hardness and tractability conditions match for resilience problems for UCQs.

A nondeterministic discounted-sum automaton (NDA) values a run by the discounted sum of the visited transition weights. That is, the weight in the i-th position of a run of a λ-NDA is divided by λⁱ, for a fixed discount factor λ > 1. This allows to model systems in which the influence of current events is more significant than that of future ones, a key paradigm in economics and other disciplines.

NDAs were considered so far with respect to a rational discount factor λ. It is known that for every integer λ > 1, the class of λ-NDAs has good computational properties: it is closed under determinization and under the algebraic operations min, max, addition, and subtraction, and there are algorithms for the classic decision problems, such as equivalence and containment, on its automata. On the other hand, for every rational λ ϵ Q \ N, the class of λ-NDAs lacks these closure properties, and it is open whether the classic decision problems on it are decidable. This situation significantly limits the usage of NDAs, as integral discount factors enforce at least a double decay in each step of the computation, and only allow for a very coarse decay granularity.

We study NDAs with real discount factors, and show that for every Pisot number λ, the class of λ-NDAs retains all of the above good computational properties of integral NDAs. Furthermore, as is the case with integral discount factors, we show that it is also decidable to compare two NDAs with different Pisot discount factors. To this end, we generalize known results on the representation of numbers in Pisot base, and connect them to NDAs. Complementing our positive results, we show that if a class of λ-NDAs is closed under determinization or under algebraic operations, then the discount factor λ must be a Pisot number and the transition weights must be in Q(λ). All our results hold equally for automata on finite words and for automata on infinite words.

We introduce the calculus of neo-Peircean relations, a string diagrammatic extension of the calculus of binary relations that has the same expressivity as first order logic and comes with a complete axiomatisation. The axioms are obtained by combining two well known categorical structures: cartesian and linear bicategories.

We study the computational complexity of solving stochastic games with mean-payoff objectives. Instead of identifying special classes in which simple strategies are sufficient to play ∈-optimally, or form ∈-Nash equilibria, we consider general partial-information multiplayer games and ask what can be achieved with (and against) finite-memory strategies up to a given bound on the memory.

We show NP-hardness for approximating zero-sum values, already with respect to memoryless strategies and for 1-player reachability games. On the other hand, we provide upper bounds for solving games of any fixed number of players k. We show that one can decide in polynomial space if, for a given k-player game, ∈ ≥ 0 and bound b, there exists an ∈-Nash equilibrium in which all strategies use at most b memory modes.

For given ∈ > 0, finding an ∈-Nash equilibrium with respect to b-bounded strategies can be done in FNP^NP. Similarly for 2-player zero-sum games, finding a b-bounded strategy that, against all b-bounded opponent strategies, guarantees an outcome within ∈ of a given value, can be done in FNP^NP. Our constructions apply to parity objectives with minimal simplifications.

Our results improve the status quo in several well-known special cases of games. In particular, for 2-player zero-sum concurrent mean-payoff games, one can approximate ordinary zero-sum values (without restricting admissible strategies) in FNP^NP.

We show that restricting the elimination principle of the natural numbers type in Martin-Löf Type Theory (MLTT) to a universe of types not containing ####II-types ensures that all definable functions are primitive recursive. This extends the concept of primitive recursiveness to general types. We discuss extensions to univalent type theories and other notions of computability. We are inspired by earlier work by Martin Hofmann [18], work on Joyal's arithmetic universes [27], and Hugo Herbelin and Ludovic Patey's sketched Calculus of Primitive Recursive Constructions [16].

We define a theory T_pr that is a subtheory of MLTT with two universes U₀ : U₁, such that all inductive types are finitary and U₀ is restricted to not contain ####II-types:

[EQUATION]

We prove soundness such that all functions N → N are primitive recursive. The proof requires that T_pr satisfies canonicity, which we easily prove using synthetic Tait computability [36].

We consider contextual equivalence in an ML-like language, where contexts have access to both general references and continuations. We show that in a finitary setting, i.e. when the base types are finite and there is no recursion, the problem is decidable for all programs with first-order references and continuations, assuming they have continuation- and reference-free interfaces. This is the best one can hope for in this case, because the addition of references to functions, to continuations or to references makes the problem undecidable.

The result is notable since, unlike earlier work in the area, we need not impose any restrictions on type-theoretic order or the use of first-order references inside terms. In particular, the programs concerned can generate unbounded heaps.

Our decidability argument relies on recasting the corresponding fully abstract trace semantics of terms as instances of automata with a decidable equivalence problem. The automata used for this purpose belong to the family of automata over infinite alphabets (aka data automata), where the infinite alphabet (dataset) has the shape of a forest.

Working in univalent foundations, we investigate the symmetries of spheres, i.e., the types of the form ####Sⁿ = ####Sⁿ. The case of the circle has a slick answer: the symmetries of the circle form two copies of the circle. For higher-dimensional spheres, the type of symmetries has again two connected components, namely the components of the maps of degree plus or minus one. Each of the two components has Z/2Z as fundamental group. For the latter result, we develop an EHP long exact sequence.

In the context of two-player games over graphs, a language L is called positional if, in all games using L as winning objective, the protagonist can play optimally using positional strategies, that is, strategies that do not depend on the history of the play. In this work, we describe the class of parity automata recognising positional languages, providing a characterisation of positionality for ω-regular languages. As corollaries, we establish decidability of positionality in polynomial time, finite-to-infinite and 1-to-2-players lifts, and show the closure under union of prefix-independent positional objectives, answering a conjecture by Kopczyński in the ω-regular case.

We show that the problem of whether a given PCTL formula has a finite model is undecidable. The undecidability result holds even for formulae of the form [EQUATION] where the validity of ϕ₁, ϕ₂ depends only on the states reachable in at most two transitions. Consequently, the problem of whether a given PCTL formula is valid in all finite-state Markov chains is not even semi-decidable.

Information-processing tasks modelled by homomorphisms between relational structures can witness quantum advantage when entanglement is used as a computational resource. We prove that the occurrence of quantum advantage is determined by the same type of algebraic structure (known as a minion) that captures the polymorphism identities of CSPs and, thus, CSP complexity. We investigate the connection between the minion of quantum advantage and other known minions controlling CSP tractability and width. In this way, we make use of complexity results from the algebraic theory of CSPs to characterise the occurrence of quantum advantage in the case of graphs, and to obtain new necessary and sufficient conditions in the case of arbitrary relational structures.

The 1-in-3 and Not-All-Eqal satisfiability problems for Boolean CNF formulas are two well-known NP-hard problems. In contrast, the promise 1-in-3 vs. Not-All-Eqal problem can be solved in polynomial time. In the present work, we investigate this constraint satisfaction problem in a regime where the promise is weakened from either side by a rainbow-free structure, and establish a complexity dichotomy for the resulting class of computational problems.

Indexed languages are a classical notion in formal language theory. As the language equivalent of second-order pushdown automata, they have received considerable attention in higher-order model checking. Unfortunately, counting properties are notoriously difficult to decide for indexed languages: So far, all results about non-regular counting properties show undecidability.

In this paper, we initiate the study of slice closures of (Parikh images of) indexed languages. A slice is a set of vectors of natural numbers such that membership of u, u+υ, u+w implies membership of u + υ + w. Our main result is that given an indexed language L, one can compute a semilinear representation of the smallest slice containing L's Parikh image.

We present two applications. First, one can compute the set of all affine relations satisfied by the Parikh image of an indexed language. In particular, this answers affirmatively a question by Kobayashi: Is it decidable whether in a given indexed language, every word has the same number of a's as b's.

As a second application, we show decidability of (systems of) word equations with rational constraints and a class of counting constraints: These allow us to look for solutions where a counting function (defined by an automaton) is not zero. For example, one can decide whether a word equation with rational constraints has a solution where the number of occurrences of a differs between variables X and Y.

Drawing inspiration from linear logic, quantitative semantics aim at representing quantitative information about programs and their executions: they include the relational model and its numerous extensions, game semantics, and syntactic approaches such as nonidempotent intersection types and the Taylor expansion of λ-terms. The crucial feature of these models is that programs are interpreted as witnesses which consume "bags" of resources.

"Bags" are often taken to be finite multisets, i.e. quotiented structures. Another approach typically seen in categorifications of the relational model is to work with unquotiented structures (e.g. sequences) related with explicit morphisms referred to here as symmetries, which express the exchange of resources. Symmetries are obviously at the core of these categorified models, but we argue their interest reaches beyond those --- notably, symmetry leaks in some non-categorified quantitative models (such as the weighted relational model, or Taylor expansion) under the form of numbers whose combinatorial interpretation is not always clear.

In this paper, we build on a recent bicategorical model called thin spans of groupoids, introduced by Clairambault and Forest. Notably, thin spans feature a decomposition of symmetry into two sub-groupoids of polarized --- positive and negative --- symmetries. We first construct a variation of the original exponential of thin spans, based on sequences rather than families. Then we give a syntactic characterisation of the interpretation of simply-typed λ-terms in thin spans, in terms of rigid intersection types and rigid resource terms. Finally, we formally relate thin spans with the weighted relational model and generalized species of structure. This allows us to show how some quantities in those models reflect polarized symmetries: in particular we show that the weighted relational model counts witnesses from generalized species of structure, divided by the cardinal of a group of positive symmetries.

We introduce the first minimal and complete equational theory for quantum circuits. Hence, we show that any true equation on quantum circuits can be derived from simple rules, all of them being standard except a novel but intuitive one which states that a multi-control 2π rotation is nothing but the identity. Our work improves on the recent complete equational theories for quantum circuits, by getting rid of several rules including a fairly impractical one. One of our main contributions is to prove the minimality of the equational theory, i.e. none of the rules can be derived from the other ones. More generally, we demonstrate that any complete equational theory on quantum circuits (when all gates are unitary) requires rules acting on an unbounded number of qubits. Finally, we also simplify the complete equational theories for quantum circuits with ancillary qubits and/or qubit discarding.

Markov's principle (MP) is an axiom in some varieties of constructive mathematics, stating that Σ⁰₁ propositions (i.e. existential quantification over a decidable predicate on N) are stable under double negation. However, there are various non-equivalent definitions of decidable predicates and thus Σ⁰₁ in constructive foundations, leading to non-equivalent Markov's principles. While this fact is well-reported in the literature, it is often overlooked, leading to wrong claims in standard references and published papers.

In this paper, we clarify the status of three natural variants of MP in constructive mathematics, by giving respective equivalence proofs to different formulations of Post's theorem, to stability of termination of computations, to completeness of various proof systems w.r.t. some model-theoretic semantics for Σ⁰₁-theories, and to finiteness principles for both extended natural numbers and trees. The first definition (MP_P) uses a purely propositional definition of Σ⁰₁ for predicates on natural numbers N, while the second one (MP_B) relies on functions N → B, and the third one (MP_PR) on a subset of these functions expressible in an explicit model of computation.

We then prove that MP_P is strictly stronger than MP_B, and that MP_B is strictly stronger than MP_PR for variants of Martin-Löf's constructive type theory (MLTT), leading to separation results for the above theorems. These separations are achieved through a model construction of MLTT in [EQUATION], a type theory parameterised by effects, which can be syntactically restricted as needed. We replicate effectful techniques going back to Kreisel twice to refute different logical principles (first MP_B, then MP_P), while simultaneously satisfying variants of those principles (first MP_PR, then MP_B) when effects are restricted.

All our results are checked by a proof assistant.

We study the use of local consistency methods as reductions between constraint satisfaction problems (CSPs), and promise version thereof, with the aim to classify these reductions in a similar way as the algebraic approach classifies gadget reductions between CSPs. This research is motivated by the requirement of more expressive reductions in the scope of promise CSPs. While gadget reductions are enough to provide all necessary hardness in the scope of (finite domain) non-promise CSP, in promise CSPs a wider class of reductions needs to be used.

We provide a general framework of reductions, which we call consistency reductions, that covers most (if not all) reductions recently used for proving NP-hardness of promise CSPs. We prove some basic properties of these reductions, and provide the first steps towards understanding the power of consistency reductions by characterizing a fragment associated to arc-consistency in terms of polymorphisms of the template. In addition to showing hardness, consistency reductions can also be used to provide feasible algorithms by reducing to a fixed tractable (promise) CSP, for example, to solving systems of affine equations. In this direction, among other results, we describe the well-known Sherali-Adams hierarchy for CSP in terms of a consistency reduction to linear programming.

Right-linear (or left-linear) grammars are a well-known class of context-free grammars computing just the regular languages. They may naturally be written as expressions with least fixed points but with products restricted to letters as left arguments, giving an alternative to the syntax of regular expressions. In this work, we investigate the resulting logical theory of this syntax. Namely, we propose a theory of right-linear algebras (RLA) over this syntax and a cyclic proof system CRLA for reasoning about them.

We show that CRLA is sound and complete for the intended model of regular languages. From here we recover the same completeness result for RLA by extracting inductive invariants from cyclic proofs. Finally, we extend CRLA by greatest fixed points, vCRLA, naturally modelled by languages of ω-words thanks to right-linearity. We show a similar soundness and completeness result of (the guarded fragment of) vCRLA for the model of ω-regular languages, this time requiring game theoretic techniques to handle the interleaving of fixed points.

For a sequence of random structures with n-element domains over a relational signature, we define its FO complexity as a certain subset in the Banach space ℓ^∞/c₀. The well-known FO zero-one law and FO convergence law correspond to FO complexities equal to {0, 1} and a subset of R, respectively. We present a hierarchy of FO complexity classes, introduce a stochastic FO reduction that allows to transfer complexity results between different random structures, and deduce using this tool several new logical limit laws for binomial random structures. Finally, we introduce a conditional distribution on graphs, subject to a FO sentence ϕ, that generalises certain well-known random graph models, show instances of this distribution for every complexity class, and prove that the set of all ϕ validating 0--1 law is not recursively enumerable.

We present a novel, yet rather simple construction within the traditional framework of Scott domains to provide semantics to probabilistic programming, thus obtaining a solution to a long-standing open problem in this area. We work with the Scott domain of random variables from a standard and fixed probability space---the unit interval or the Cantor space---to any given Scott domain. The map taking any such random variable to its corresponding probability distribution provides a Scott continuous surjection onto the probabilistic power domain of the underlying Scott domain, which preserving canonical basis elements, establishing a new basic result in classical domain theory. If the underlying Scott domain is effectively given, then this map is also computable. We obtain a Cartesian closed category by enriching the category of Scott domains by a partial equivalence relation to capture the equivalence of random variables on these domains. The constructor of the domain of random variables on this category, with the two standard probability spaces, leads to four basic strong commutative monads, suitable for defining the semantics of probabilistic programming.

A transducer is finite-valued if for some bound k, it maps any given input to at most k outputs. For classical, one-way transducers, it is known since the 80s that finite valuedness entails decidability of the equivalence problem. This decidability result is in contrast to the general case, which makes finite-valued transducers very attractive. For classical transducers it is also known that finite valuedness is decidable and that any k-valued finite transducer can be decomposed as a union of k single-valued finite transducers.

In this paper, we extend the above results to copyless streaming string transducers (SSTs), answering questions raised by Alur and Deshmukh in 2011. SSTs strictly extend the expressiveness of oneway transducers via additional variables that store partial outputs. We prove that any k-valued SST can be effectively decomposed as a union of k (single-valued) deterministic SSTs. As a corollary, we obtain equivalence of SSTs and two-way transducers in the finite-valued case (those two models are incomparable in general). Another corollary is an elementary upper bound for checking equivalence of finite-valued SSTs. The latter problem was already known to be decidable, but the proof complexity was unknown (it relied on Ehrenfeucht's conjecture). Finally, our main result is that finite valuedness of SSTs is decidable. The complexity is PSpace, and even PTime when the number of variables is fixed.

We present the first definition of strictly associative and unital ∞-category. Our proposal takes the form of a type theory whose terms describe the operations of such structures, and whose definitional equality relation enforces desired strictness conditions. The key technical device is a new computation rule in the definitional equality of the theory, which we call insertion, defined in terms of a universal property. On terms for which it is defined, this operation "inserts" one of the arguments of a substituted coherence into the coherence itself, appropriately modifying the pasting diagram and result type, and simplifying the syntax in the process. We generate an equational theory from this reduction relation and we study its properties in detail, showing that it yields a decision procedure for equality.

Expressed as a type theory, our model is well-adapted for generating and verifying efficient proofs of higher categorical statements. We illustrate this via an OCaml implementation, and give a number of examples, including a short encoding of the syllepsis, a 5-dimensional homotopy that plays an important role in the homotopy groups of spheres.

Maslov's class K is an expressive fragment of First-Order Logic known to have decidable satisfiability problem, whose exact complexity, however, has not been established so far. We show that K has the exponential-sized model property, and hence its satisfiability problem is NExpTime-complete. Additionally, we get new complexity results on related fragments studied in the literature, and propose a new decidable extension of the uniform one-dimensional fragment (without equality). Our approach involves a use of satisfiability games tailored to K and a novel application of paradoxical tournament graphs.

It is known that for subgraph-closed graph classes the first-order model checking problem is fixed-parameter tractable if and only if the class is nowhere dense [Grohe, Kreutzer, Siebertz, STOC 2014]. However, the dependency on the formula size is non-elementary, and in fact, this is unavoidable even for the class of all trees [Frick and Grohe, LICS 2002]. On the other hand, it is known that the dependency is elementary for classes of bounded degree [Frick and Grohe, LICS 2002] as well as for classes of bounded pathwidth [Lampis, ICALP 2023]. In this paper we generalise these results and almost completely characterise subgraph-closed graph classes for which the model checking problem is fixed-parameter tractable with an elementary dependency on the formula size. Those are the graph classes for which there exists a number d such that for every r, some tree of depth d and size bounded by an elementary function of r is avoided as an (≤r)-subdivision in all graphs in the class. In particular, this implies that if the class in question excludes a fixed tree as a topological minor, then first-order model checking for graphs in the class is fixed-parameter tractable with an elementary dependency on the formula size.

Interactions between derivatives and fixpoints have many important applications in both computer science and mathematics. In this paper, we provide a categorical framework to combine fixpoints with derivatives by studying Cartesian differential categories with a fixpoint operator. We introduce an additional axiom relating the derivative of a fixpoint with the fixpoint of the derivative. We show how the standard examples of Cartesian differential categories where we can compute fixpoints provide canonical models of this notion. We also consider when the fixpoint operator is a Conway operator, or when the underlying category is closed. As an application, we show how this framework is a suitable setting to formalize the Newton-Raphson optimization for fast approximation of fixpoints and extend it to higher order languages.

We study existence and computability of finite bases for ideals of polynomials over infinitely many variables. In our setting, variables come from a countable logical structure A, and embeddings from A to A act on polynomials by renaming variables. First, we give a sufficient and necessary condition for A to guarantee the following generalisation of Hilbert's Basis Theorem: every polynomial ideal which is equivariant, i.e. invariant under renaming of variables, is finitely generated. Second, we develop an extension of classical Buchberger's algorithm to compute a Gröbner basis of a given equivariant ideal. This implies decidability of the membership problem for equivariant ideals. Finally, we sketch upon various applications of these results to register automata, Petri nets with data, orbitfinitely generated vector spaces, and orbit-finite systems of linear equations.

Logical relations constitute a key method for reasoning about contextual equivalence of programs in higher-order languages. They are usually developed on a per-case basis, with a new theory required for each variation of the language or of the desired notion of equivalence. In the present paper we introduce a general construction of (step-indexed) logical relations at the level of Higher-Order Mathematical Operational Semantics, a highly parametric categorical framework for modeling the operational semantics of higherorder languages. Our main result states that for languages whose weak operational model forms a lax bialgebra, the logical relation is automatically sound for contextual equivalence. Our abstract theory is shown to instantiate to combinatory logics and λ-calculi with recursive types, and to different flavours of contextual equivalence.

Graph neural networks (GNN) are deep learning architectures for graphs. Essentially, a GNN is a distributed message passing algorithm, which is controlled by parameters learned from data. It operates on the vertices of a graph: in each iteration, vertices receive a message on each incoming edge, aggregate these messages, and then update their state based on their current state and the aggregated messages. The expressivity of GNNs can be characterised in terms of certain fragments of first-order logic with counting and the Weisfeiler-Lehman algorithm.

The core GNN architecture comes in two different versions. In the first version, a message only depends on the state of the source vertex, whereas in the second version it depends on the states of the source and target vertices. In practice, both of these versions are used, but the theory of GNNs so far mostly focused on the first one. On the logical side, the two versions correspond to two fragments of first-order logic with counting that we call modal and guarded.

The question whether the two versions differ in their expressivity has been mostly overlooked in the GNN literature and has only been asked recently (Grohe, LICS'23). We answer this question here. It turns out that the answer is not as straightforward as one might expect. By proving that the modal and guarded fragment of first-order logic with counting have the same expressivity over labelled undirected graphs, we show that in a non-uniform setting the two GNN versions have the same expressivity. However, we also prove that in a uniform setting the second version is strictly more expressive.

In automated complexity analysis, noninterference-based type systems statically guarantee, via soundness, the property that well-typed programs compute functions of a given complexity class, e.g., the class FP of functions computable in polynomial time. These characterizations are also extensionally complete - they capture all functions - but are not intensionally complete as some polytime algorithms are rejected. This impact on expressive power is an unavoidable cost of achieving a tractable characterization. To circumvent this issue, an avenue arising from security applications is to find a relaxation of noninterference based on a declassification mechanism that allows critical data to be released in a safe and controlled manner. Following this path, we present a new and intuitive declassification policy preserving FP-soundness and capturing strictly more programs than existing noninterference-based systems. We show the versatility of the approach: it also provides a new characterization of the class BFF of second-order polynomial time computable functions in a second-order imperative language, with first-order procedure calls. Type inference is tractable: it can be done in polynomial time.

We investigate a class of combinatory algebras, called ribbon combinatory algebras, in which we can interpret both the braided untyped linear lambda calculus and framed oriented tangles. Any reflexive object in a ribbon category gives rise to a ribbon combinatory algebra. Conversely, From a ribbon combinatory algebra, we can construct a ribbon category with a reflexive object, from which the combinatory algebra can be recovered. To show this, and also to give the equational characterisation of ribbon combinatory algebras, we make use of the internal PRO construction developed in Hasegawa's recent work. Interestingly, we can characterise ribbon combinatory algebras in two different ways: as balanced combinatory algebras with a trace combinator, and as balanced combinatory algebras with duality.

We identify morphisms of strong profunctors as a categorification of quantum supermaps. These black-box generalisations of diagrams-with-holes are hence placed within the broader field of profunctor optics, as morphisms in the category of copresheaves on concrete networks. This enables the first construction of abstract logical connectives such as tensor products and negations for supermaps in a totally theory-independent setting. These logical connectives are found to be all that is needed to abstractly model the key structural features of the quantum theory of supermaps: black-box indefinite causal order, black-box definite causal order, and the factorisation of definitely causally ordered supermaps into concrete circuit diagrams. We demonstrate that at the heart of these factorisation theorems lies the Yoneda lemma and the notion of representability.

We study the problem of distinguishing between two independent samples [EQUATION], [EQUATION] of a binomial random graph G(n, p) by first order (FO) sentences. Shelah and Spencer proved that, for a constant α ∈ (0, 1), G(n, n^−-α) obeys FO zero-one law if and only if α is irrational. Therefore, for irrational α ∈ (0, 1), any fixed FO sentence does not distinguish between [EQUATION] with asymptotical probability 1 (w.h.p.) as n → ∞. We show that the minimum quantifier depth k_α of a FO sentence [EQUATION] distinguishing between [EQUATION] depends on how closely α can be approximated by rationals:

• for all non-Liouville α ∈ (0, 1), k_α = Ω(ln ln ln n) w.h.p.;

• there are irrational α ∈ (0, 1) with k_α that grow arbitrarily slowly w.h.p.;

• [EQUATION] for all α ∈ (0, 1).

The main ingredients in our proofs are a novel randomized algorithm that generates asymmetric strictly balanced graphs as well as a new method to study symmetry groups of randomly perturbed graphs.

Craig interpolation is a fundamental property of logics with a plethora of applications from philosophical logic to computer-aided verification. The question of which interpolants can be obtained from an interpolation algorithm is of profound importance. Motivated by this question, we initiate the study of completeness properties of interpolation algorithms. An interpolation algorithm ℐ is complete if, for every interpolant C of an implication A → B, there is a proof P of A → B such that C is logically equivalent to ℐ(P). We establish incompleteness and different kinds of completeness results for several standard algorithms for resolution and the sequent calculus for propositional, modal, and first-order logic.

We study the determinisation and unambiguisation problems of weighted automata over the field of rationals: Given a weighted automaton, can we determine whether there exists an equivalent deterministic, respectively unambiguous, weighted automaton? Recent results by Bell and Smertnig show that the problem is decidable, however they do not provide any complexity bounds. We show that both problems are in PSPACE for polynomially-ambiguous weighted automata.

We aim to describe the isomorphism types of infinite structures in the language of first-order logic. This pursuit holds importance in logic in computer science, encompassing model theory, descriptional complexity, and the foundations of computability. We introduce the notion of quasi-axiomatizability aimed at describing the isomorphism types of structures. Our focus centers on two classes of algorithmically presented structures. The first is the class of structures for which the positive atomic diagrams are computably enumerable. We call these structures positive structures. The second is the class of structures for which the negative atomic diagrams are computably enumerable. We call these structures negative structures. We study quasi-axiomatizability of structures from these classes by ∃, ∀, ∃∀, and ∀∃-sentences in expansions of languages. Our work is a contribution to the interplay between expressive power of first-order logic, computability, and model theory.

Automatic Differentiation is the study of the efficient computation of differentials. While the first automatic differentiation algorithms are concomitant with the birth of computer science, the specific backpropagation algorithm has been brought to a modern light by its application to neural networks. This work unveils a surprising connection between backpropagation and Gödel's Dialectica interpretation, a logical translation that realizes semi-classical axioms. This unexpected correspondence is exploited through different logical settings. In particular, we show that the computational interpretation of Dialectica translates to the differential λ-calculus and that Differential Linear Logic subsumes the logical interpretation of Dialectica.

We show that the regular separability problem of VASS reachability languages is decidable and F_ω-complete. At the heart of our decision procedure are doubly-marked graph transition sequences, a new proof object that tracks a suitable product of the VASS we wish to separate. We give a decomposition algorithm for DMGTS that not only achieves perfectness as known from MGTS, but also a new property called faithfulness. Faithfulness allows us to construct, from a regular separator for the Z-versions of the VASS, a regular separator for the N-versions. Behind faithfulness is the insight that, for separability, it is sufficient to track the counters of one VASS modulo a large number that is determined by the decomposition.

The Weisfeiler-Leman (WL) dimension is an established measure for the inherent descriptive complexity of graphs and relational structures. It corresponds to the number of variables that are needed and sufficient to define the object of interest in a counting version of first-order logic (FO). These bounded-variable counting logics were even candidates to capture graph isomorphism, until a celebrated construction due to Cai, Fürer, and Immerman [Combinatorica 1992] showed that Ω(n) variables are required to distinguish all non-isomorphic n-vertex graphs.

Still, very little is known about the precise number of variables required and sufficient to define every n-vertex graph. For the bounded-variable (non-counting) FO fragments, Pikhurko, Veith, and Verbitsky [Discret. Appl. Math. 2006] provided an upper bound of [EQUATION] and showed that it is essentially tight. Our main result yields that, in the presence of counting quantifiers, [EQUATION] variables suffice. This shows that counting does allow us to save variables when defining graphs. As an application of our techniques, we also show new bounds in terms of the vertex cover number of the graph.

To obtain the results, we introduce a new concept called the WL depth of a graph. We use it to analyze branching trees within the Individualization/Refinement (I/R) paradigm from the domain of isomorphism algorithms. We extend the recursive procedure from the I/R paradigm by the possibility of splitting the graphs into independent parts. Then we bound the depth of the obtained branching trees, which translates into bounds on the WL dimension and thereby on the number of variables that suffice to define the graphs.

Since the introduction of the semilattice relevant logic S by [Urquhart 1972, 1973], its decision problem has persisted as an open problem.

[Urquhart 1984] showed that many relevant logics are undecidable, yet S eluded these techniques. Eventually, this led experts, including [Urquhart 2016], to conjecture that S is decidable. Contrary to this conjecture, by interpreting a tiling problem, we show that S is undecidable.

Proving compositionality of behavioral equivalence on state-based systems with respect to algebraic operations is a classical and widely studied problem. We study a categorical formulation of this problem, where operations on state-based systems modeled as coalgebras can be elegantly captured through distributive laws between functors. To prove compositionality, it then suffices to show that this distributive law lifts from sets to relations, giving an explanation of how behavioral equivalence on smaller systems can be combined to obtain behavioral equivalence on the composed system.

In this paper, we refine this approach by focusing on so-called codensity lifting of functors, which gives a very generic presentation of various notions of (bi)similarity as well as quantitative notions such as behavioral metrics on probabilistic systems. The key idea is to use codensity liftings both at the level of algebras and coalgebras, using a new generalization of the codensity lifting. The problem of lifting distributive laws then reduces to the abstract problem of constructing distributive laws between codensity liftings, for which we propose a simplified sufficient condition. Our sufficient condition instantiates to concrete proof methods for compositionality of algebraic operations on various types of state-based systems. We instantiate our results to prove compositionality of qualitative and quantitative properties of deterministic automata. We also explore the limits of our approach by including an example of probabilistic systems, where it is unclear whether the sufficient condition holds, and instead we use our setting to give a direct proof of compositionality.

In addition, we propose a compositional variant of Komorida et al.'s codensity games for bisimilarities. A novel feature of this variant is that it can also compose game invariants, which are subsets of winning positions. Under our sufficient condition of the liftability of distributive laws, composed games give an alternative proof of the preservation of bisimilarities under the composition.

We propose Pushdown Normal Form (PDNF) Bisimulation to verify contextual equivalence in higher-order functional programming languages with local state. Similar to previous work on Normal Form (NF) bisimulation, PDNF Bisimulation is sound and complete with respect to contextual equivalence. However, unlike traditional NF Bisimulation, PDNF Bisimulation is also decidable for a class of program terms that can reach configurations of unbounded size, so long as the source of unboundedness is the call stack. Our approach relies on the principle that, in model-checking for reachability, pushdown systems can be simulated by finite-state automata designed to accept their initial/final stack content. We embody this in a stack-less Labelled Transition System (LTS), together with an on-the-fly saturation procedure for call stacks, upon which bisimulation is defined. We develop up-to techniques and a prototype implementation able to verify equivalences from the literature and others inspired by real code, which were out of reach for previous work.

A uniformisation of a binary relation is a functional relation contained in it, with the same domain. The uniformisation problem asks whether such a uniformisation can be defined in a given formalism.

We solve this problem in the context of regular relations over finite words, for the fragment FO²[<] of First-Order Logic with two variables: we provide an algorithm that decides if a given regular relation over finite words admits a uniformisation definable in FO²[<].

The paper provides a new representation of languages definable in FO²[<], which can be used for the decidability of other problems involving this formalism, e.g. the problem of separability of two regular languages by a language definable in FO²[<].

Currently, there is a gap between the tools used by probability theorists and those used in formal reasoning about probabilistic programs. On the one hand, a probability theorist decomposes probabilistic state along the simple and natural product of probability spaces. On the other hand, recently developed probabilistic separation logics decompose state via relatively unfamiliar measure-theoretic constructions for computing unions of sigma-algebras and probability measures. We bridge the gap between these two perspectives by showing that these two methods of decomposition are equivalent up to a suitable equivalence of categories. Our main result is a probabilistic analog of the classic equivalence between the category of nominal sets and the Schanuel topos. Through this equivalence, we validate design decisions in prior work on probabilistic separation logic and create new connections to nominal-setlike models of probability.

In the setting of homotopy type theory, each type can be interpreted as a space. Moreover, given an element of a type, i.e. a point in the corresponding space, one can define another type which encodes the space of loops based at this point. In particular, when the type we started with is a groupoid, this loop space is always a group. Conversely, to every group we can associate a type (more precisely, a pointed connected groupoid) whose loop space is this group: this operation is called delooping. The generic procedures for constructing such deloopings of groups (based on torsors, or on descriptions of Eilenberg-MacLane spaces as higher inductive types) are unfortunately equipped with elimination principles which do not directly allow eliminating to untruncated types, and are thus difficult to work with in practice. Here, we construct deloopings of the cyclic groups Z_m which are cellular, and thus do not suffer from this shortcoming. In order to do so, we provide type-theoretic implementations of lens spaces, which constitute an important family of spaces in algebraic topology. Our definition is based on the computation of an iterative join of suitable maps from the circle to an arbitrary delooping of Z_m. In some sense, this work generalizes the construction of real projective spaces by Buchholtz and Rijke, which handles the case m = 2, although the general setting requires more involved tools. Finally, we use this construction to also provide cellular descriptions of dihedral groups, and explain how we can hope to use those to compute the cohomology and higher actions of such groups.

By means of a simple reduction from Hilbert's 10th problem we prove the somewhat surprising result that termination of one-rule rewrite systems by a linear interpretation in the natural numbers is undecidable. The very same reduction also shows the undecidability of termination of one-rule rewrite systems using the Knuth-Bendix order with subterm coefficients. The linear termination problem remains undecidable for one-rule rewrite systems that can be shown terminating by a (non-linear) polynomial interpretation. We further show the undecidability of the problem whether a one-rule rewrite system can be shown terminating by a polynomial interpretation with rational or real coefficients. Several of our results have been formally verified in the Isabelle/HOL proof assistant.

Spoiler-Duplicator games are used in finite model theory to examine the expressive power of logics. Their strategies have recently been reformulated as coKleisli maps of game comonads over relational structures, providing new results in finite model theory via categorical techniques. We present a novel framework for studying Spoiler-Duplicator games by viewing them as event structures. We introduce a first systematic method for constructing comonads for all one-sided Spoiler-Duplicator games: game comonads are now realised by adjunctions to a category of games, generically constructed from a comonad in a bicategory of game schema (called signature games). Maps of the constructed categories of games are strategies and generalise coKleisli maps of game comonads; in the case of one-sided games they are shown to coincide with suitably generalised homomorphisms. Finally, we provide characterisations of strategies on two-sided Spoiler-Duplicator games; in a common special case they coincide with spans of event structures.

We propose to study transformations on graphs, and more generally structures, by looking at how the cut-rank (as introduced by Oum) of subsets is affected when going from the input structure to the output structure. We consider transformations in which the underlying sets are the same for both the input and output, and so the cut-ranks of subsets can be easily compared. The purpose of this paper is to give a characterisation of logically defined transductions that is expressed in purely structural terms, without referring to logic: transformations which decrease the cut-rank, in the asymptotic sense, are exactly those that can be defined in monadic second-order logic. This characterisation assumes that the transduction has inputs of bounded treewidth; we also show that the characterisation fails in the absence of any assumptions.

The decidability of axiomatic extensions of the modal logic K with modal reduction principles, i.e. axioms of the form ⋄^kp → ⋄ⁿp, has remained a long-standing open problem. In this paper, we make significant progress toward solving this problem and show that decidability holds for a large subclass of these logics, namely, for quasi-dense logics. Such logics are extensions of K with modal reduction axioms such that 0 < k < n (dubbed quasi-density axioms). To prove decidability, we define novel proof systems for quasi-dense logics consisting of disjunctive existential rules, which are first-order formulae typically used to specify ontologies in the context of database theory. We show that such proof systems can be used to generate proofs and models of modal formulae, and provide an intricate model-theoretic argument showing that such generated models can be encoded as finite objects called templates. By enumerating templates of bound size, we obtain an ExpSpace decision procedure as a consequence.

We develop the theory of strong and commutative monads in the 2-dimensional setting of bicategories. This provides a framework for the analysis of effects in many recent models which form bicategories and not categories, such as those based on profunctors, spans, or strategies over games.

We then show how the 2-dimensional setting provides new insights into the semantics of concurrent functional programs. We introduce concurrent pseudomonads, which capture the fundamental weak interchange law connecting parallel composition and sequential composition. This notion brings to light an intermediate level, strictly between strength and commutativity, which is invisible in traditional categorical models. We illustrate the concept with the continuation pseudomonad in concurrent game semantics.

In developing this theory, we take care to understand the coherence laws governing the structural 2-cells. We give many examples and prove a number of practical and foundational results.

Multiparty session types (MP) are a type discipline for enforcing the structured, deadlock-free communication of concurrent and message-passing programs. Traditional MP have a limited form of choice in which alternative communication possibilities are offered by a single participant and selected by another. Mixed choice multiparty session types (MCMP) extend the choice construct to include both selections and offers in the same choice. This paper first proposes a general typing system for a mixed choice synchronous multiparty session calculus, and prove type soundness, communication safety, and deadlock-freedom.

Next we compare expressiveness of nine subcalcli of MCMP-calculus by examining their encodability (there exists a good encoding from one to another) and separation (there exists no good encoding from one calculus to another). We prove 8 new encodablity results and 20 new separation results. In summary, MCMP is strictly more expressive than classical multiparty sessions (MP) in [19] and mixed choice in mixed sessions in [8]. This contrasts to the results proven in [8, 50] where mixed sessions [8] do not add any expressiveness to non-mixed fundamental sessions in [64], shedding a light on expressiveness of multiparty mixed choice.

A seminal theorem by van Benthem characterises the bisimulation-invariant fragment of First Order Logic (FOL) in terms of Modal Logic. Similarly, Janin and Walukiewicz have shown that the bisimulation-invariant fragment of Monadic Second Order Logic (MSO) corresponds precisely to the (modal) mu-calculus. Notably, neither argument immediately carries over when only considering finite structures. In the case of FOL, Rosen provided an alternative proof, which also works over finite structures. However, such characterisations for any logic more expressive than FOL over finite structures have remained long-standing open problems. In this paper, we prove such a characterisation for parameter-free Monadic Least Fixpoint Logic, a well-known logic in between FOL and MSO. In particular, we show that, over finite structures, every two-way bisimulation-invariant formula in this logic is equivalent to a formula in the two-way mu-calculus and vice versa.

We look at concatenation hierarchies of classes of regular languages. Each such hierarchy is determined by a single class, its basis: level n is built by applying the Boolean polynomial closure operator "BPol" n times to the basis. An important and challenging open question in automata theory is deciding if a regular language belongs to a given level. For the historical dot-depth hierarchy, the membership problem is only known to be decidable at levels one and two.

We give a generic algebraic characterization of the operator BPol. It implies that for any concatenation hierarchy, if n is at least two, membership at level n reduces to a more complex problem, called covering, for the previous level, n - 1. Combined with earlier results on covering, this implies that membership is decidable for dot-depth three and for level two in the main hierarchies of the literature. For instance, we obtain that the levels two in both the modulo hierarchy and the group hierarchy have decidable membership.

The internal Church thesis (CT) is a logical principle stating that one can associate to any function f : N → N a concrete code, in some Turing-complete language, that computes f. While the compatibility of CT in simpler systems has been long known, its compatibility with dependent type theory is still an open question.

In this paper, we answer this question positively. We define "MLTT", a type theory extending MLTT with quote operators in which CT is derivable. We furthermore prove that "MLTT" is consistent, strongly normalizing and enjoys canonicity using a rather standard logical relation model. All the results in this paper have been mechanized in Coq¹.

We introduce Probabilistic Regular Expressions (PRE), a probabilistic analogue of regular expressions denoting probabilistic languages in which every word is assigned a probability of being generated. We present and prove the completeness of an inference system for reasoning about probabilistic language equivalence of PRE based on Salomaa's axiomatisation of Kleene Algebra.

In homotopy type theory, a natural number type is freely generated by an element and an endomorphism. Similarly, an integer type is freely generated by an element and an automorphism. Using only dependent sums, identity types, extensional dependent products, and a type of two elements with large elimination, we construct a natural number type from an integer type. As a corollary, homotopy type theory with only Σ, Id, Π, and finite colimits with descent (and no universes) admits a natural number type. This improves and simplifies a result by Rose.

Disjoint-paths logic, denoted FO+ DP, extends first-order logic (FO) with atomic predicates dp_k[(x₁, y₁), …, (x_k, y_k)], expressing the existence of internally vertex-disjoint paths between x_i and y_i, for 1 ≤ i ≤ k. We prove that for every graph class excluding some fixed graph as a topological minor, the model checking problem for FO+ DP is fixed-parameter tractable. This extends the model checking algorithm of Golovach et al. [SODA 2023] for FO+ DP for minor-closed graph classes. It also essentially settles the question of tractable model checking for this logic on subgraph-closed classes, since the problem is hard on subgraph-closed classes not excluding a topological minor (assuming a further mild condition on efficiency of encoding).

Monads and comonads are important constructions from category theory which find widespread application in computer science and other related disciplines. Distributive laws allow these constructions to interact compositionally. Such laws are not guaranteed to exist, and even when they do, finding them can be a difficult task.

Inspired by recent results which establish conditions under which no distributive laws can exist between pairs of monads, we present a family of no-go theorems for the existence of distributive laws of a comonad over a monad.

We begin by showing that in the category of sets every container has a unique Kleisli law over the non-empty powerset monad. We then show that this Kleisli law only extends to a comonad-monad distributive law if the comonad is a coreader comonad. Consequently, every other directed container does not distribute over the powerset monad. Next, we generalise our results to a large class of monads, which we call uniform choice monads. Examples of monads in this class include any multiset or distribution monad parameterised by a suitable semiring. Finally, we extend our results to the category of relational structures where we show that several game comonads, recently introduced in the context of finite model theory, fail to distribute over variants of the powerset and distribution monads, which are used to capture relaxations of the constraint satisfaction problem. Overall, our no-go results cover a diverse range of (co)monads that are of interest in many areas of mathematics and computer science, such as probability theory, programming languages, and finite model theory.

We propose a semantic foundation for logics for reasoning in settings that possess a distinction between equality of variables, a coarser equivalence of variables, and a notion of conditional independence between variables. We show that such relations can be modelled naturally in atomic sheaf toposes. Equivalence of variables is modelled by an intrinsic relation of atomic equivalence that is possessed by every atomic sheaf. We identify additional structure on the category generating the atomic topos (primarily, the existence of a system of independent pullbacks) that allows conditional independence to be interpreted in the topos. We then study the logic of equivalence and conditional independence that is induced by the internal logic of the topos. This atomic sheaf logic is a classical logic that validates a number of fundamental reasoning principles relating equivalence and conditional independence. As a concrete example of this abstract framework, we use the atomic topos over the category of surjections between finite nonempty sets as our main running example. In this category, the interpretations of equivalence and conditional independence coincide with those given by the multiteam semantics of independence logic, in which the role of equivalence is taken by the relation of mutual inclusion. A major difference from independence logic is that, in atomic sheaf logic, the multiteam semantics of the equivalence and conditional independence relations is embedded within a classical surrounding logic. At the end of the paper, we briefly outline two other instances of our framework, to demonstrate its versatility. The first of these is a category of probability sheaves, in which atomic equivalence is equality-in-distribution, and the conditional independence relation is the usual probabilistic one. Our other example is the Schanuel topos (equivalent to nominal sets) where equivalence is orbit equality and conditional independence amounts to a relative form of separatedness.

Given two n-element structures, A and ℬ, which can be distinguished by a sentence of k-variable first-order logic (ℒ^k), what is the minimum f(n) such that there is guaranteed to be a sentence Φ ∈ ℒ^k with at most f(n) quantifiers, such that A ⊨ Φ but ℬ ⊭ Φ? We will present various results related to this question obtained by using the recently introduced QVT games [14]. In particular, we show that when we limit the number of variables, there can be an exponential gap between the quantifier depth and the quantifier number needed to separate two structures. As a consequence, we show that ℒ^k+1 is exponentially more succinct that ℒ^k. We also show, in the setting of the existential-positive fragment, how to lift quantifier depth lower bounds to quantifier number lower bounds. This leads to almost tight bounds.

The initial algebra for an endofunctor F provides a recursion and induction scheme for data structures whose constructors are described by F. The initial-algebra construction by Adámek (1974) starts with the initial object (e.g. the empty set) and successively applies the functor until a fixed point is reached, an idea inspired by Kleene's fixed point theorem. Depending on the functor of interest, this may require transfinitely many steps indexed by ordinal numbers until termination.

We provide a new initial algebra construction which is not based on an ordinal-indexed chain. Instead, our construction is loosely inspired by Pataraia's fixed point theorem and forms the colimit of all finite recursive coalgebras. This is reminiscent of the construction of the rational fixed point of an endofunctor that forms the colimit of all finite coalgebras. For our main correctness theorem, we assume the given endofunctor is accessible on a (weak form of) locally presentable category. Our proofs are constructive and fully formalized in Agda.