Séminaire, 30 mars 2023

Programme

10:30 – 12:00

Pierre Clairambault (LIS, CNRS)

Invited talk: The Geometry of Causality : Multi-token Geometry of Interaction and Its Causal Unfolding

Concurrent Games is a framework developed in the past decade for semantics of programming languages. In Concurrent Games, a program is interpreted as an event structure, representing its interactive behaviour with its execution environment. The representation is extremely fine-grained: it is causal as in so-called truly concurrent models of concurrency, showing explicitely the dependence and independence of computational events, and the non-deterministic branching points.

This interpretation is computed in a modular way by induction on programs, following the methodology of denotational semantics. This is good, because it means that the semantics can be used to reason compositionally on programs. But it is also bad, because the many layers of the interpretation of the source code in a denotational model and the complexity of the operations involved (notably, the composition of strategies) blurs the relationship between the source code and the semantics.

In this work, we make concurrent games operational. More precisely, we show that programs can be translated compositionally intro certain coloured Petri nets, combining intuitions from game semantics, Girard's Geometry of Interaction, and folklore ideas on the representation of first-order imperative concurrent programs as Petri nets. We regard these coloured Petri nets as a kind of intermediate representation, still close to the source code. But as finite graphs unfold to infinite trees, Petri nets unfold to event structures; and here we show that this unfolding yields the same event structure obtained denotationally from the interpretation in concurrent games.

We deploy this for Idealized Parallel Algol, a call-by-name higher-order concurrent programming language that is well-studied in the game semantics literature. The translation is implemented, and available at:

https://ipatopetrinets.github.io/

This is joint work with Simon Castellan.

13:45 – 14:45

Jules Jacobs (Radboud University)

Invited talk: Fast Coalgebraic Bisimilarity Minimization

Coalgebraic bisimilarity minimization generalizes classical automaton minimization to a large class of automata whose transition structure is specified by a functor, subsuming strong, weighted, and probabilistic bisimilarity. This offers the enticing possibility of turning bisimilarity minimization into an off-the-shelf technology, without having to develop a new algorithm for each new type of automaton. Unfortunately, there is no existing algorithm that is fully general, efficient, and able to handle large systems.

We present a generic algorithm that minimizes coalgebras over an arbitrary functor in the category of sets as long as the action on morphisms is sufficiently computable. The functor makes at most O(m logn) calls to the functor-specific action, where n is the number of states and m is the number of transitions in the coalgebra.

While more specialized algorithms can be asymptotically faster than our algorithm (usually by a factor of (m/n)), our algorithm is especially well suited to efficient implementation, and our tool often uses much less time and memory on existing benchmarks, and can handle larger automata, despite being more generic.

15:15 – 16:15

Will Troiani (LIPN and Melbourne (Australia))

Invited talk: Computation in logic as the splitting of idempotents in algebraic geometry; two models of multiplicative linear logic

A hypersurface f = 0 in complex affine space is singular if and only if there exists a non-contractible matrix factorization (to be defined in the talk). Matrix factorisations are organised into a bicategory where composition is defined via a two-step process, first an infinite model of the composite is described, and then a terminating procedure is followed to extract a finite  presentation. Is this terminating procedure a semantics of cut-elimination? By considering simple cases, Daniel Murfet and myself have uncovered two models of multiplicative linear logic, one in the space of coordinate rings where cut-elimination corresponds to the celebrated Buchberger Algorithm, and the other in the space of Quantum Error Correction Codes, where cut-elimination corresponds to quantum error correction. The general picture has led Murfet and myself to postulate that the splitting of idempotents has fundamental relevance to the theory of computation. This talk defends this proposition.