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.
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.
Among the approaches directed towards the analysis of quantitative properties of programs, one can certainly mention the metric approaches and the differential/resource-aware ones. In both, the notion of (non-)linearity in the sense of linear logic plays a central role: the first ones aim at treating program distances, and duplication leads to interpret bounded programs as Lipschitz maps; the second ones aim at directly handling duplication in the syntax, and duplication leads to interpret programs as power series. A natural question is thus whether these two apparently unrelated ways of handling (non-)linearity can be somehow connected. At a first glance, there seems to be a “logarithmic” gap between the two: in metric models n duplications result in a Lipschitz function nx, while in differential models this results in a polynomial x^n, not Lipschitz. The central insight of my talk is that a natural way to overcome this obstacle and bridge these two viewpoints is to consider differential semantics in the framework of tropical mathematics, which is a rich combinatorial counterpart of usual algebraic geometry in tight relation with optimization and computational problems.
I will give an overview of some recent work on applying categorical methods in finite model theory and descriptive complexity. A key idea of a research program started by Abramsky, Dawar et al. in 2017 is that various forms of model comparison game, central to finite model theory, can be encoded as game comonads', i.e. resource-indexed comonads on the category of relational structures. For example, the following ingredients can be captured in a syntax-free way: Ehrenfeucht-Fraïssé games, fragments of first-order logic with bounded quantifier rank, and the combinatorial parameter of tree-depth. This approach covers also finite variable fragments, modal and guarded fragments, and more. The pattern of game comonads has been axiomatised at a general level in terms ofarboreal adjunctions', i.e. adjunctions between an extensional category (typically, in the examples, a category of relational structures) and a resource-indexed family of arboreal' categories. I will illustrate an application of this axiomatic framework to the study ofequi-resource' homomorphism preservation theorems in (finite) model theory, exemplified by Rossman's equirank homomorphism preservation theorem. If time allows, I will also discuss recent work on identifying the expressive power of arboreal adjunctions.
Dans ce séminaire nous étudions des classes d’arbres étiquetés selon différents modèles d’étiquetages croissants. Ces arbres sont utiles dans la modélisation de nombreux processus. Nous adoptons dans nos recherches différents points de vues complémentaires (combinatoire ou probabiliste) afin d’enrichir les résultats connus sur les arbres croissants classiques et de proposer de nouvelles classes d’arbres moins contraintes que les modèles existants dans la littérature.
Un pavage est un recouvrement du plan par des tuiles qui ne se chevauchent pas. On appelle sous-shift un ensemble de pavages qui est invariant par translation et fermé (pour la topologie habituelle sur les pavages). Ici on s’intéresse au cas où il y a un nombre fini de tuiles à translation près, les tuiles sont des losanges, et à chaque fois que deux tuiles sont adjacentes elle partagent soit un unique sommet en commun soit une arête entière en commun. Sur ces pavages, on peut imposer des règles locales (à la manière des tuiles de Wang) en ajoutant des couleurs sur les arêtes des tuiles avec la règle que deux tuiles qui partagent une arête doivent avoir la même couleur pour cette arête. Dans ce cas, pour une même tuile géométrique, on peut avoir plusieurs copies avec des couleurs différentes sur les arêtes. Étant donné un sous-shift X de pavages par losanges, le problème du domino sur X prend en entrée un ensemble fini de règles locales F et renvoie Vrai si il existe un pavage de X qui respecte les règles locales F et Faux dans le cas contraire. Ce problème est co-Récursivement-Énumérable-complet et nous allons présenter une réduction many-one depuis le problème du domino classique sur les tuiles de Wang.
This talk has three parts. First, I want to explain how monoid acts can be viewed as models of computation. Second, I will sketch my thesis work on categories of actions of topological monoids. Third, if there is time, I would like to explain how this work would need to be extended in order to capture the monoid acts from the first part, point out some obstacles that need to be overcome, and give some intuition on what building such a topos-theoretic context could provide. Note that while I will give complexity-theoretic motivation, I want to apply this theory to monoid and group acts of all kinds, so feel free to ask questions about your favourite ones.
The notion of hypergraph has been introduced as a generalization of graphs so that each hyperedge is a subset of the set of vertices, without constraints on its cardinality. A widely investigated problem related both to graphs and to hypergraphs concerns the characterization and reconstruction from their degree sequences. Concerning graphs, this problem has been efficiently solved in 1960 by Erdos and Gallai, while no efficient solutions are possible in the case of hypergraphs, even in the simple case of 3-uniform ones, as shown in 2018 by Deza et al. So, to reduce the NP-hard core of the hypergraph reconstruction problem, we consider a class of degree sequences defined by Deza et al. that show interesting geometrical and algebraic properties. We propose some ideas on how use those properties to challenge the related reconstruction problem.
En sémantique des langages, l'équivalence contextuelle de programmes est une notion clef, mais sa définition se prête mal à la manipulation, on cherche donc des modèles corrects et complets lui donnant une expression plus pratique. Les jeux et la sémantique interactive sont de tels modèles, applicables à beaucoup de langages et donnant une équivalence coïnductivement définie. Dans cette présentation je vais esquisser visuellement et de manière intuitive un formalisme de jeux général qui se prête bien à la formalisation dans un assistant de preuve. Je vais également décrire différents genres d'arbres inductifs et coïnductifs ainsi qu'une manière pratique de construire des jeux à partir de composants plus élémentaires.
In this seminar, I will focus on the characterisation of bijective digitized rotations and reflections. Although the characterisation of bijective digitized rotations in 2D is well known, the extension to 3D is still an open problem. A certification algorithm exists that allows to verify that a digitized 3D rotation defined by a quaternion is bijective. In this seminar, we show how we use geometric algebra to represent a bijective digitized rotation as a pair of bijective digitized reflections. Visualization of bijective digitized reflections in 3D using geometric algebra leads to a conjectured characterization of 3D bijective digitized reflections and, thus, rotations. So far, any known quaternion that defines a bijective digitized rotation verifies the conjecture. An approximation method of any 3D digitized reflection by a conjectured bijective one is also proposed. Some experimental results will be shown with DGtal.