We consider compositionality, adequacy, and full abstraction from an algebraic point of view. A denotational semantics d is compositional if the denotation of a phrase is a function of the denotations of its (immediate) parts. Modelling a language as an initial  algebra over a finitary signature, compositionality is then that the image of the denotation function d can be turned into an algebra. Thus d becomes a homomorphism — indeed an epimorphism. So  we can factor the denotation function d through a compositional denotation function h, i.e., an algebra homomorphism. 

What can we do if the given denotation function d is not compositional? Say that a  compositional denotation semantics h is adequate with respect to the given denotation function if it factors through d. Then is there a best available adequate semantics? In [Hod] Wilfrid Hodges gave a construction, which can be phrased as dividing the syntax out by the “full abstraction” equivalence (actually congruence) relation, where two phrases P and Q are equivalent in this sense if, and only if, they have the same denotation in all language contexts.  This is  the final adequate semantics, as long as we restrict ourselves to epimorphisms.

In this talk we see that this pattern extends to other cases, but, perhaps surprisingly, not all. In the first we look at languages with variable-binding, following ideas of Peter Aczel for the appropriate notion of algebra. In the second, we look at the standard framework for the denotational semantics of programming languages, namely omega cpos (i.e., partial orders with lubs of increasing omega chains). In all these cases one can work with any algebra, not just free ones. However, and perhaps surprisingly, there are cases where the pattern fails, for example if we allow function symbols with countable arities there may be no final adequate semantics. An open problem emerges: to classify the categories of algebras where the final adequate denotation functions exist.  In the case of the category of sets, we see that such T-algebras exist for any finitary monad T; it may even be that a converse holds.

[Hod] Wilfrid Hodges, Formal Features of Compositionality, Journal of Logic, Language and Information, 10(1), 7-28,2001.

Higher category theory is one of the most general approaches to compositionality, with broad and striking applications across computer science, mathematics and physics. We present a new, simple way to define higher categories, in which many important compositional properties emerge as theorems, rather than axioms. Our approach is amenable to computer implementation, and we present a new proof assistant we have developed, with a powerful graphical calculus. In particular, we will outline a substantial new proof we have developed in our setting.

Distributional models of natural language use contextual co-occurences to build vectors for words and treat these as semantic representations of the words. These vectors are used for natural language tasks such as entailment, classification, paraphrasing, indexing and so on. Extending the word vectors to phrase and sentence vectors has been the Achilles heel of these models. Building raw vectors for larger language units goes against the distributional hypothesis and suffers from data sparsity. Composition is the way forward. In this talk I will show how category theory can help. I will present categorical models of language based on finite dimensional vector spaces and of Lambek's categorial grammars (residuated monoids, pregroups), joint work with Balkir, Clark, Coecke, Grefenstette, Kartsaklis, and Milajevs. I will also present more recent work, joint with Muskens, on direct vector models of lambda calculus, following the lead of Montague who applied these to natural language. The latter will enable me to relate this work to our preliminary joint work with Abramsky on sheaf theoretic models of language.

Compact closed categories have been exploited to provide compositional semantics for a variety of fields, including quantum computation and natural language processing. More recently, efforts have been made to apply these techniques to more unusual fields, such as the mathematical modelling of cognitive processes.

When applying these compositional techniques to a new field of investigation, the question often arises as to how to identify a suitable compact closed category capturing the phenomena of interest. The category of relations is a well known compact closed category and the notion of binary relation permits several different axes of variation. In this talk we will show how this freedom has been exploited in recent work to construct compact closed categories with a variety of desirable properties, and the general techniques that can be applied.

Suppose that a convex-operational theory has two properties: tomographic locality (states on composite systems are uniquely characterized by the statistics of local measurements) and transitivity (every two pure states are connected by a reversible transformation). Does it follow that this theory is automatically a subtheory of quantum mechanics? This conjecture has first been formulated by Tony Short. In the talk, I give evidence for this conjecture, but also for a surprising way in which it could fail: namely, by going from pairs to triples of systems.

Contextuality is one of the fundamental features of quantum mechanics that set it apart from classical physical theories, and recent work establishes its rôle as a resource providing a quantum advantage in certain information-processing and computational tasks. We discuss the contextual fraction as a quantitative measure of contextuality, defined for any empirical model (i.e. table indicating the probability of outcomes of measurements in a given experimental scenario). The contextual fraction bears a precise relationship to maximum violations of generalised Bell inequalities, and it is shown to be monotone with respect to a range of operations which can be thought as forming the “free” operations in a resource theory of contextuality. It is also closely related to quantifiable advantages in certain tasks, such as cooperative games and a certain form of measurement-based quantum computation.

We argue that compositionality is important when building meaningful methodologies and tools for cybersecurity. There are many cybersecurity mitigations, but how do they compose? For example how do access controls and cryptography compose against a threat like data theft? Some cybersecurity controls may compose independently, others cooperating, in other cases "the winner takes it all", etc. This compositionality presents challenges to linearity and so to performance. We will talk about recent work on the mathematics of this compositionality and its role in developing decision support systems for cybersecurity capable to efficient analyze billions of possible strategic behaviours.

Linearisability is a central notion for verifying concurrent libraries: a given library is proven safe if its operational history can be rearranged into a new sequential one which, in addition, satisfies a given specification. Linearisability has been examined for libraries in which method arguments and method results are of ground type, including libraries parameterised with such methods. In this talk we extend linearisability to the general higher-order setting: methods can be passed as arguments and returned as values. A library may also depend on abstract methods of any order. This generalised notion, along with its encapsulated variant, can be shown to be sound using techniques from operational game semantics.

This is joint work with Andrzej Murawski.

In 2010, Luis Caires and Frank Pfenning developed a propositions-as-types correspondence for concurrent computation, along the lines of the standard Curry-Howard correspondence between simply typed lambda-calculus and intuitionistic logic. Their correspondence connects a form of linear logic, and the pi-calculus equipped with session types (type-theoretic formulations of communication protocols). As well as guaranteeing correct communication in the sense that messages follow the specified protocol, the type system guarantees deadlock-free execution of concurrent processes by imposing a rather severe prohibition on cyclic interconnections. Earlier work by Naoki Kobayashi developed a more liberal type system for deadlock-freedom in the pi-calculus, which allows the formation of cyclic interconnections if there is no actual cyclic dependency between communication operations. Kobayashi's system was developed from computational intuitions, but it is natural to wonder whether it can be given a logical foundation. In this talk we explore a reformulation of Kobayashi's deadlock-freedom proof as a cut-elimination result, and assess its consequences on the computational and logical sides of the Curry-Howard correspondence.

No abstract available.

Recurrence relations have been of interest since ancient times. Perhaps the most famous is the Fibonacci numbers, where each additional term in the sequence is obtained as the sum of the previous two. I will show how we can use a graphical language of string diagrams?a ?graphical linear algebra??to reason about recurrence relations, and as a bonus, obtain efficient implementations. The application amounts to a compositional, string diagrammatic treatment of signal flow graphs?a model of computation originally studied by Claude Shannon in the 1940s.