Solving equation systems in ω-categorical algebras

We study the computational complexity of deciding whether a given set of term equalities and inequalities has a solution in an [Formula: see text]-categorical algebra [Formula: see text]. There are [Formula: see text]-categorical groups where this problem is undecidable. We show that if [Formula: see text] is an [Formula: see text]-categorical semilattice or an abelian group, then the problem is in P or NP-hard. The hard cases are precisely those where [Formula: see text] has a uniformly continuous minor-preserving map to the clone of projections on a two-element set. The results provide information about algebras [Formula: see text] such that [Formula: see text] does not satisfy this condition, and they are of independent interest in universal algebra. In our proofs we rely on the Barto–Pinsker theorem about the existence of pseudo-Siggers polymorphisms. To the best of our knowledge, this is the first time that the pseudo-Siggers identity has been used to prove a complexity dichotomy.

Involution-rigidness — a new exactness property, and its weak version

In this paper, we introduce and study a new exactness property in the sense of categorical algebra, which can be seen as a natural strengthening of the well-known Mal’tsev property. A variety of universal algebras has this exactness property if and only if its algebraic theory contains binary terms [Formula: see text] and an [Formula: see text]-ary term [Formula: see text] satisfying [Formula: see text], and [Formula: see text] for each [Formula: see text]. We also study the “weak” version of this exactness property, which similarly strengthens the “weak Mal’tsev property” in the sense of the second author.

ALGEBRAIC LINEAR ORDERINGS

An algebraic linear ordering is a component of the initial solution of a first-order recursion scheme over the continuous categorical algebra of countable linear orderings equipped with the sum operation and the constant 1. Due to a general Mezei-Wright type result, algebraic linear orderings are exactly those isomorphic to the linear ordering of the leaves of an algebraic tree. Using Courcelle's characterization of algebraic trees, we obtain the fact that a linear ordering is algebraic if and only if it can be represented as the lexicographic ordering of a deterministic context-free language. When the algebraic linear ordering is a well-ordering, its order type is an algebraic ordinal. We prove that the Hausdorff rank of any scattered algebraic linear ordering is less than ωω. It follows that the algebraic ordinals are exactly those less than ωωω.

The structure of first-order causality

Game semantics describe the interactive behaviour of proofs by interpreting formulas as games on which proofs induce strategies. Such a semantics is introduced here for capturing dependencies induced by quantifications in first-order propositional logic. One of the main difficulties that has to be faced during the elaboration of this kind of semantics is to characterise definable strategies, that is, strategies that actually behave like a proof. This is usually done by restricting the model to strategies satisfying subtle combinatorial conditions, whose preservation under composition is often difficult to show. In this paper we present an original methodology to achieve this task, which requires a combination of advanced tools from game semantics, rewriting theory and categorical algebra. We introduce a diagrammatic presentation of the monoidal category of definable strategies of our model using generators and relations: these strategies can be generated from a finite set of atomic strategies, and the equality between strategies admits a finite axiomatisation, and this equational structure corresponds to a polarised variation of the bialgebra notion. The work described in this paper thus forms a bridge between algebra and denotational semantics in order to reveal the structure of dependencies induced by first-order quantifiers, and lays the foundations for a mechanised analysis of causality in programming languages.