ABSTRACT. The so-called algebraic approach to the constraint satisfaction problem (CSP) has been a prevalent method of the study of complexity of these problems since early 2000's. The core of this approach is the notion of polymorphisms which determine the complexity of the problem (up to log-space reductions). In the past few years, a new, more general version of the CSP emerged, the promise constraint satisfaction problem (PCSP), and the notion of polymorphisms and most of the core theses of the algebraic approach were generalised to the promise setting. Nevertheless, recent work also suggests that insights from other fields are immensely useful in the study of PCSPs including algebraic topology. In this paper, we provide an entry point for category-theorists into the study of complexity of CSPs and PCSPs. We show that many standard CSP notions have clear and well-known categorical counterparts. For example, the algebraic structure of polymorphisms can be described as a set-functor defined as a right Kan extension. We provide purely categorical proofs of core results of the algebraic approach including a proof that the complexity only depends on the polymorphisms. Our new proofs are substantially shorter and, from the categorical perspective, cleaner than previous proofs of the same results. Moreover, as expected, are applicable more widely. We believe that, in particular in the case of PCSPs, category theory brings insights that can help solve some of the current challenges of the field.

ABSTRACT. Higher-dimensional automata (HDAs) provide a geometric model of true concurrency, yet their standard formulation encodes an artificial total order on events. This representational artifact causes a fundamental mismatch between the combinatorial structure of HDAs and their observable behavior, leading to logical asymmetries and complicating the application of categorical tools. In this paper, we resolve this tension by developing a semantics for HDAs that is independent of event order, based on interval ipomsets (partially ordered multisets with interfaces) that preserve only precedence and concurrency. We prove that for any HDA, the traditional ST–trace of an execution path corresponds precisely to its associated interval ipomset. On the structural side, we show that the presheaf-theoretic presentation with an unordered base and the combinatorial presentation of symmetric HDAs are categorically isomorphic. Finally, by characterizing ST- and hereditary history-preserving (hhp) bisimulation via ipomset isomorphism, we provide a unified, order-free foundation for HDA semantics. Our results resolve several critical ambiguities in the literature: they provide the necessary path-category structure to canonically apply the Open Maps framework, eliminate representational artifacts in temporal and modal logics, and bridge systematic mismatches between HDAs and other models of concurrency such as Petri nets.

ABSTRACT. We explain how to construct a cartesian closed fibration of higher-order regular languages using glueing techniques combined with a fibered refinement of the usual Frobenius reciprocity formula.

ABSTRACT. We present a unified, categorical theory of monads and distributive laws \emph{in substructural contexts}. In the study of distributive laws, the roles of (the absence of) structural rules for variable contexts have been recognized; our theory formalizes these substructural situations using Tronin's \emph{verbal categories} $\W$, in a uniform and presentation-independent manner. We define the notion of \emph{$\W$-operadic monad} (those ``defined'' in the context $\W$) and that of \emph{$\W$-commutative monad} (those ``preserved'' in the context $\W$). We present a canonical construction of a distributive law $ST\to TS$; it is applicable when $S$ is $\W$-operadic and $T$ is $\W$-commutative (under mild conditions). This accounts for many known and new distributive laws. When the condition fails, we can \emph{refine} $S$ and force $\W$-operadicity; this generalizes Varacca and Winskel's construction of indexed valuations.

ABSTRACT. A monadic decomposition of a formula over a first-order theory is an equivalent Boolean combination of atomic formulas, each containing only one variable. Monadic decomposition is a generic simplification technique that has found applications in various settings such as quantifier elimination, string solving, and constraint databases. Previous work has mostly focused on the decision problem of whether a formula admits a monadic decomposition. However, much less is known on how to actually efficiently produce a small monadic decomposition, which is required for any application. We study this question for the quantifier-free fragment of Presburger arithmetic. Here, monadic decomposability is known to be coNP-complete, and monadic decompositions can be computed in exponential time. An exponential size lower bound was only known for monadic decompositions in DNF or CNF. In this work, we extend this an exponential lower bound to general monadic decompositions. Guided by this lower bound, we present fragments that admit polynomially-sized monadic decompositions which, in many cases, can be constructed efficiently. A surprising key ingredient in our proof are small-depth circuits for arithmetic operations in Chinese remainder representation, due to Beame, Cook, Hoover (1986).

ABSTRACT. We consider expansions of Presburger arithmetic with families of monadic polynomial predicates. (Examples of such predicates are the set of perfect squares, or the set of integers of the form 2n^3-5n+3, etc.) Although the full attendant first-order theories are well known to be undecidable, very little is known when one restricts the number of variables. For single-variable theories, we obtain positive results for the following families of predicates: (i) for perfect powers, decidability of the corresponding theory follows from the solvability of hyperelliptic Diophantine equations; (ii) for polynomials of degree at most three, we establish decidability by relying on the low genus of the resulting algebraic curves; (iii) for arbitrary polynomials, conditional decidability is entailed by an effective version of Faltings's theorem, which itself was recently proved subject to certain classical number-theoretic conjectures. In turn, we present various hardness results for theories with unresolved decidability status by using them to encode certain longstanding open Diophantine problems.

ABSTRACT. Recently, symbolic structures were proposed as finite representations of potentially infinite first-order structures, where Linear Integer Arithmetic terms and formulas define the domain and interpretations of a structure. We generalize symbolic structures to use any base theory that admits a standard model, and prove decidability of the model-checking problem, which determines whether a given symbolic structure satisfies a given first-order formula, for decidable base theories. This enables proving decidability for fragments of first-order logic by establishing a symbolic model property, which states that every satisfiable formula has a symbolic model. We use this approach to prove decidability for several fragments that extend the fragment of stratified formulas, relaxing the quantifier-alternation constraints by allowing one sort to have self-looping functions, under certain restrictions. To establish the symbolic model property for these fragments we construct a symbolic model for a formula from an arbitrary model. The construction and its correctness are proved in a generic fashion, which may be instantiated to other similarly restricted fragments.

ABSTRACT. The Orbit Problem asks whether the orbit of a point under a matrix reaches a given target set. When the target is a single point, the problem was shown to be decidable in polynomial time by Kannan and Lipton. This decidability result was later extended by Chonev et al. to targets of dimension 3 (in arbitrary ambient dimension), but decidability remains open for subspaces of dimension 4. At the other extreme, the special case of the Orbit Problem in which the target set is a hyperplane of codimension 1 is equivalent to the Skolem Problem for linear recurrence sequences, whose decidability has been open for many decades. In this paper, we show that the Orbit Problem is decidable if the target subspace has dimension logarithmic in the dimension of the orbit. Over rationals, we moreover obtain a complexity bound NP^RP in this case. On the other hand, we show that the version of the Orbit Problem where the dimension of the target subspace is linear in the dimension of the orbit is as hard as the Skolem Problem.

ABSTRACT. Discrete probabilistic programs (DPPs) provide a highly expressive formalism for compactly defining arbitrary finite probabilistic models. This expressivity comes at a price: DPP inference is PSPACE-hard. In this work, we show that DPP inference only takes polynomial time for programs that are `structurally simple'. More precisely, inference can be performed in polynomial time when the primal graph of each function appearing in the probabilistic program has bounded treewidth, and the inverse acceptance probability is at most exponential in the size of the probabilistic program. Existing algorithms do not achieve this performance guarantee. Our method relies on finding suitable decompositions, algebraisations, of the string diagrams underlying DPPs, employing existing algorithms for tree decompositions. This is independent of the probabilistic setting of DPPs and has direct applications to many problems, such as evaluating queries on relational databases and cybersecurity risk assessment via attack trees.

ABSTRACT. The Metropolis--Hastings (MH) algorithm is a foundational Markov chain Monte Carlo algorithm. In this paper, we ask whether it is possible to formulate and analyse MH with existing tools from categorical probability theory, using a recent involutive framework proposed for MH-type algorithms as a concrete case study. We first show how basic concepts such as invariance and reversibility can be formulated in Markov categories, and how aspects of the involutive framework can be captured using CD categories. We then study enrichments of CD categories over commutative monoids. These provide a rich setting for reasoning synthetically about a range of important probabilistic concepts, including substochastic kernels, finite and $\sigma$-finite measures, absolute continuity, singular measures, and Lebesgue decompositions. This structure allows us to give very general necessary and sufficient conditions for an MH-type sampler to be reversible with respect to a given target distribution.

ABSTRACT. We establish a connection between two results in the literature on probabilistic semantics: a formulation of De Finetti's theorem in the language of category theory due to Jacobs and Staton, and the generic construction of the free exponential of Linear Logic by Melliès et al, that has been instantiated in the model of probabilistic coherence spaces by Crubillé et al. The structural proximity of these two construction is manifest, but making this connection formal requires technical developments on the relationship between the category of stochastic kernels and the category of integrable cones, two well-known categories in probabilistic semantics. We then use this connection to give a characterization of the total elements of the probabilistic coherence space $!\Bool$.

ABSTRACT. We describe semantic structures relevant for interpreting dependent types for statistical and probabilistic modelling. Our development extends the theory of quasi-Borel spaces (qbses) of Staton et. al, which support simply-typed, higher-order probability theory with continuous distributions. It is well-known that qbses can interpret a dependent-type theory supporting dependent function-spaces through the codomain fibration. We define an equivalent split fibration based on the family fibration, which we call quasi-Borel families (qbfs), characterise its structure, equip it with fibred monads of measures and probability, and use them to develop dependently-typed probability theory. We characterise the structure of the qbf fibration that is relevant for dependently-typed probability theory in elementary form. Our characterisations include: context extension, dependent pairs, dependent functions, extensional identity types, fibred products and coproducts, subspaces, a universe of propositions, and straightforward internalisation and externalisation principles for discrete spaces. We use these concepts to define fibred distribution and probability monads, the semantic structure needed to interpret probability distributions under a dependent context. We show that this structure satisfies a fibred version of Kock's synthetic measure theory. We also use these concepts to develop a qbs counterpart to Kolmogorov's conditional expectation. Our main result is a version of the conditional expectation that, under standard regularity assumptions, is measurable in both the random variables we are conditioning, and the observation map we are conditioning by.

ABSTRACT. Stable graphs, or equivalently Littlestone classes, were characterized by existence of linear-sized 'good' sets, a kind of strongly homogeneous set, in work of Malliaris-Shelah and Malliaris-Moran. We prove a parallel result for VC classes, showing these are characterized by existence of linear-sized symmetric or asymmetric good pairs (which we define). We give several proofs, each requiring drawing from methods and results from different areas, and resulting in different kinds of bounds. We finish with a few words on our learning theory motivation for these investigations and state some further research directions.

ABSTRACT. Consider two planar graphs which are subject to edge insertions and deletions. We show that whether the two graphs are isomorphic can be maintained with first-order logic formulas and auxiliary data of polynomial size. This places the dynamic planar graph isomorphism problem into the dynamic descriptive complexity class DynFO. As a consequence, there is a dynamic constant-time parallel algorithm with polynomial-size auxiliary data which maintains whether two dynamic planar graphs are isomorphic.

ABSTRACT. An infinite structure has the finite length property (over a given field) if, for each of its finite powers, strict chains of equivariant subspaces in the corresponding free vector space are bounded in length. Prior work showed that the countable pure set and the dense linear order without endpoints have this property.We generalise these results to (a) structures approximated by finite substructures with few orbits, provided the field is of characteristic zero, and (b) generically ordered expansions of Fraïssé limits with free amalgamation, in vocabularies consisting of unary and binary relations. As a special case, we deduce the finite length property of the Rado graph using both methods. We also describe some connections with function spaces, weighted register automata, and solving orbit-finite systems of linear equations.

ABSTRACT. Lovász (1967) showed that two graphs $G$ and $H$ are isomorphic if, and only if, they are homomorphism indistinguishable over all graphs, i.e., $G$ and $H$ admit the same number of number of homomorphisms from every graph $F$. Subsequently, a substantial line of work studied homomorphism indistinguishability over restricted graph classes. For example, homomorphism indistinguishability over minor-closed graph classes $\mathcal{F}$ such as the class of planar graphs, the class of graphs of treewidth $\leq k$, pathwidth $\leq k$, or treedepth $\leq k$, was shown to be equivalent to quantum isomorphism and equivalences with respect to counting logic fragments, respectively. Via such characterizations, the distinguishing power of e.g. logical or quantum graph isomorphism relaxations can be studied with graph-theoretic means. In this vein, Roberson (2022) conjectured that homomorphism indistinguishability over every graph class excluding some minor is not the same as isomorphism. We prove this conjecture for all vortex-free graph classes. In particular, homomorphism indistinguishability over graphs of bounded Euler genus is not the same as isomorphism. As a negative result, we show that Roberson's conjecture fails when generalized to graph classes excluding a topological minor. Furthermore, we show homomorphism distinguishing closedness for several graph classes including all topological-minor-closed and union-closed classes of forests, and show that homomorphism indistinguishability over graphs of genus $\leq g$ (and other parameters) forms a strict hierarchy.

ABSTRACT. A lazy program interpreter postpones computation until the result is actually needed. This is typically more efficient than an eager (or call-by-value) interpreter, but a concern is that the semantics is not generally preserved. We propose a new semantic analysis of lazy evaluation that relies on a subtle combination of name generation and read-only state. For a language with arbitrary algebraic effects and data types, we derive conditions under which lazy evaluation computes the same result as the eager semantics. The semantic model suggests better intermediate representations of sum and product types in a lazy interpreter, along with equations that justify further optimizations. To illustrate we sketch an implementation in OCaml. Our motivation is practical: the origin of this work is a real-world application of probabilistic programming, in which large algebraic data types cause significant performance issues with a call-by-value interpreter. Our lazy semantics justifies better optimized representations, and provides principled foundations for other methods involving laziness in probabilistic programming.

ABSTRACT. We introduce a dialect of the asynchronous $\pi$-calculus, called AW$\pi$, in which (1) an input name may be owned, at any time, by at most one process; (2) each name has either only the input or only the output capability. As a result, special processes called wires (aka forwarders, that is, processes that receive values at one name and re-transmit) behaves as substitutions when composed with any AW$\pi$ process.Thus AW$\pi$ naturally yields a category, whose morphisms are AW$\pi$ processes (modulo the reference behavioural equivalence, barbed congruence) and whose objects are types; and where wires act as identity morphisms. We show that the category of processes can be further organized into (sub)categories with the structures needed for the interpretation of common higher-order language features in the literature by drawing on insights from game semantics; notably we construct a relative Seely category, the categorical structure that concurrent game semantics has. At the same time, AW$\pi$ follows the tradition of ordinary $\pi$-calculi in that expressiveness is preserved and the operational and algebraic theory are developed in a similar manner, notwithstanding substantial technical differences in their development and proofs.In short, the goal of AW$\pi$ is to remain faithful to the operational and algebraic tradition of the $\pi$-calculi while connecting to the tradition of denotational models for programming languages.

ABSTRACT. Consider a 4-player version of Matching Pennies where a team of three players competes against the Devil. Each player simultaneously says “Heads” or “Tails”. The team wins if all four choices match; otherwise the Devil wins. If all team players randomise independently, they win with probability 1/8; if all players share a common source of randomness, they win with probability 1/2. What happens when _each pair_ of team players shares a source of randomness? Can the team do better than win with probability 1/4? The surprising (and nontrivial) answer is yes! We introduce Dicey Games, a formal framework motivated by the study of distributed systems with shared sources of randomness (of which the above example is a specific instance). We characterise the existence, representation and computational complexity of optimal strategies in Dicey Games, and we study the problem of allocating limited sources of randomness optimally within a team.

ABSTRACT. We consider multi-dimensional payoff functions in partially observable Markov decision processes. We study the structure of the set of expected payoff vectors of all strategies (policies) and study what kind are needed to achieve a given expected payoff vector. In general, pure strategies (i.e., not resorting to randomisation) do not suffice for this problem. We prove that for any payoff for which the expectation is well-defined under all strategies, it is sufficient to mix (i.e., randomly select a pure strategy at the start of a play and committing to it for the rest of the play) finitely many pure strategies to approximate any expected payoff vector up to any precision. Furthermore, for any payoff for which the expected payoff is finite under all strategies, any expected payoff can be obtained exactly by mixing finitely many strategies.