The Theoretical Cosynus Seminar

The theoretical cosynus seminar is aimed at PhD students and young researchers (but older are also welcome) of the Coynus team (but people from other teams are also welcome) in order to have informal presentations about

in the areas of fundamental computer science. This is intended as a safe space to discuss research being done, or share interest about research from others. More mature works are typically presented in the proofs and algorithms seminar.

Everybody is welcome to subscribe to the mailing-list or to the calendar.

Mehdi Zadem (LIX) – Goal Abstraction in Hierarchical Reinforcement Learning via Reachability Analysis
22 January 2024 at 16:00 in Philippe Flajolet

However, the existing Hierarchical Reinforcement Learning (HRL) approaches relying on symbolic reasoning are often limited as they require a manual goal representation. The challenge in autonomously discovering a symbolic goal representation is that it must preserve critical information, such as the environment dynamics.

I will present a developmental mechanism for subgoal discovery via an emergent representation that abstracts (i.e., groups together) sets of environment states that have similar roles in the task. This mechanism is integrated in a HRL algorithm and shown to be data-efficient, transferrable and interpretable on a set of navigation tasks.

Elies Harington (LIX) – Introduction to Homotopy Type Theory
23 November 2023 at 16:00 in Kateryna Lohvynivna Yushchenko

Homotopy Type Theory (thereafter, HoTT) is a logical foundation for mathematics developed in the early 2010’s. Like the name suggests, the fundamental objects in HoTT are homotopy types, rather than sets. Homotopy types are mathematical objects that first arose in the study of algebraic topology : there a homotopy type is just a topological space up to a “weak homotopy equivalence”. However since then a number of ways of defining homotopy types in set theory have been discovered, so much so that an entire theory has been developed for studying and comparing different models of homotopy types : the theory of Quillen Model Categories. In HoTT however, there is no particular choice of a model : HoTT is the internal language of the theory of homotopy types. Hence every proof in HoTT is automatically true in any particular model.

From the point of view of Computer Science, HoTT is based on Martin Löf’s Type Theory (rather than on first order logic like in the case of ZFC), which makes it very prone to formalization in formal proof assistants. The main axiom distinguishing HoTT from ordinary MLTT also has a nice type-theoretic interpretation : the invariance of properties of data structures under a suitable notion of isomorphism.

In this talk, I will present Homotopy Type Theory, and explain the main ideas and intuitions to have when working in homotopy-theoretic mathematics.

Martin Krejca (LIX) – Evolving Probability Distributions
06 November 2023 at 16:00 in Philippe Flajolet

Heuristic optimization is performed in a multitude of ways. A very common strategy is to create a set of solutions, typically drawn at random, and to then iteratively update it by modifying the solutions randomly, keeping good solutions and eliminating bad ones. An interesting alternative approach is to maintain a probabilistic model instead of a solution set. In this approach, solutions are sampled randomly according to the model, and the model is then updated based on the observed distribution of good samples.

In this talk, we provide a rough overview of the mathematical analysis of algorithms that encompass both of the above approaches, known as randomized search heuristics. We then focus on an algorithm class that follows the second approach, so-called estimation-of-distribution algorithms (EDAs). We discuss the general ideas that go into proving run time guarantees for EDAs and the problems that arise when considering more complex EDAs.

Titouan Carette (LIX) – Graphical Linear Algebra
23 October 2023 at 16:00 in Philippe Flajolet

Linear algebra is everywhere, and anyone studying mathematics, physics, computer science or engineering will have to master some of it at some point. It seems then surprising that the very abstract category theory, particularly string diagrammatic notation, can bring new insights about what is often considered a very basic piece of mathematics. In this talk, I will introduce the linear relation formalism and the associated diagrammatic language. I will go through many elementary notions of linear algebra purely pictorially. The content of this talk is mainly inspired by the work of Fabio Zanasi, Pawel Sobocinski, Filippo Bonchi, and others, with some concepts and notations imported from my work on quantum diagrammatic languages. https://graphicallinearalgebra.net/2015/04/23/makelele-and-linear-algebra/

Émile Oleon (LIX) – Delooping cyclic groups with lens spaces in homotopy type theory
09 October 2023 at 16:00 in Philippe Flajolet

Lens spaces can be described as quotients of the 3-dimensional sphere by (free) actions of cyclic groups. They were first introduced by Tietze in 1908, and have played an important role in the study of manifold topology throughout the 20 century. They were for instance the first known example of 3 dimensional manifolds whose homotopy type is not caracterised by the classicals invariants of algebraic topology (that is homology and homotopy groups).

The construction of such spaces can be generalised in higher dimensions, allowing us to define approximations of the homotopy type of K(ℤₖ,1), the delooping of the cyclic group with k elements. In particular we can construct in that way a model of K(ℤₖ,1) by considering an inductive limit. We will see how to replicate these constructions in the homotopy type theory setting. The interest of such an approach is that the model of Bℤₖ we will obtain is cellular, as opposed to classical models of group deloopings in HoTT (e.g. via the type of G-torsors or via truncation). It thus open the way to a the computation of the cohomology of ℤₖ in homotopy type theory.

Morgan Rogers (LIPN, Paris Nord) – Actegories: the generic setting for monoid acts
19 October 2022 at 16:00 in Philippe Flajolet

The microcosm principle is the informal idea that given an algebraic theory, the most general setting in which such structures can be defined is obtained by lifting the theory to the level of categories. For monoid acts, also known as modules, this results in the notion of actegory, which consists of a monoidal category M (the most general setting in which monoids can be defined), an ordinary category C (the class of objects on which the monoids shall act) and an action of the former on the latter given by a functor C × M → C satisfying some compatibility conditions with respect to the monoidal structure on M. In this talk I’ll explain my motivation for studying these things and give a bunch of examples. Disclaimer: I only came to this topic recently, so I will not be presenting big or novel results; this is just a window into my monoid action adventure.

Bryce Clarke (LIX) – An introduction to enriched cofunctors
06 October 2022 at 16:00 in Philippe Flajolet

Many concepts in category theory may be generalised to the enriched setting where we are able to capture a wider range of examples. The basic notions of category, functor, and natural transformation all admit straightforward generalisations when enriching in an arbitrary monoidal category, and form the basis of enriched category theory. Cofunctors are another kind of morphism between categories which capture a notion of lifting, and the recent introduction of cofunctors between weighted categories by Perrone has motivated the development of an enriched version. This talk has three goals: (1) to introduce the definition of a cofunctor enriched in a distributive monoidal category; (2) examine the duality between enriched functors and cofunctors and state what it means for them to be compatible; (3) discuss several examples of enriched cofunctors for various bases of enrichment, including enrichment in weighted sets. This talk is based on joint work with Matthew Di Meglio (https://arxiv.org/abs/2209.01144).

Samuel Mimram (LIX) – Division by 2, in homotopy type theory
28 September 2022 at 16:00 in Grace Hopper

Natural numbers are isomorphism classes of finite sets and one can look for operations on sets which, after quotienting, allow recovering traditional arithmetic operations. Moreover, from a constructivist perspective, it is interesting to study whether those operations can be performed without resorting to the axiom of choice (the use of classical logic is usually necessary). Following the work of Bernstein, Sierpiński, Doyle and Conway, we study here “division by two” (or, rather, regularity of multiplication by two). We provide here a full formalization of this operation on sets, using the cubical variant of Agda, which is an implementation of the homotopy type theory setting, thus revealing some interesting points in the proof. As a novel contribution, we also show that this construction extends to general types, as opposed to sets. This is joint work with Emile Oleon.

Louis Lemonnier (LMF, University Paris-Saclay) – Central Submonads and Notions of Computation
07 June 2022 at 14:00 in Nicole Reine Lepaute

The notion of “centre” has been introduced for many algebraic structures in mathematics. A notable example is the centre of a monoid which always determines a commutative submonoid. Monads (in category theory) can be seen as generalisations of monoids and in this paper we show how the notion of centre may be extended to strong monads acting on symmetric monoidal categories. We show that the centre of a strong monad T, if it exists, determines a commutative submonad Z of T , such that the Kleisli category of Z is isomorphic to the premonoidal centre (in the sense of Power and Robinson) of the Kleisli category of T. We provide three equivalent conditions which characterise the existence of the centre of T. While not every strong monad admits a centre, we show that every strong monad on well-known naturally occurring categories does admit a centre, thereby showing that this new notion is ubiquitous. We also provide a computational interpretation of our ideas which consists in giving a refinement of Moggi’s monadic metalanguage. The added benefit is that this allows us to immediately establish a large class of contextually equivalent terms for monads that admit a non-trivial centre by simply looking at the richer syntactic structure provided by the refinement.

Bryce Clarke – An introduction to delta lenses
19 May 2022 at 14:00 in Nicole Reine Lepaute

Delta lenses are functors equipped with a suitable choice of lifts, and were first introduced in 2011 to model so-called bidirectional transformations between systems. In this talk, I will provide an introduction to several category-theoretic perspectives of delta lenses which were developed throughout my PhD research. Categories, functors, and delta lenses organise into a double category, and I will demonstrate how many interesting properties of delta lenses may be studied via this two-dimensional categorical structure.

Cameron Calk – Abstract strategies and formal coherence
21 April 2022 at 14:15 in Nicole Reine Lepaute

Kleene algebra have widespread use in mathematics and computer science, from formal language theory to program correctness. Following formalisations of abstract rewriting results in modal Kleene algebra, globular 2-Kleene algebras were introduced, providing a formal setting for reasoning about coherence proofs in abstract rewriting systems. On the other hand, normalisation strategies give a categorical interpretation of the notion of contracting homotopies, constructed via confluent and terminating rewriting. This approach relates standardisation to coherence results in the context of higher dimensional rewriting systems. In this work, we formalise the notion of normalisation strategy in the setting of globular 2-Kleene algebras. In such structures, normalisation strategies allow us to prove a formal coherence theorem via convergent abstract rewriting.

Aly-Bora Ulusoy – A Really Short Hike Through Model Theoretical Galois Theory
29 March 2022 at 14:00 in Nicole Reine Lepaute

Short talk about the Galois theory applied to models of first-order theories. Using symmetry arguments to express non-computability.

Roman Kniazev – Why should study directed loop spaces?
22 March 2022 at 14:00 in Nicole Reine Lepaute

In the first part of the talk, we will discuss classical links of loop spaces with homotopy and (co)homology, together with recognition principle relating loop spaces and operads. In the second part, we will tentatively introduce analogous constructions and suggest possible developments in the context of directed spaces.