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.
Étant donné deux fonctions réelles $f$ et $g$, qui engendrent deux structures o-minimales, respectivement $M(f)$ et $M(g)$, on dira que $f$ est définissable à partir de $g$ si le graphe de $f$ appartient à $M(g)$. On peut considérer la non-interdéfinissabilité de deux fonctions o-minimales $f$ et $g$ comme une sorte d'indépendance fonctionnelle, qui généralise celle différentielle-algébrique. La motivation initiale de ce travail est la question suivante : soient $f$ la restriction à la demi-droite réelle ${ x: x>1}$ de la fonction $\zeta$ de Riemann et $g$ la restriction à la demi-droite réelle positive de la fonction Gamma d'Euler (deux fonctions o-minimales). Est-ce que $f$ est définissable à partir de $g$ ? Pour répondre (négativement) à cette question (et à d'autres questions dans le même esprit), nous montrons que l'on peut plonger le corps des germes de fonctions définissables dans une structure o-minimale $M$ engendrée par une classe quasi-analytique généralisée, dans un corps de séries logarithmico-exponentielles, et que l'image $F$ d'un germe $f$ par ce plongement est un développement trans-asymptotique de $f$ dans une échelle asymptotique appropriée. En étudiant les propriétés de tels objets formels $F$ (support, coefficients, convergence...) on peut déduire que certains germes réels ne sont pas définissables dans la structure $M$. (travail en cours avec J.-P. Rolin et P. Speissegger).
We state and prove a version of Kurdyka-Lojasiewicz inequality for a mapping definable in an o-minimal structure, with values in $\R^k$, $k>1$. It implies a uniform bound for the measure of submanifolds transversal to the fibers.
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.
Motivés par les travaux de Batyrev sur la correspondance de McKay, Denef et Loeser ont défini une mesure motivique sur les variétés algébriques $X$ avec des singularités quotient, la mesure d'orbifold. Le volume de cette mesure est lié à la cohomologie orbifold de $X$.
Dans un travail en cours avec Michael Groechenig et Paul Ziegler nous étendons cette théorie aux quotients de variétés lisses par des groupes réductifs. Il n'y a pas d'analogue de la cohomologie d'orbifold connu en général, mais pour certaines classes d'espaces de modules, notamment pour des fibrés vectoriels sur une courbe, le bon analogue semble être la cohomologie dite BPS issue de la théorie de Donaldson-Thomas.
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.
La modélisation et la simulation d’écoulements diphasiques constituent un sujet de recherche important, notamment pour leurs applications en sûreté nucléaire. Dans certains scenarii d’accidents interviennent des écoulements très hétérogènes, constitués d’eau liquide et de bulles d’air et de vapeur. Afin de modéliser de tels écoulements, on privilégie des modèles moyennés, donnant une description macroscopique des écoulements, la description à l’échelle des interfaces eau-gaz étant hors portée. Cependant connaître les propriétés de l’interface, en particulier l’évolution de l’aire interfaciale et de la tension de surface, demeure important. Le but de cet exposé est de présenter deux manières de dériver des modèles moyennés d’écoulements diphasiques avec tension de surface, la première par une méthode d’homogénéisation, la seconde par un principe d’Hamilton.
In this talk, I will show that smooth functions on convex bodies in Euclidean space, whose sequence of derivatives is dominated by a suitable given weight sequence of positive real numbers, have many polynomial-like properties. Let us call them “controlled differentiable functions” for brevity. Functions in quasianalytic Denjoy--Carleman classes are examples, but sometimes the results also apply in the non-quasianalytic setting.
I will introduce an integer, depending on the given weight sequence, the diameter of the domain, and the sup-norm of the function, which, in analogy to the polynomial degree, allows to express the polynomial-like behavior quantitatively. For instance, I will present a bound on the codimension one Hausdorff measure of the zero set and show that it can be locally parameterized by Sobolev functions. Moreover, I will discuss a Remez-type inequality and several applications for controlled differentiable functions. Many of the results depend only on the derivatives up to some finite order, which can be determined explicitly.
The local parameterization of the zero set by $W^{1,p}$ Sobolev functions is based on joint work with Adam Parusinski in which, for any smooth family of monic polynomials, we determined the optimal order of summability $p \ge 1$ (solely in terms of the degree) such that there is a $W^{1,p}$ choice of the roots.
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.
Je présenterai une introduction à mes articles récents avec Armin Rainer sur la perturbation des polynômes d'une ou plusieurs variables, et avec Guillaume Rond sur la perturbation des opérateurs linéaires. En particulier, nous avons considéré avec A. Rainer les racines de polynômes complexes unitaires d'une variable dont les coefficients dépendent de manière lisse d'un paramètre réel t. Nous avons montré qu'une telle racine, si elle est continue en t, est nécessairement localement absolument continue et nous avons donné une estimation optimale de sa régularité de Sobolev.
Dans un article avec Guillaume Rond, nous avons montré qu’une famille analytique de matrices normales dépendant d'un multiparamètre peut être localement diagonalisée analytiquement si le discriminant de son polynôme caractéristique est à croisement normal. On a un résultat similaire pour la décomposition des valeurs singulières des familles de matrices arbitraires.
La théorie de la perturbation des polynômes et des opérateurs linéaires est motivée par la théorie des équations à dérivées partielles.
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.
A result coming from Dulac, and proved independently by Écalle and Ilyashenko in the 80's, asserts that an analytic vector field in the real plane cannot have a sequence of limit cycles accumulating to a singular point. In this talk, we deal with this problem for analytic vector fields in dimension three, in a non-trivial but not too degenerated situation. Namely, the linear part at the singularity has two non-zero imaginary eigenvalues. We describe completely the distribution of all possible local cycles around the singularity, showing that there are no isolated ones in some neighborhood, which proves Dulac's property. Joint work with Nuria Corral and María Martín.
We investigate the energy decay of hyperbolic system of wave-wave with generalized acoustic boundary conditions in N-dimensional space, with the equations being coupled through boundary connection. First, by spectrum approach combining with a general criteria of Arendt-Batty, we prove that our model is strongly stable. Then, after proving that this system lacks the exponential stability, we establish different type of polynomial energy decay rates provided that the coefficients of the acoustic boundary conditions satisfy some assumptions. Further, we present some appropriate examples and show that our assumptions have been set correctly. Finally, we prove that the obtained energy decay rate is optimal in particular case.
Je vais expliquer une nouvelle preuve d'un théorème de Gabrielov des années 70 concernant le rang d'un germe d'application analytique. Ceci nous permet d'obtenir un résultat plus général que le résultat original de Gabrielov. Je vais montrer ensuite comment cet énoncé nous permet de montrer que l'ensemble des points Nash d'un ensemble sous-analytique est lui-même un ensemble sous-analytique, résultat démontré en 90 par Pawlucki.
La Conjecture de Sard classique prévoit que l’image de toutes les courbes singulières partant d’un point fixé sur une variété équipée d’une structure sous-riemannienne est de mesure nulle. Nous discuterons dans cet exposé d’une conjecture plus faible portant uniquement sur les courbes singulières de rang minimal. Nous expliquerons comment ce problème est relié, dans le cas analytique réel, aux propriétés de certains feuilletages sous-analytiques et présenterons des résultats positifs dans le cas de feuilletages dit « splittable ». Ceci est tiré d’un travail en collaboration avec André Belotto et Adam Parusinski.
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 consider a stochastic individual-based model for the evolution of a population, whose space of possible traits is given by the vertices of a finite graph. The dynamics is driven by births, deaths, competition, and mutations along the edges of the graph. We are interested in the large population limit under a mutation rate given by a negative power of the carrying capacity K of the system. This results in several mutant traits being present at the same time and competing for invading the resident population. We describe the time evolution of the orders of magnitude of each sub-population on the \log K time scale, as K tends to infinity. Using techniques developed in [Champagnat, Méléard, Tran, 2019], we show that these are piecewise affine continuous functions, whose slopes are given by an algorithm describing the changes in the fitness landscape due to the succession of new resident or emergent types. I will illustrate the theorem by examples describing surprising phenomena arising from the geometry of the graph and/or the rate of mutations. If time permits I will finish with an application to the phenomenon of evolutionary rescue.
In this talk, we introduce nonlinear diffusion equations with absorption, in the most general form
∂_t(u) = ∆u^m − |x|^σ u^p, for m > 1 and p > 0.
Looking for solutions to the Cauchy problem in a first part of the talk, we give a brief survey of general facts for the previous equation in the case of the spatially homogeneous absorption σ = 0, related to very singular solutions and finite time extinction of solutions: that is, the existence of a time Te ∈ (0, ∞) such that u(t) ≢ 0 for any t ∈ (0, Te), but u(Te) ≡ 0. In the second and more specialized part of the talk, we present some recent results including well-posedness, instantaneous shrinking of the supports of solutions, non-extinction versus extinction depending on the initial condition, and large time behavior for the general equation with σ > 0 and 0 < p < 1, emphasizing on the importance of the critical exponent σ := 2(1 − p)/(m − 1) and its influence on the dynamics of the equation.
Joint work with Philippe Laurençot (Univ. de Savoie, Chambéry) and Ariel Sánchez (Univ. Rey Juan Carlos, Madrid).
By clustering the polar curves of 2-variable function germs, in the Topological category, one may derive a bijective correspondence of a certain partition of polar quotients. In the case of the Lipschitz category, we explain how this bijective correspondence may be refined in terms of the gradient canyons. We will show how the tracking of the contact orders of the polar arcs and of the roots of a holomorphic 2-variable germ, induces a natural partition of the set of polar arcs into clusters, in such a way that the classical bijective correspondence of branches of topologically right-equivalent function germs induces a bijective correspondence of those clusters. (Clustering polar curves, Topology and its Applications 313 (2022) with P. Migus and M. Tibar.)
Dans cet exposé, nous présentons l'étude numérique du système type Boussinesq d'ordre supérieur/étendu décrivant la propagation des ondes de surface. Une reformulation appropriée équivalente est proposée, rendant le modèle plus approprié pour l'implémentation numérique et significativement amélioré en termes de propriétés dispersives linéaires dans les régimes à haute fréquence grâce à l'ajustement approprié d'un paramètre de correction de dispersion. De plus, nous montrons qu'un intérêt significatif se cache derrière la dérivation d'une nouvelle formulation du système de Boussinesq d'ordre supérieur/étendu qui évite le calcul des dérivées d'ordre supérieur existant dans le modèle. Nous montrons que cette formulation a l'avantage d'un domaine d'application étendu tout en restant stable. Nous développons un schéma de ``splitting'' du second ordre où la partie hyperbolique du système est traitée avec un schéma de volumes finis d'ordre élevé et la partie dispersive est traitée avec un schéma de différences finies. Des simulations numériques sont ensuite réalisées pour valider le modèle et les méthodes numériques.