Positive fragmentsA number of model-comparison games central to (finite) model theory, such as pebble and Ehrenfeucht-Fraïssé games, can be captured as comonads on categories of relational structures.In particular, the coalgebras for these comonads encode in a syntax-free way preservation of resource-indexed logic fragments, such as first-order logic with bounded quantifier rank or a finite number of variables.In this paper, we extend this approach to existential and positive fragments (i.e., without universal quantifiers and without negations, respectively) of first-order and modal logic.We show, both concretely and at the axiomatic level of arboreal categories, that the preservation of existential fragments is characterised by the existence of so-called pathwise embeddings, while positive fragments are captured by a newly introduced notion of positive bisimulation.As an application, we offer a new proof of an equi-resource Lyndon positivity theorem for (multi)modal logic.

We introduce an algebraic structure for studying state-independent contextuality arguments, a key form of quantum non-classicality exemplified by the well-known Peres-Mermin magic square, and used as a source of quantum advantage. We introduce commutation groups presented by generators and relations, and analyse them in terms of a string rewriting system. There is also a linear algebraic construction, a directed version of the Heisenberg group. We introduce contextual words as a general form of contextuality witness. We characterise when contextual words can arise in commutation groups, and explicitly construct non-contextual value assignments in other cases. We give unitary representations of commutation groups as subgroups of generalized Pauli n-groups.

The classical homomorphism preservation theorem, due to Łoś, Lyndon and Tarski, states that a first-order sentence φ is preserved under homomorphisms between structures if, and only if, it is equivalent to an existential positive sentence ψ. Given a notion of (syntactic) complexity of sentences, an “equi-resource” homomorphism preservation theorem improves on the classical result by ensuring that ψ can be chosen so that its complexity does not exceed that of φ. We describe an axiomatic approach to equi-resource homomorphism preservation theorems based on the notion of arboreal category. This framework is then employed to establish novel homomorphism preservation results, and improve on known ones, for various logic fragments, including first-order, guarded and modal logics.

Game comonads provide a categorical syntax-free approach to finite model theory, and their Eilenberg-Moore coalgebras typically encode important combinatorial parameters of structures. In this paper, we develop a framework whereby the essential properties of these categories of coalgebras are captured in a purely axiomatic fashion. To this end, we introduce arboreal categories, which have an intrinsic process structure, allowing dynamic notions such as bisimulation and back-and-forth games, and resource notions such as number of rounds of a game, to be defined. These are related to extensional or "static" structures via arboreal covers, which are resource-indexed comonadic adjunctions. These ideas are developed in a general, axiomatic setting, and applied to relational structures, where the comonadic constructions for pebbling, Ehrenfeucht-Fra\"iss\'e and modal bisimulation games recently introduced by Abramsky et al. are recovered, showing that many of the fundamental notions of finite model theory and descriptive complexity arise from instances of arboreal covers.

Game comonads, introduced by Abramsky, Dawar and Wang and developed by Abramsky and Shah, give an interesting categorical semantics to some Spoiler-Duplicator games that are common in finite model theory. In particular they expose connections between one-sided and two-sided games, and parameters such as treewidth and treedepth and corresponding notions of decomposition. In the present paper, we expand the realm of game comonads to logics with generalised quantifiers. In particular, we introduce a comonad graded by two parameters $n \leq k$ such that isomorphisms in the resulting Kleisli category are exactly Duplicator winning strategies in Hella's $n$-bijection game with $k$ pebbles. We define a one-sided version of this game which allows us to provide a categorical semantics for a number of logics with generalised quantifiers. We also give a novel notion of tree decomposition that emerges from the construction.

In this paper, we give an overview of some recent work on applying tools from category theory in finite model theory, descriptive complexity, constraint satisfaction, and combinatorics. The motivations for this work come from Computer Science, but there may also be something of interest for model theorists and other logicians. The basic setting involves studying the category of relational structures via a resource-indexed family of adjunctions with some process category - which unfolds relational structures into tree-like forms, allowing natural resource parameters to be assigned to these unfoldings. One basic instance of this scheme allows us to recover, in a purely structural, syntax-free way: the Ehrenfeucht-Fraïssé game; the quantifier rank fragments of first-order logic; the equivalences on structures induced by (i) the quantifier rank fragments, (ii) the restriction of this fragment to the existential positive part, and (iii) the extension with counting quantifiers; and the combinatorial parameter of tree-depth (Nesetril and Ossona de Mendez). Another instance recovers the k-pebble game, the finite-variable fragments, the corresponding equivalences, and the combinatorial parameter of treewidth. Other instances cover modal, guarded and hybrid fragments, generalized quantifiers, and a wide range of combinatorial parameters. This whole scheme has been axiomatized in a very general setting, of arboreal categories and arboreal covers. Beyond this basic level, a landscape is beginning to emerge, in which structural features of the resource categories, adjunctions and comonads are reflected in degrees of logical and computational tractability of the corresponding languages. Examples include semantic characterisation and preservation theorems, and Lovász-type results on counting homomorphisms.

Contextuality is a key signature of quantum non-classicality, which has been shown to play a central role in enabling quantum advantage for a wide range of information-processing and computational tasks. We study the logic of contextuality from a structural point of view, in the setting of partial Boolean algebras introduced by Kochen and Specker in their seminal work. These contrast with traditional quantum logic à la Birkhoff and von Neumann in that operations such as conjunction and disjunction are partial, only being defined in the domain where they are physically meaningful. We study how this setting relates to current work on contextuality such as the sheaf-theoretic and graph-theoretic approaches. We introduce a general free construction extending the commeasurability relation on a partial Boolean algebra, i.e. the domain of definition of the binary logical operations. This construction has a surprisingly broad range of uses. We apply it in the study of a number of issues, including: - establishing the connection between the abstract measurement scenarios studied in the contextuality literature and the setting of partial Boolean algebras; - formulating various contextuality properties in this setting, including probabilistic contextuality as well as the strong, state-independent notion of contextuality given by Kochen-Specker paradoxes, which are logically contradictory statements validated by partial Boolean algebras, specifically those arising from quantum mechanics; - investigating a Logical Exclusivity Principle, and its relation to the Probabilistic Exclusivity Principle widely studied in recent work on contextuality as a step towards closing in on the set of quantum-realisable correlations; - developing some work towards a logical presentation of the Hilbert space tensor product, using logical exclusivity to capture some of its salient quantum features.

In this work, we revisit the problem of testing membership in regular languages, first studied by Alon et al. [1]. We develop a one-sided error property tester for regular languages under weighted edit distance that makes O((1/ε) log(1/ε)) non-adaptive queries, assuming that the language is described by an automaton of constant size. Moreover, we show a matching lower bound, essentially closing the problem for the edit distance. As an application, we improve the space bound of the current best streaming property testing algorithm for visibly pushdown languages from O((1/ε)^4 log^6 n) to O((1/ε)^3 log^5 n log log n), where n is the size of the input. Finally, we provide aΩ(max((1/ε) , log n)) lower bound on the memory necessary to test visibly pushdown languages in the streaming model, significantly narrowing the gap between the known bounds.

In previous work ([1], [2], [3]), it has been shown how a range of model comparison games which play a central role in finite model theory, including Ehrenfeucht-Fraïssé, pebbling, and bisimulation games, can be captured in terms of resource-indexed comonads on the category of relational structures. Moreover, the coalgebras for these comonads capture important combinatorial parameters such as tree-width and tree-depth.The present paper extends this analysis to quantifier-guarded fragments of first-order logic. We give a systematic account, covering atomic, loose and clique guards. In each case, we show that coKleisli morphisms capture winning strategies for Duplicator in the existential guarded bisimulation game, while back-and-forth bisimulation, and hence equivalence in the full guarded fragment, is captured by spans of open morphisms. We study the coalgebras for these comonads, and show that they correspond to guarded tree decompositions. We relate these constructions to a syntax-free setting, with a comonad on the category of hypergraphs.

Abstract Combinatorial games are widely used in finite model theory, constraint satisfaction, modal logic and concurrency theory to characterize logical equivalences between structures. In particular, Ehrenfeucht–Fraïssé games, pebble games and bisimulation games play a central role. We show how each of these types of games can be described in terms of an indexed family of comonads on the category of relational structures and homomorphisms. The index $k$ is a resource parameter that bounds the degree of access to the underlying structure. The coKleisli categories for these comonads can be used to give syntax-free characterizations of a wide range of important logical equivalences. Moreover, the coalgebras for these indexed comonads can be used to characterize key combinatorial parameters: tree depth for the Ehrenfeucht–Fraïssé comonad, tree width for the pebbling comonad and synchronization tree depth for the modal unfolding comonad. These results pave the way for systematic connections between two major branches of the field of logic in computer science, which hitherto have been almost disjoint: categorical semantics and finite and algorithmic model theory.

Abstract The present work achieves a mathematical, in particularsyntax-independent, formulation ofdynamicsandintensionalityof computation in terms ofgamesandstrategies. Specifically, we givegame semanticsof a higher-order programming language that distinguishes programmes with the same value yet different algorithms (or intensionality) and thehiding operationon strategies that precisely corresponds to the (small-step) operational semantics (or dynamics) of the language. Categorically, our games and strategies give rise to acartesian closed bicategory, and our game semantics forms an instance of a bicategorical generalisation of the standard interpretation of functional programming languages in cartesian closed categories. This work is intended to be a step towards a mathematical foundation of intensional and dynamic aspects of logic and computation; it should be applicable to a wide range of logics and computations.

We study simulation and quantum resources in the setting of the sheaf-theoretic approach to contextuality and nonlocality. Resources are viewed behaviourally, as empirical models. In earlier work, a notion of morphism for these empirical models was proposed and studied. We generalize and simplify the earlier approach, by starting with a very simple notion of morphism, and then extending it to a more useful one by passing to a co-Kleisli category with respect to a comonad of measurement protocols. We show that these morphisms capture notions of simulation between empirical models obtained via “free” operations in a resource theory of contextuality, including the type of classical control used in measurement-based quantum computation schemes.

Combinatorial games are widely used in finite model theory, constraint satisfaction, modal logic and concurrency theory to characterize logical equivalences between structures. In particular, Ehrenfeucht-Fraïssé games, pebble games, and bisimulation games play a central role. We show how each of these types of games can be described in terms of an indexed family of comonads on the category of relational structures and homomorphisms. The index k is a resource parameter which bounds the degree of access to the underlying structure. The coKleisli categories for these comonads can be used to give syntax-free characterizations of a wide range of important logical equivalences. Moreover, the coalgebras for these indexed comonads can be used to characterize key combinatorial parameters: tree-depth for the Ehrenfeucht-Fraïssé comonad, tree-width for the pebbling comonad, and synchronization-tree depth for the modal unfolding comonad. These results pave the way for systematic connections between two major branches of the field of logic in computer science which hitherto have been almost disjoint: categorical semantics, and finite and algorithmic model theory.

Pebble games are a powerful tool in the study of finite model theory, constraint satisfaction and database theory. Monads and comonads are basic notions of category theory which are widely used in semantics of computation and in modern functional programming. We show that existential k-pebble games have a natural comonadic formulation. Winning strategies for Duplicator in the k-pebble game for structures A and B are equivalent to morphisms from A to B in the coKleisli category for this comonad. This leads on to comonadic characterisations of a number of central concepts in Finite Model Theory: · Isomorphism in the co-Kleisli category characterises elementary equivalence in the k-variable logic with counting quantifiers. · Symmetric games corresponding to equivalence in full k-variable logic are also characterized. · The treewidth of a structure A is characterised in terms of its coalgebra number: the least k for which there is a coalgebra structure on A for the k-pebbling comonad. · Co-Kleisli morphisms are used to characterize strong consistency, and to give an account of a Cai-Fürer-Immerman construction. · The k-pebbling comonad is also used to give semantics to a novel modal operator. These results lay the basis for some new and promising connections between two areas within logic in computer science which have largely been disjoint: (1) finite and algorithmic model theory, and (2) semantics and categorical structures of computation.

Homomorphisms between relational structures play a central role in finite model theory, constraint satisfaction and database theory. A central theme in quantum computation is to show how quantum resources can be used to gain advantage in information processing tasks. In particular, non-local games have been used to exhibit quantum advantage in boolean constraint satisfaction, and to obtain quantum versions of graph invariants such as the chromatic number. We show how quantum strategies for homomorphism games between relational structures can be viewed as Kleisli morphisms for a quantum monad on the (classical) category of relational structures and homomorphisms. We show a general connection between these notions and state-independent quantum realizations of strong contextuality in the Abramsky-Brandenburger formulation of contextuality. We use these results to exhibit a wide range of examples of contextuality-powered quantum advantage, and to unify several apparently diverse strands of previous work.

We present a novel coalgebraic formulation of infinite extensive games. We define both the game trees and the strategy profiles by possibly infinite systems of corecursive equations. Certain strategy profiles are proved to be subgame-perfect equilibria using a novel proof principle of predicate coinduction which is shown to be sound. We characterize all subgame-perfect equilibria for the dollar auction game. The economically interesting feature is that in order to prove these results we do not need to rely on continuity assumptions on the pay-offs which amount to discounting the future. In particular, we prove a form of one-deviation principle without any such assumptions. This suggests that coalgebra supports a more adequate treatment of infinite-horizon models in game theory and economics.

Contextuality is a key feature of quantum mechanics that provides an important non-classical resource for quantum information and computation. Abramsky and Brandenburger used sheaf theory to give a general treatment of contextuality in quantum theory [New Journal of Physics 13 (2011) 113036]. However, contextual phenomena are found in other fields as well, for example database theory. In this paper, we shall develop this unified view of contextuality. We provide two main contributions: firstly, we expose a remarkable connection between contexuality and logical paradoxes; secondly, we show that an important class of contextuality arguments has a topological origin. More specifically, we show that "All-vs-Nothing" proofs of contextuality are witnessed by cohomological obstructions.

We investigate the use of coalgebra to represent quantum systems, thus providing a basis for the use of coalgebraic methods in quantum information and computation. Coalgebras allow the dynamics of repeated measurement to be captured, and provide mathematical tools such as final coalgebras, bisimulation and coalgebraic logic. However, this application raises new challenges for coalgebra: how to accommodate the contravariance which arises naturally as we represent both the states and the properties of physical systems; and how to represent the symmetries of these systems, which account e.g. for their unitary dynamics. This motivates us to introduce a novel fibrational structure for coalgebra, and also to make new connections betwen coalgebras and Chu spaces.

We define a strongly normalising proof-net calculus corresponding to the logic of strongly compact closed categories with biproducts. The calculus is a full and faithful representation of the free strongly compact closed category with biproducts on a given category with an involution. This syntax can be used to represent and reason about quantum processes.

Quantum information and computation is concerned with the use of quantum-mechanical systems to carry out computational and information-processing tasks (Nielsen and Chunag, 2000). In the few short years that this approach has been studied, a number of remarkable concepts and results have emerged, most notably:a couple of spectacular algorithms and a number of information protocols, exemplified by quantum teleportation, which exploit quantum entanglement in an essential fashion. The current tools available for developing quantum algorithms and protocols are deficient on two main levels: firstly, they are too low-level and at a more fundamental level, the standard mathematical framework for quantum mechanics (which is essentially due to von Neumann (1932)) is actually insufficiency comprehensive for informatic purposes. In joint work with Bob Coecke, we have recently made some striking progress in addressing both these points. They have recast the von Neumann formalism at a more abstract and conceptual level, using category theory.

Particular focus in this paper is on quantum information protocols, which exploit quantum-mechanical effects in an essential way. The particular examples we shall use to illustrate our approach will be teleportation (Benett et al., 1993), logic-gate teleportation (Gottesman and Chuang,1999), and entanglement swapping (Zukowski et al., 1993). The ideas illustrated in these protocols form the basis for novel and potentially very important applications to secure and fault-tolerant communication and computation (2001,1999,2000).

We introduce nominal games for modelling programming languages with dynamically generated local names, as exemplified by Pitts and Stark's nu-calculus. Inspired by Pitts and Gabbay's recent work on nominal sets, we construct arenas and strategies in the world (or topos) of Fraenkel-Mostowski sets (or simply FM-sets). We fix an infinite set N of names to be the "atoms" of the FM-theory, and interpret the type v of names as the flat arena whose move-set is N. This approach leads to a clean and precise treatment of fresh names and standard game constructions (such as plays, views, innocent strategies, etc.) that are considered invariant under renaming. The main result is the construction of the first fully-abstract model for the nu-calculus.

Connections between the sequentiality/concurrency distinction and the semantics of proofs are investigated, with particular reference to games and Linear Logic.

We present an axiomatic framework for Girard's Geometry of Interaction based on the notion of linear combinatory algebra. We give a general construction on traced monoidal categories, with certain additional structure, that is sufficient to capture the exponentials of Linear Logic, which produces such algebras (and hence also ordinary combinatory algebras). We illustrate the construction on six standard examples, representing both the ‘particle-style’ as well as the ‘wave-style’ Geometry of Interaction.

A new concurrent form of game semantics is introduced. This overcomes the problems which had arisen with previous, sequential forms of game semantics in modelling Linear Logic. It also admits an elegant and robust formalization. A Full Completeness Theorem for Multiplicative-Additive Linear Logic is proved for this semantics.

A games model of a programming language with higher-order store in the style of ML-references is introduced. The category used for the model is obtained by relaxing certain behavioural conditions on a category of games previously used to provide fully abstract models of pure functional languages. The model is shown to be fully abstract by means of factorization arguments which reduce the question of definability for the language with higher-order store to that for its purely functional fragment.

We define a category of games /spl Gscr/, and its extensional quotient /spl Escr/. A model of the lazy X-calculus, a type-free functional language based on evaluation to weak head normal form, is given in /spl Gscr/, yielding an extensional model in /spl Escr/. This model is shown to be fully abstract with respect to applicative simulation. This is, so fear as we known, the first purely semantic construction of a fully abstract model for a reflexively-typed sequential language.

Abstract We present a game semantics for Linear Logic, in which formulas denote games and proofs denote winning strategies. We show that our semantics yields a categorical model of Linear Logic and prove full completeness for Multiplicative Linear Logic with the MIX rule: every winning strategy is the denotation of a unique cut-free proof net. A key role is played by the notion of history-free strategy; strong connections are made between history-free strategies and the Geometry of Interaction. Our semantics incorporates a natural notion of polarity, leading to a refined treatment of the additives. We make comparisons with related work by Joyal, Blass, et al.

This paper describes the integrated engineering study scheme, based around a set of 4 year MEng programmes of study, established by Imperial College. The paper outlines the rationale for the scheme and gives an account of its constituent programmes of study and the curriculum. The organisation and pattern of teaching, student workload and assessment methods are discussed. A detailed comparison of the scheme with the proposals and recommendations of the important model curricula are given.

Various notions of observing and testing processes are placed in a uniform algebraic framework in which observations are taken as constituting a quantale. General completeness criteria are stated, and proved in our applications.

A new formal embodiment of J.-Y. Girard's (1989) geometry of interaction program is given. The geometry of interaction interpretation considered is defined, and the computational interpretation is sketched in terms of dataflow nets. Some examples that illustrate the key ideas underlying the interpretation are given. The results, which include the semantic analogue of cut-elimination, stated in terms of a finite convergence property, are outlined.>

This paper defines the categorical notions of relators and transformations and shows that these concepts enable us to give a semantics for polymorphic, higher order functional programs.We demonstrate the pertinence of this semantics to the analysis of polymorphic programs by proving that strictness analysis is a polymorphic invariant.

Some basic topics in the theory of concurrency are studied from the point of view of denotational semantics, and particularly the “domain theory in logical form” developed by the author. A domain of synchronization trees is defined by means of a recursive domain equation involving the Plotkin powerdomain. The logical counterpart of this domain is described, and shown to be related to it by Stone duality. The relationship of this domain logic to the standard Hennessy-Milner logic for transition systems is studied; the domain logic can be seen as a rational reconstruction of Hennessy-Milner logic from the standpoint of a very general and systematic theory. Finally, a denotational semantics for SCCS based on the domain of synchronization trees is given, and proved fully abstract with respect to bisimulation.

We develop a formalism for abstract interpretation based on logical relations. As a case study, we use this formalism to give new proofs of correctness for strictness analysis on the typed λ-calculus, and also for termination analysis. We then go on to a deeper study of the duality between safety and liveness properties, and the construction of abstraction functions which can be used to give the best possible interpretations of higher-type constants. This turns out to be a special case of the construction of Kan extensions in category theory. Necessary and sufficient conditions are given for abstraction functions to be definable over continuous type structures and for the abstraction functions themselves to be continuous.