6th Southern and Midlands Logic Seminar, University of Oxford

The sixth meeting of the Southern and Midlands Logic Seminar (SMLS) will be held on the afternoon of Tuesday 18th June at the University of Oxford.

This event is co-located with the 7th International Conference on Applied Category Theory, taking place on June 17-21, and with 40th Conference on Mathematical Foundations of Programming Semantics, scheduled for June 19-21. Note that participation in ACT and MFPS requires registration for a small fee.

Participation in SMLS is free to all, but please contact Bartek Klin if you intend to participate, to help us plan practical arrangements.

Participants are encouraged to join the SMLS community on Slack, which is used for announcements and coordination. Please contact one of the SMLS organisers to be added.

The meeting is supported by a London Mathematical Society Joint Research Groups grant.

Programme: Tuesday 18th June, 2024

Last updated 16/06/24.

Venue -- changed as of 12.06!

All talks, lunch and coffee breaks will take place in the Department of Computer Science on the corner of Parks Road and Keble Road. The talks will be in the Bill Roscoe Lecture Theatre (also known as Lecture Theatre B) on the ground floor, and lunch and coffee will be served in the nearby Atrium. The most convenient entrance to reach these locations is from 6 Keble Road.

The venue is a mile away from the Oxford train station. If you do not feel like walking (for about 20 minutes), the venue is close to the bus stops at St Giles’ Church, on Banbury Road and Woodstock Road, but not all bus routes stop there (see Oxford Bus Company for details).

Abstracts

A Uniform Approach to Automata Learning. Daniela Petrisan, IRIF, Université de Paris.
In this talk we present generic algorithms for minimization and learning for various forms of automata, starting with deterministic automata, weighted automata and sequential transducers.
We start by describing various forms of automata from a more abstract perspective. We can think of automata as machines that processes some input, according to its structure (word, tree,...) and produces some effect in some universe of output values (Boolean values, probabilities, weights in a semiring, words over some alphabet,... ). We model automata as functors from an input category – describing the structure of the inputs – to some output category – describing the computational effect.
We show how minimization results from automata theory can be presented at this level of generality. We then give an overview of Angluin’s L^∗ algorithm and its variations, and see how we can reuse the minimization results in order to obtain a generic learning algorithm for functorial automata.

An Introduction to Proof Mining Metatheorems Through the Lens of Probability Theory. Keji Nori, University of Bath.
The fundamental logical 'substrates' of proof mining are the so-called general logical metatheorems on bound extractions. They use well-known proof interpretations like Gödel's functional interpretation to provide general results that quantify and allow for extracting the computational content from large classes of theorems and proofs from the respective area of application they are intended for. In this talk, I shall give a gentle introduction to the formal systems (extensions of finite type arithmetic) and logical techniques (Goedel's functional interpretation and Howard's majorizability) used in proof mining and how one extends these systems and techniques to study the computational content of probability theory. Developing such a system for probability theory is a recent joint work with Nicholas Pischke.

Commutative codensity monads and probability bimeasures. Zev Shirazi, University of Oxford.
Several well-studied probability monads have been expressed as codensity monads over small categories of stochastic maps, giving a limit description of spaces of probability measures. In this paper we show how properties of probability monads such as commutativity and affineness can arise from their codensity presentation. First we show that their codensity presentation is closely related to another characterisation of probability monads as terminal endofunctors admitting certain maps into the Giry monad, which allows us to generalise a result by Van Breugel on the Kantorovich monad. We then provide sufficient conditions for a codensity monad to lift to MonCat, and give a characterisation of exactly pointwise monoidal codensity monads; codensity monads that satisfy a strengthening of these conditions. We show that the Radon monad is exactly pointwise monoidal, and hence give a description of the tensor product of free algebras of the Radon monad in terms of Day convolution. Finally we show that the Giry monad is not exactly pointwise monoidal due to the existence of probability bimeasures that do not extend to measures, although its restriction to standard Borel spaces is. We introduce the notion of a *-monad and its Kleisli monoidal op-multicategory to describe the categorical structure that organises the spaces of probability polymeasures on measurable spaces.

Learning Closed Signal Flow Graphs. Katya Piotrovskaya, University College London.
If one wanted to represent a system in which data travels through multiple pathways while being transformed along the way, how might they do so? One interesting way would be to use a graphical language called signal flow graphs. In this talk we will introduce a specific class of signal flow graphs which are behaviourally equivalent to weighted finite automata on a singleton alphabet. In particular, we will discuss how the structure of closed signal flow graphs can be inferred from their behaviour. We will show that the algorithm we present has a better computational complexity than existing learning algorithms for weighted finite automata -- even when they are restricted to the case of a singleton alphabet.

Proof-relevant partial equivalence relations. Sam Speight, University of Birmingham.
Partial equivalence relations are important in semantics of type theory, higher-order computability and more. In this talk I will introduce categories of proof-relevant partial equivalence relations. This is part of a wider program exploring higher-dimensional realizability, inspired by the homotopy interpretation of type theory.

On the expressivity of linear recursion schemes. Andrzej Murawski, University of Oxford.
In the last decade or so, higher-order recursion schemes (HORS) have emerged as a promising technique for model-checking higher-order programs. I will discuss several results concerning the case when HORS are typed using linear logic (intuitionistic multiplicative additive linear logic, to be precise). It turns out that such schemes have an automata-theoretic counterpart, namely restricted tree-stack automata, which come from linguistics, where they were introduced to study the so-called multiple context-free languages. This leads to a new perspective on linear HORS and new decidability results. This is joint work with Pierre Clairambault (deterministic case, MFCS’19), Guanyan Li and Luke Ong (probabilistic case, LICS’22).

SMLS Organisers

Local Organisers