Team seminar
Logic, Computer Science, and Discrete Mathematics

Organiser: Sébastien Tavenas.

Lien ical.

Grégory Chichery, LIS, Aix-Marseille Université. June 20, 2024, 10 a.m. TLR limd
Lifting final coalgebras and initial algebras, a reconstruction

Many categorical models of linear logic with fixed points arise as total categories over the category Rel of sets and relations. They are form ∫Q, the Grothendieck category for a functor Q : Rel -> Pos. We will define the concepts of fixed points and Grothendieck category and then we give a result to lift functor from the base category to the total category and studies also how to lift fixed points. In particular, the category of coalgebras for the lifted functor is a total category, and when Q factors through SLatt, the category of posets with joins and maps that preserve them, we found the same result.

Kave Salamatian, LISTIC, Université Savoie Mont Blanc. June 13, 2024, 10 a.m. TLR limd
Ironing the Graphs: Toward a Correct Geometric Analysis of Large-Scale Graphs

Graph embedding approaches attempt to project graphs into geometric entities, {\em i.e.}, manifolds. At its core, the idea is that the geometric properties of the projected manifolds are helpful in the inference of graph properties. However, the choice of the embedding manifold is critical and, if incorrectly performed, can lead to misleading interpretations due to incorrect geometric inference. We argue that the classical embedding techniques cannot lead to correct geometric interpretation as the microscopic details, {\em e.g.}, curvature at each point, of manifold, that are needed to derive geometric properties in Riemannian geometry methods are not available, and we cannot evaluate the impact of the underlying space on geometric properties of shapes that lie on them. We advocate that for doing correct geometric interpretation the embedding of a graph should be done over regular constant curvature manifolds. To this end, we present an embedding approach, the discrete Ricci flow graph embedding (dRfge) based on the discrete Ricci flow that adapts the distance between nodes in a graph so that the graph can be embedded onto a constant curvature manifold that is homogeneous and isotropic, {\em i.e.}, all directions are equivalent and distances comparable, resulting in correct geometric interpretations. A major contribution of this paper is that for the first time, we prove the convergence of discrete Ricci flow to a constant curvature and stable distance metric over the edges. A drawback of using the discrete Ricci flow is the high computational complexity that prevented its usage in large-scale graph analysis. Another contribution of our work is a new algorithmic solution that makes it feasible to calculate the Ricci flow for graphs of up to 50k nodes, and beyond. The intuitions behind the discrete Ricci flow make it possible to obtain new insights into the structure of large-scale graphs.

Krzysztof Worytkiewicz, LAMA. May 30, 2024, 10 a.m. TLR limd
Implicative Assemblies

Implicative algebras, recently discovered by Miquel, are combinatorial structures unifying classical and intuitionistic realizability as well as forcing. In this talk we introduce implicative assemblies as sets valued in the separator of an underlying implicative algebra. Given a fixed implicative algebra A, implicative assemblies over A organise themselves in a category AsmA with tracked set-theoretical functions as morphisms. We show that AsmA is a quasitopos with a natural numbers object (NNO).

Pierre-Étienne Meunier, . May 16, 2024, 10 a.m. 8B-232 limd
Projet Pijul, un système de contrôle de versions

Comment un résultat de catégories a inspiré une solution aux problèmes de performance de Darcs. Darcs est un système de contrôle de versions sorti en 2005, basé sur des patchs, ce qui le rendait extrêmement simple à utiliser et particulièrement rigoureux, en particulier dans sa gestion des conflits. Seul problème, il prenait parfois un temps exponentiel en la taille de l'histoire pour son opération la plus courante (appliquer des patchs). Je vous expliquerai comment nous avons résolu le problème, en utilisant des catégories et des structures de données purement fonctionnelles, pour concevoir un algo en temps logarithmique pour tous les cas (sauf un cas dégénéré en temps linéaire).

Le résultat est un système déterministe (ce qui le distingue de tous les autres outils de contrôle de versions), facile à apprendre et à utiliser, tout en passant à des échelles qu'aucun autre système de contrôle de versions distribué ne peut atteindre.

Colin Weill-Duflos, LAMA. March 21, 2024, 10 a.m. TLR limd
Digital Calculus Frameworks and Comparative Evaluation of their Laplace-Beltrami operators

In a first part I'll will broadly cover the topic of what the Laplace- Beltrami is, its different characterization and its many uses in computer graphics.

Then I'll cover our works on the topic of building this operator (along with a wider digital calculus framework) on digital surfaces (boundary of voxels). These surfaces cannot benefit directly from the classical mesh calculus frameworks. In our recent work, we propose two new calculus frameworks dedicated to digital surfaces, which exploit a corrected normal field. First we build a corrected interpolated calculus by defining inner products with position and normal interpolation in the Grassmannian. Second we present a corrected finite element method which adapts the standard Finite Element Method with a corrected metric per element. Experiments show that these digital calculus frameworks seem to converge toward the continuous calculus, offer a valid alternative to classical mesh calculus, and induce effective tools for digital surface processing tasks.

Adrienne Lancelot, IRIF, Université de Paris. March 7, 2024, 10 a.m. TLR limd
Normal Form Bisimulations by Value

Normal form bisimilarities are a natural form of program equivalence resting on open terms, first introduced by Sangiorgi in call-by-name. The literature contains a normal form bisimilarity for Plotkin’s call-by-value 𝜆-calculus, Lassen’s enf bisimilarity, which validates all of Moggi’s monadic laws and can be extended to validate 𝜂. It does not validate, however, other relevant principles, such as the identification of meaningless terms—validated instead by Sangiorgi’s bisimilarity—or the commutation of lets. These shortcomings are due to issues with open terms of Plotkin’s calculus. We introduce a new call-by-value normal form bisimilarity, deemed net bisimilarity, closer in spirit to Sangiorgi’s and satisfying the additional principles. We develop it on top of an existing formalism designed for dealing with open terms in call-by-value. It turns out that enf and net bisimilarities are incomparable, as net bisimilarity does not validate Moggi’s laws nor 𝜂. Moreover, there is no easy way to merge them. To better understand the situation, we provide an analysis of the rich range of possible call-by-value normal form bisimilarities, relating them to Ehrhard’s relational model.

Lê Thành Dũng Nguyễn, LIP, ENS Lyon. Feb. 22, 2024, 10 a.m. TLR limd
Implicit automata in typed λ-calculi I: aperiodicity in a non-commutative logic

We give a characterization of star-free languages (a well-known subclass of regular languages) in a λ-calculus with support for non-commutative affine types (in the sense of linear logic), via the algebraic characterization of the former using aperiodic monoids. This was the first result in a research program that Cécilia Pradic (Swansea University) and I have carried out since my PhD, on which I will say a few words.

Tom Hirschowitz, . Feb. 15, 2024, 10 a.m. 8D-104 Iseran limd
A semantic notion of inference rule for (dependent, quantitative) type theory

Type theory is a family of formal systems ranging from programming language semantics to the foundations of mathematics. In practice, type theories are defined by means of “inference rules”. Everyone in the community understands them to some extent, but they do not have any commonly accepted rigorous interpretation. Or, rather, they have several interpretations, none of which is entirely satisfactory.

In this work, after a brief overview of the literature, we introduce a rigorous, semantic notion of inference rule, our thesis being that most syntactic inference rules written in practice may be directly interpreted in this framework. If time permits, we will sketch how this covers quantitative type theories.

This is joint work in progress with André Hirschowitz and Ambroise Lafont.

Jacques-Olivier Lachaud, LAMA, Chambéry. Feb. 8, 2024, 10 a.m. TLR limd
Michela Ascolese, University of Florence. Jan. 18, 2024, 11 a.m. TLR limd
Polytime algorithms for the reconstruction of 3-uniform hypergraphs

I describe a P-time heuristic to reconstruct a subclass of degree sequences of 3-uniform hypergraphs. The heuristic bases on some geometrical properties of the involved hypergraphs and also produces a small set of ambiguous hyperedges that has to be individually considered.

Andrea Frosini, University of Florence. Jan. 18, 2024, 10 a.m. TLR limd
On the reconstruction of 3-uniform hypergraphs from unique degree sequences

We consider the problem of detecting and reconstructing degree sequences of 3-uniform hypergraphs. The problem is known to be NP-hard, so some subclasses are inspected in order to detect instances that admit a P-time reconstruction algorithm. Here, I consider instances having specific numerical patterns and I show how to easily reconstruct them.

Nacim Oijid, LIRIS , Université Lyon 1. Jan. 11, 2024, 10 a.m. TLR limd
Complexity of Maker-Breaker Games on edge sets of graphs

We initiate the study of the algorithmic complexity of Maker-Breaker games played on edge sets of graphs for general graphs. We mainly consider three of the big four such games: the connectivity game, perfect matching game, and H-game. Maker wins if she claims the edges of a spanning tree in the first, a perfect matching in the second, and a copy of a fixed graph H in the third. We prove that deciding who wins the perfect matching game and the H-game is PSPACE-complete, even for the latter in graphs of small diameter if H is a tree. Seeking to find the smallest graph H such that the H-game is PSPACE-complete, we also prove that there exists such an H of order 51.

On the positive side, we show that the connectivity game and arboricity-k game are polynomial-time solvable. We then give several positive results for the H-game, first giving a structural characterization for Breaker to win the P4-game, which gives a linear-time algorithm for the P4-game. We provide a structural characterization for Maker to win the K_{1,l}-game in trees, which implies a linear-time algorithm for the K_{1,l}-game in trees. Lastly, we prove that the K_{1,l}-game in any graph, and the H-game in trees are both FPT parameterized by the length of the game. We leave the complexity of the last of the big four games, the Hamiltonicity game, as an open question.

Clément Blaudeau, Cambium team, Inria Paris. Dec. 7, 2023, 10:15 a.m. TLR limd
Retrofitting OCaml modules, an Fω-inspired approach for a modern module system

ML modules offer large-scale notions of composition and modularity. Provided as an additional layer on top of the core language, they have proven both vital to the working OCaml and SML programmers, and inspiring to other use-cases and languages. Unfortunately, their meta-theory remains difficult to comprehend, and more recent extensions (abstract signatures, module aliases) lack a complete formalization. Building on a previous translation from ML modules to Fω, we propose a new comprehensive description of a significant subset of OCaml modules, including both applicative and generative functors and transparent ascription -- a useful new feature. By exploring the translations both to and from Fω, we provide a complete description of the signature avoidance issue, as well as insights on the limitations and benefits of the path-based approach of OCaml type-sharing.

Greta Coraglia, LUCI Lab, University of Milan. Nov. 30, 2023, 10 a.m. TLR limd
Categorical models of subtyping

We start from categorical semantics of dependent types and propose structural rules involving a new notion of subtyping. We begin by recalling a few classical models, which traditionally have been heavily set-based: this is the case for categories with families, categories with attributes, and natural models. In particular, all of them can be traced back to certain discrete fibrations. We extend this intuition to the case of general, non necessarily discrete, fibrations, and use the newly found structure on the fibers to interpret a form of subtyping. Interestingly, the emerging notion turns out to be closely related to that of coercive subtyping. This is joint work with J. Emmenegger.

Peio Borthelle, . Nov. 23, 2023, 10 a.m. TLR limd
Operational game semantics, certified in Coq

Une sémantique des jeux opérationelle certifiée en Coq

La sémantique des jeux opérationelle (OGS) est une méthode pour transformer l'évaluateur d'un langage de programmation en une sémantique correcte vis-à-vis de l'équivalence contextuelle, basée sur l'interprétation des termes ouvert comme des "stratégies" pour interagir avec n'importe quel environnement d'exécution. Avec mes encadrants de thèse j'ai développé une formalisation en Coq de cette construction en s'abstrayant légèrement des détails syntaxiques du langage considéré. Je vais commencer par motiver et présenter le fonctionnement intuitif des OGS, puis donner un aperçu de nos contributions. Et enfin pour les plus courageux détailler un point technique de la preuve de correction: la propriété "d'avancement" de la composition d'une stratégie active avec une stratégie passive.

Operational game semantics, certified in Coq

Operational game semantics (OGS) is a method to transform an evaluator for a programming language into a semantic space which is correct with respect to contextual equivalence. It is based on interpreting open terms as "strategies" to interact with any execution environment. With my doctoral advisors I have developped a Coq formalization of this construction, abstracting away some syntactic details of the considered language. I will start this talk by motivating and presenting OGS intuitively, and will then give a high level view of our contributions. Finally for the bravest I will detail a technical point of the correction proof, namely the "progress" property of the composition of an active strategy with a passive strategy.

Valentin Gledel, . Nov. 9, 2023, 10 a.m. TLR limd
Complexité des jeux positionels.

Complexité des jeux positionels.

Les jeux positionnels sont des jeux à deux joueurs joués sur un hypergraphe. Les joueurs sélectionnent alternativement des sommets de l'hypergraphe et les conditions de victoires dépendent du remplissage des hyperarêtes. Le Morpion est le plus célèbre exemple de jeu positionnel avec les lignes, colonnes et diagonales formant les hyperarêtes et le premier joueur à remplir une hyperarête gagnant la partie. Les jeux positionnels ont été étudiés depuis leur introduction par Hales et Jewett en 1963, et ont été popularisés par Erdős et Selfridge en 1973. La version Maker-Breaker des jeux positionnels, la version la plus étudiée, a été prouvée comme étant PSPACE-complet par Schaefer en 1978, mais de nombreux problèmes restent ouverts concernant la complexité des jeux positionnels. En particulier, la complexité de la version Avoider-Enforcer restait ouverte, et les jeux positionnels et leur complexité étaient peu étudiés sur des classes restreintes d'hypergraphes. Dans cette présentation, nous allons commencer par introduire les jeux positionnels et donner un aperçu des principaux résultats du domaine. Puis, nous esquisserons une preuve de la PSPACE-complétude de la version Avoider-Enforcer. Enfin, nous conclurons cette présentation en étudiant les jeux positionnels en lien avec des problèmes de graphes et la complexité de tels problèmes.

Complexity of positionnal games

Positional games are two-player games played on a hypergraph. The players alternate selecting vertices of the hypergraph, and the winning conditions depend solely on the filling of the hyperedges. Tic-tac-toe is a famous example of a positional game, with the rows, columns, and diagonals forming the hyperedges and the first player to fill a hyperedge winning the game. Positional games have been studied since their introduction by Hales and Jewett in 1963, and were popularized by Erdős and Selfridge in 1973. Even though the Maker-Breaker convention, the most studied form of positional games, was proven to be PSPACE-complete by Schaefer in 1978, many problems remained open regarding the complexity of positional games. In particular, the complexity of the Avoider-Enforcer convention remained open, and positional games and their complexity were little considered on more restricted classes of hypergraphs. This presentation will begin with an introduction to positional games, providing an overview of the main results in the field. Then, we will give a proof sketch for PSPACE-completeness of the Avoider-Enforcer game. Finally, we will conclude this presentation by studying positional games in relation to graph problems and the complexity of such problems.

Ralph Sarkis, LIP, ENS Lyon. Oct. 26, 2023, 10 a.m. TLR limd
Universal Quantitative Algebra

Universal algebra and equational logic stand as well-established tools for reasoning about programs and program equivalences. Universal quantitative algebra and quantitative equational logic were introduced in 2016 as a natural extension of these to reason about program distances. I will present the result of a few years of work with Matteo Mio and Valeria Vignudelli on improving and streamlining the original paper.

A central result in the classical realm is the correspondence between algebraic theories and (finitary) monads on the category Set. While a complete axiomatization of monads corresponding to quantitative algebraic theories remains out of reach, I will show every lifting of a monad on Set with an algebraic presentation can be presented by a quantitative algebraic theory. This result encompasses all currently known applications.

Yoann Barszezak, LAMA. Oct. 12, 2023, 10 a.m. TLR limd
Nerves of shapely monads and bicategories

Nerve theorems offer combinatorial characterisations of algebraic structures. Categorists have come up with nerve theorems for increasingly general classes of structures. The talk will consist of a gentle introduction to this theory, focusing on nerve theorems for so-called familial and analytic monads. The motivation for these monads is that they lend themselves well to defining structures graphically, in a suitable sense. Time permitting, we will touch upon work in progress towards defining higher-dimensional structures using this technology.

Lison Blondeau, LIS, Marseille. Oct. 5, 2023, 10 a.m. TLR limd
Strategies as Resource Terms, and their Categorical Semantics

As shown by Tsukada and Ong, normal (extensional) simply-typed resource terms correspond to plays in Hyland-Ong games, quotiented by Melliès’ homotopy equivalence. Though inspiring, their proof is indirect, relying on the injectivity of the relational model w.r.t. both sides of the correspondence — in particular, the dynamics of the resource calculus is taken into account only via the compatibility of the relational model with the composition of normal terms defined by normalization.

In the present talk, we revisit and extend these results. Our first contribution is to restate the correspondence by considering causal structures we call augmentations, which are canonical representatives of Hyland-Ong plays up to homotopy. This allows us to give a direct and explicit account of the connection with normal resource terms. As a second contribution, we extend this account to the reduction of resource terms: building on a notion of strategies as weighted sums of augmentations, we provide a denotational model of the resource calculus, invariant under reduction. A key step — and our third contribution — is a categorical model we call a resource category, which is to the resource calculus what differential categories are to the differential λ-calculus.

Damien Pous, Lyon. June 29, 2023, 2 p.m. limd
Reductions for Kleene algebra with top (jww Jana Wagemaker, after discussions with Paul Brunet, Amina Doumane & Jurriaan Rot)

We will prove two completeness results for Kleene algebra with a top element, with respect to languages and binary relations. While the equational theories of those two classes of models coincide over the signature of Kleene algebra, this is no longer the case when we consider an additional constant ``top'' for the full element. Indeed, the full relation satisfies more laws than the full language, and we show that those additional laws can all be derived from a single additional axiom. The proofs combine models of closed languages, reductions, a bit of graphs, and a bit of automata.