I will present an algebraic approach to stochastic graph-rewriting. Rules are seen as particular elements of an algebra of “diagrams”: the diagram algebra D. Diagrams can be thought of as formal computational traces represented in partial time. They can be evaluated to normal diagrams (each corresponding to a rule) and generate an associative unital non-commutative algebra of rules: the rule algebra R. Evaluation becomes a morphism of unital associative algebras which maps general diagrams in D to normal ones in R. In this algebraic reformulation, usual distinctions between graph observables (real-valued maps on the set of graphs defined by counting subgraphs) and rules disappear. Actual graph-rewriting is recovered as a canonical representation of the rule algebra as linear operators over the vector space generated by (isomorphism classes of) finite graphs. This shift of point of view, away from its canonical representation to the rule algebra itself, has unexpected consequences. We find that natural variants of the evaluation morphism map give rise to concepts of graph transformations hitherto not considered. This is joint work with N. Behr and V. Danos.
La reformulation du système Euler 2d incompressible sous la forme d'une inclusion différentielle par De Lellis et Székelyhidi (cf. e.g. Bull. Amer. Math. Soc. vol. 49, 347-375) a permis d'appliquer le h-principe à plusieurs familles d'équations de la mécanique des fluides en 2d. De telles techniques fournissent alors une myriade de solutions faibles, indiquant que le problème de Cauchy est mal posé au sens de Hadamard. Pour le système compressible isentropique 2d, des conditions suffisantes pour l'apparition de ces solutions non-standard'' peuvent s'exprimer sous la forme de relations algébriques (évoquant un peu le théorème de Lax), simplifiant beaucoup leur mise en œuvre. Ainsi, il est possible de construire explicitement, dans le cas $gamma=3$, des données initiales Lipschitz générant une infinité de solutions faibles après l'apparition du choc. Qu'en est-il de la situation sur le plan numérique ? En suivant des indications issues de certaines publications de P.L. Roe dans les années 90's, on observe que plusieurs schémas basés sur le splitting dimensionnel font apparaitre des tourbillons aux endroits où les oscillations doivent se développer dans les solutions non-standard exactes. Tout ceci semble être cohérent avec certaines caractéristiques spécifiques à ce type de solutionssurprenantes''. (joint work with Dr. Elisabetta Chiodaroli, with assistance from Drs. Denise Aregba and Roger Kappeli)
Dans ce travail, on s’intéresse à des configurations optimales de ressources (typiquement des denrées alimentaires) nécessaires à la survie d’une espèce, dans un espace fermé. A cette fin, nous utilisons un modèle dit logistique pour décrire l’évolution de la densité d’individus constituant cette population. Cette équation fait intervenir une fonction représentant la répartition hétérogène (en espace) des ressources. La question principale traitée dans cet exposé peut se formuler ainsi : comment répartir de façon optimale des ressources dans un habitat ? Elle est reformulée comme un problème extremal de valeur propre, dans lequel on cherche à minimiser la valeur propre principale d’un opérateur par rapport au domaine occupé par les ressources. Nous présenterons dans cet exposé de nouveaux résultats complétant l’analyse de ces problèmes, tels que la caractérisation complète des solutions en dimension 1 ou pour des formes d’habitat particulières en dimension supérieure, ainsi que de nombreuses propriétés qualitatives. Il s'agit de travaux en cours, en collaboration avec Jimmy Lamboley (univ. Paris Dauphine), Antoine Laurain (univ. Sao Paulo), Grégoire Nadin (univ. Paris 6).
Le but de cet exposé est de présenter certaines des méthodes de dérivation de modèles continus à partir de systèmes de particules. Ce type de modèle s'est beaucoup développé et est très largement sorti du cadre purement physique: modèles multi-agents en économie, dynamique d'opinion en sciences sociales, ou dynamique de cellules/micro-organismes en biologie. Du fait du très grand nombre de particules ou agent, le comportement de ces systèmes est a priori particulièrement complexe. Un des enjeux principaux des dérivations de champ moyen est de comprendre comment la limite vers un modèle continu (équations de Vlasov...) contribue à réduire cette complexité.
Dans cet exposé, on donne quelques versions des inégalités de Lojasiewicz (du gradient et pour la fonction de distance) quand les fonctions considérées sont la fonction de la valeur propre maximale d'une matrice polynomiale symétrique et la fonction de la valeur singulière minimale d'une matrice polynomiale quelconque.
Operational Techniques (Kripke Logical Relations and Environmental/Open/Parametric Bisimulations) have matured enough to become now formidable tools to prove contextual equivalence of effectful higher-order programs. However, it is not yet possible to automate such proofs -- the problem being of course in general undecidable. In this talks, we will see how to take the best of these techniques to design an automatic procedure which is able many non-trivial examples of equivalence, including most of the examples from the literature. The talk will describe the main ingredients of this method: - Symbolic reduction to evaluate of programs, - Transition systems of heap invariants, as used with Kripke Logical Relations, - Temporal logic to abstract over the control flow between the program and its environment, - Circular proofs to automate the reasoning over guarded recursive predicates.
Beaucoup d'applications nécessitent de pouvoir considérer des champs de vitesses de propagation non nécessairement réguliers. Nous montrerons lors de cet exposé comment encoder la possible perte de régularité. Ceci requiert une analyse plus précise de la structure des équations combinée à une nouvelle approche de la compacité de l'équation de continuité par l'introduction de poids appropriés. Cette méthode a été introduite en collaboration avec Pierre-Emmanuel Jabin (CSCAMM, University of Maryland) et a notamment permis de résoudre deux problèmes jusque là encore ouvert: Existence globale de solutions faibles pour Navier-Stokes compressible avec pression thermo-dynamiquement instable et avec tenseur anisotrope. Nous discuterons la méthode, énoncerons les résultats dans leur généralité et présenterons la portée d'une telle méthode sur d'autres applications possibles.
Unification is a central operation in the construction of a range of computational logic systems based on first-order and higher-order logics. First-order unification has a number of properties that dominates the way it is incorporated within such systems. In particular, first-order unification is decidable, unary, and can be performed on untyped term structures. None of these three properties hold for full higher-order unification: unification is undecidable, unifiers can be incomparable, and term-level typing can dominate the search for unifiers. The so-called pattern subset of higher-order unification was designed to be a small extension to first-order unification that respected the basic laws governing λ-binding (the equalities of α, β, and η-conversion) but which also satisfied those three properties. While the pattern fragment of higher-order unification has been popular in various implemented systems and in various theoretical consideration, it is too weak for a number of applications. In this paper, we define an extension of pattern unification that is motivated by some existing applications and which satisfies these three properties. The main idea behind this extension is that the arguments to a higher-order, free variables can be more than just distinct bound variables: they can also be terms constructed from (sufficient numbers of) such variables using term constructor and where no argument is a subterm of any other argument. We show that this extension to pattern unification satisfies the three properties mentioned above.
In this talk we start by introducing the Euler and the original Green-Naghdi systems for the propagation of internal waves of two immiscible, ideal, incompressible irrotational fluids under the shallow water hypothesis. After we introduce different new asymptotic models in the Green-Naghdi regime. We will discuss and compare qualitative proprieties of this different models regarding, inter alia, their frequency dispersion propriety and its influence on the high-frequency Kelvin-Helmholtz instabilities. All our new asymptotic models are fully justified.
It might appear that solving initial value problems in the past'' is of little interest at an institution dedicated toinventing the future.'' However, this impression is deceiving. It is actually of great interest to know how the present influences the future or whether it impacts the future at all. In this context, backward uniqueness (inverting the future) becomes of paramount significance. As is taught in every beginning course on complex analysis, the modulus of an analytic function on a bounded domain has its maximum on the boundary. The Phragmen-Lindeloef theorem extends this result to unbounded regions, under the assumption of a suitable growth condition at infinity. In this talk, it will be shown how the Phragmen-Lindeloef theorem can be used to prove backward uniqueness for linear partial differential equations. Examples include problems which in a sense are perturbations of cases where backward uniqueness does not hold. In particular, we shall show how backward uniqueness can be obtained for the linearized equations of compressible fluid flow and for the damped wave equation with absorbing boundary conditions.
Je vais présenter un problème d'estimée locale en zéro dans des quotients d'anneaux de séries algébriques. La question consiste à relier l'ordre d'annulation d'un polynôme modulo un idéal au degré de ce polynôme. Nous considérerons aussi le cas de l'ordre d'une série algébrique. Finalement nous montrerons comment ces estimées locales permettent de ``contrôler'' la transcendance des solutions d'équations linéaires à coefficients séries algébriques, solutions pour lesquelles des contraintes de support sont imposées. Ce type d'équations apparaît naturellement en combinatoire ou en théorie des singularités.
Thomas Streicher has reformulated Krivine's notion of classical realizability into abstract Krivine structures and showed that from any such structure one can build a tripos out of it. They are called Krivine triposes and form a subclass of relative realizability triposes in the sense of van Oosten and Hofstra. In this talk, I will present a characterization of those Krivine triposes, indeed, they are exactly boolean subtriposes of relative realizability triposes. I will also talk about a concrete construction of non-localic Krivine triposes. These results are from my master thesis supervised by Jaap van Oosten.
La conjecture de Yano (1982) prédit les racines du polynôme de Bernstein générique d'un germe de courbe plane irréductible. Je vais expliquer les idées de la preuve dans le cas de deux paires de Puiseux et monodromie à valeurs propres distinctes. C'est un travail commun avec Enrique Artal Bartolo, Ignacio Luengo et Alejandro Melle-Hernandez (2016).
At POPL'96, Hughes, Pareto and Sabry presented an approach to the termination of closed ML-like programs based on type-checking and the abstract interpretation of a semantic notion of size. This approach was then extended by several authors to open terms and more complex type systems. In the first part, I will show how it can be extended in other directions: arbitrary user-defined notions of size and rewriting-based function definitions. In the second part, I will show how the decidability of type-checking (with size-induced subtyping) can be reduced to the existence, in the size algebra, of a smallest solution for any solvable set of inequalities, and show it for the successor algebra (which is enough to subsume Coq termination checker for instance).
Les réseaux de nano-fils ferromagnétiques représentent maintenant dans le domaine de la nano-électronique. Les propriétés géométrique de ces objets conditionnent la dynamique des charges magnétiques qui peuvent ainsi être piégées et être utilisées dans les cadre de systèmes de stockage d’information particulièrement stables. Dans cet exposé, nous proposerons un aperçu des modèles existants de nano-fils vus comme structures asymptotiques d’objets tridimensionnels. Ensuite, nous nous concentrerons sur la modélisation des connexions entre objets et la version discrète du modèle ainsi obtenu.
In this talk I will present some recent work, with H. Michalewski, on the study of an extension of MSO on infinite trees with the so-called ``measure quantifier''. This kind of research is motivated, as I will discuss, by a long-standing open problem in the field of verification of probabilistic programs. I will state a negative (i.e., undecidability) result but also present some interesting (currently) open problems.
On montre que toute famille de singularités analytiques, réelles ou complexes, équisingulière au sens de Zariski, peut être trivialisée par un homeomorphisme semi-algébrique, arc-analytique, et analytique par rapport au paramètre. Cela montre en particulier la conjecture de fibration de Whitney : l’existence, pour toute variété analytique complexe, d’une stratification qui possède localement un feuilletage (w)-régulier. Une telle stratification peut être construite de manière algorithmique. (travail en collaboration avec Laurentiu Paunescu)
We prove that if a linear equation, whose coefficients are continuous rational functions on a nonsingular real algebraic surface, has a continuous solution, then it also has a continuous rational solution. This is known to fail in higher dimensions. (Joint work with K. Kurdyka)