Séance informelle sur la ludique ou la complexité implicite ou les relations entre ludique et calculs de processus.
About 10 years ago, Boris Shapiro and Michael Shapiro made a remarkable conjecture about real solutions to geometric problems coming from the classical Schubert calculus. While the conjecture remains open, there is truly overwhelming computational evidence supporting it, and Eremenko and Gabrielov proved it for Grassmannians of 2-planes, where the conjecture is the appealing statement that a rational function with only real critical points must be real.
In my talk, I will introduce the Shapiro conjecture and discuss what we know about it. This includes a simple counterexample and a refinement which is supported by massive experimental evidence. This evidence includes tantalizing computations which suggest a strengthening: that a certain discriminant polynomial is a sum of squares, or more generally that it has such an algebraic certificate of positivity.
Un groupe de traces est le quotient d'un groupe libre par des relations de commutation entre certaines lettres. On peut représenter les traces par des tas de pièces colorées. Dans une première partie, nous étudions les groupes de traces d'un point de vue combinatoire et obtenons une formule explicite de la série génératrice d'un groupe de traces, comparable à la formule d'inversion de Möbius pour le monoïde de traces. Dans un deuxième temps, nous utilisons cette formule pour étudier le taux de croissance moyen asymptotique d'un tas de pièces colorées.
We present a new approach to the problem of static typing in languages of the ML family. The basic idea is to generalize the pseudo linear unification algorithm you can use in the Hindley-Milner algorithm. The obtained language is very expressive compared to existing ML implementation and do not require type annotation for many features of ML that usually needs some (like modules, object, ...).
Un ovale d’une courbe algébrique réelle plane est dit pair, s’il est contenu dans un nombre pair d’ovales de la courbe. En 1906, Virginia Ragsdale a conjecturé que pour toute courbe de degré 2k avec p ovales pair,
La théorie de types a été inventée au début du 20eme siècle avec le but d'éliminer les paradoxes qui viennent de l'application d'une fonction à elle-même. Le lambda calcul a été développé (par Church) vers 1930 comme une théorie de fonctions. En 1940, Church ajoutait les types à son lambda calcul. Ces types étaient simples, ce qui veut dire qu'ils n'étaient jamais construits par des lieurs (comme un $lambda$). Alors, on a des termes comme $lambda_{x:T}.B$ (qui sont construits par le lieur $lambda$) mais on n'a pas des lieurs qu'on peut utiliser pour construire un type. Malgré l'influence qu'a connue le lambda calcul typé de Church, sa limitation a aboutit a la création de plusieures théories de types dans la deuxième partie du 20eme siècle. Dans ces calculs, les types sont construits par des lieurs. Dans la plupart de ces calculs, on trouve deux lieurs : le $lambda$ (pour construire des termes) et le $Pi$ (ou $forall$, pour construire des types). Ces deux lieurs nous permettent de distinguer les fonctions (qu'on construit avec les $lambda$s) des types (qu'on construit avec les $Pi$). En plus, dans ces calculs, on permet bien la $beta$-réduction mais pas la $Pi$-réduction. Autrement dit, dans ces calculs on a bien la règle : $(lambda_{x:A}.B)C rightarrow B[x:=C]$ Mais pas la règle : $(Pi_{x:A}.B)C rightarrow B[x:=C]$ En particulier, lorsque $b$ a le type $B$, on donne à $(lambda_{x:A}.b)C$ le type $B[x:=C]$ à la place de $(Pi_{x:A}.B)C$. Il y a quelques extensions puissantes des théorie des types qui donnent le même comportement au $Pi$ qu'au $lambda$ (par exemple, en Automath, dans le langage de programmation Henk de Simon Peyton Jones, etc.). Ca nous aboutit à poser la question : pourquoi distinguer entre le $lambda$ et le $Pi$ lorsque des systèmes comme Automath nous montrent qu'il est plus avantageux de traiter les types exactement comme les termes? Dans cette présentation je décrit un système ou les deux lieurs sont identifiés et je montre que ce système a toutes les propriétés qu'on désire d'un système de typage sauf pour l'unicité des types. Mais je démontre aussi que cette perte de l'unicité des types n'est pas grave parce qu'il y a un isomorphisme entre le typage avec deux lieurs et le typage avec un seul lieur et en plus, tous les différent types d'un même terme, suivent le même modèle.
On appelle circuit tout ensemble de n+2 points entiers dans Zn. Un système polynomial est supporté par un circuit si ses n équations ont pour support commun un circuit dans Zn.
On donne ici des bornes supérieures sur le nombre de solutions réelles d’un tel système en fonction du "rang modulo 2" du circuit et de la dimension de l’espace affine du sous-ensemble minimal du circuit constitué de points affinement dépendants. On montre que ces bornes sont exactes en dessinant des graphes sur la sphère de Riemann, qui sont des exemples de "Dessins d’enfants".
On obtient aussi qu’un tel système a au plus n+1 solutions positives (dont toutes les coordonnées sont strictement positives), et cette borne est exacte. Cette dernière borne n+1 améliore considérablement la borne donnée par le théorème de Khovanskii (théorie des Fewnomials).
We will look at what is involved in formally proving results about languages with binding. We will in particular focus on what we want to prove, what we actually do prove, and what requirements we need to put on the formalisms that we use.
Je présenterai deux résultats concernant le contrôle d’une structure o-minimale par ses ensembles définissables de dimension deux :
- La structure engendrée par les sous-ensembles semi-algébriques de R2 élimine ses quantificateurs (théorème de Tarski-Seidenberg pour les ensembles semi-2-algébriques).
En particulier, il existe une structure o-minimale strictement plus petite que celle des semi-algébriques mais qui définit (exactement) TOUS les ensembles semi-algébriques de R2.
- Considérons une expansion (o-minimale) S du corps des réels qui admet un théorème de décomposition C^{infty}.
S’il existe un n>1 tel que tous les ensembles S-définissables sont en fait semi-algébriques alors S est la structure des semi-algébriques.
On peut ainsi "reconnaître" les structures qui définissent des ensembles non semi-algébriques dès la dimension 2.