TBA
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
Let d, k be fixed coprime positive integers with min{d, k} > 1. A class of polynomial-exponential Diophantine equations of the form x^2 + d^y = k^z , x, y, z ∈ Z+ (1) is usually called the generalized Ramanujan-Nagell equation. It has a long history and rich content. In 2014, N. Terai discussed the solution of (1) in the case d = 2k − 1. He conjectured that for any k with k > 1, the equation x^2 + (2k − 1)^y = k^z , x, y, z ∈ Z+ (2) has only one solution (x, y, z) = (k − 1, 1, 2). The above conjecture has been verified in some special cases. In this work, firstly, using the modular approach, we prove that if k ≡ 0 (mod 4), 30 < k < 724 and 2k − 1 is an odd prime power, then under the GRH, the equation (2) has only one positive integer solution (x, y, z) = (k − 1, 1, 2). The above results solve some difficult cases of Terai’s conecture concerning the equation (2). Secondly, using various elementary methods in number theory, we give certain criterions which can make the equation (2) to have no positive integer solutions (x, y, z) with y ∈ {3, 5}. These results make up the defiency of the modular approach when applied to (2). This is a joint work with Maohua Le and Elif Kızıldere Mutlu.
[English version below]
Cet atelier vise à réunir les doctorants et les chercheurs sur le thème des Equations Diophantiennes et des Equations Algébriques, avec pour objectif l'étude de leurs solutions. Dans une première partie, les exposés sont consacrés à plusieurs types d'équations Diophantiennes :
In a second Part, we study the geometry of the solutions of a class of almost-Newman lacunary polynomials, constructed on trinomials, with coefficients 0, -1,+1. We show the links with
Rényi dynamical systems of numeration and the problem of the nontrivial minoration of the Mahler measure of reciprocal algebraic integers which are real, nonzero and not roots of unity.
Website and programme: https://diophantlehmer.sciencesconf.org/.
TBA
Squier's coherence theorem and its generalisations provide a categorical interpretation of contracting homotopies via confluent and terminating rewriting. In particular, this approach relates standardisation to coherence results in the context of higher dimensional rewriting systems. On the other hand, modal Kleene algebras (MKAs) have provided a description of properties of abstract rewriting systems, and classic (one-dimensional) consistency results have been formalised in this setting. In this talk, I will recall the notion of higher Kleene algebra, introduced as an extension of MKAs, and which provide a formal setting for reasoning about (higher dimensional) coherence proofs for abstract rewriting systems. In this setting, I will describe and sketch a proof of the Church-Rosser theorem with higher-dimensional witnesses, and briefly explain how Squier's coherence theorem is formalised.