Programme
Les exposés jeune chercheur durent 15mn + 5mn de questions. Le programme exact est en cours de construction.
Descriptions des cours
Géométrie de l'interaction
Responsable : Jean-Yves Girard
Le programme de Géométrie de l'Interaction (GdI) visait à construire une interprétation satisfaisante sur le plan mathématique de la dynamique des programmes. Ce programme a connu une première (et inattendue) réalisation en 1988 avec l'interprétation des preuves/programmes par des isométries partielles sur l'espace de Hilbert, et celle de la dynamique au travers de la formule d'exécution qui exprime la solution d'une équation de rétroaction.
Dans les trois niveaux fondationnels de la logique:
- 1. les formules ou niveau de vérité, prouvabilité, cohérence....
- 2. les preuves ou niveau de la fonctionnalité (catégories),
- 3. la dynamique ou niveau de l'élimination des coupures
la GdI se place au plus profond, au niveau 3. D'où la question de l'articulation avec les niveaux plus traditionnels ; ainsi, comment définir la vérité en GdI?
La première GdI était muette à ce sujet. La seconde GdI s'approche davantage de l'esprit des algèbres d'opérateurs (algèbres stellaires et de von Neumann), de façon à analyser
- 1. la vérité;
- 2. l'infini (ou encore : la pérennité, i.e., les exponentielles de la logique linéaire);
- 3. la complexité algorithmique.
Ils semblent que ces trois aspects de la logique (et du calcul) dérivent d'une racine commune, la notion de point de vue, qui s'inspire de celle de mesure en mécanique quantique.
La sophistication des algèbres d'opérateurs devrait à terme induire un renouveau méthodologique dans le domaine ; telle est du moins l'ambition avouée du projet de la GdI.
Références : le Point Aveugle en général; plus particulièrement le tome II, chapitres 18-21 et aussi le cours de Tende (la partie II sera écrite dans qq mois).
Algèbre et géométrie de la réécriture
Responsable : Yves Lafont
Ce cours est une introduction à la théorie de Squier sur les invariants algébriques de la réécriture.
Bibliographie : Y. Lafont, Algebra and Geometry of Rewriting, à paraître dans Applied Categorical Structures
Complexité calculatoire implicite
Responsable : Patrick Baillot
Intervenants : Jean-Yves Moyen, Paulin de Naurois.
La complexité calculatoire implicite a pour objet le calcul à ressources bornées (temps, espace). Il s'agit d'étudier dans le cadre d'un calcul général (lambda-calcul, réécriture) des disciplines de programmation permettant de garantir statiquement et formellement que sur toute entrée, le programme terminera avec une certaine borne en temps ou en espace. L'exemple le plus classique est celui des programmes terminant en temps polynomial (Ptime), et cette branche de recherche s'est développée notamment à partir des travaux de Leivant, Bellantoni et Cook, Jones, Girard...
Dans ce cours nous présenterons les principales approches en complexité implicite, essentiellement pour la caractérisation de la classe Ptime, en présentant leurs fondements théoriques puis les différents critères d'analyse de programmes qu'ils permettent de définir :
- d'une part l'approche basée sur un bridage des structures de contrôle (récursion): récursion primitive ramifiée et quasi-interprétations pour la réécriture;
- d'autre part celle dérivée de la logique linéaire visant à contrôler la réutilisation de ressources: logiques linéaires light et systèmes de types pour la complexité en lambda-calcul.
Pavages, modèles géométriques et calcul
Responsable : Bruno Durand
Intervenants : Emmanuel Jeandel, Grégory Lafitte, Nicolas Ollinger.
Pavages, de l'apériodicité à l'indécidabilité (2h, Nicolas Ollinger)
les jeux de tuiles et les pavages du plan ; la problématique de l'apériodicité (Wang et Berger) ; construction d'un pavage apériodique (Robinson, substitution et auto-similarités) ; calculer dans des pavages, indécidabilités ; application à la dynamique des AC.
Pavages et logique (1h, Emmanuel Jeandel)
pavage comme théorie logique finie ; quasipériodicité et théories complètes ; retour aux théories logiques et au problème de décision de Hilbert ; classes syntaxiques de la logique du premier ordre ; frontière décidabilité/indécidabilité.
Complexité de Kolmogorov et logique (1h, Gregory Lafitte)
premiers éléments de complexité de Kolmogorov ; preuves élémentaires: exemple du Castor affairé ; incomplétude de Gödel à la Chaitin ; retour sur la complexité structurelle des pavages.
Combinatoire algèbrique
Responsable : Florent Hivert
Le but de ce cours est de donner un aperçu de ce que nous pouvons apprendre en exploitant les structures algébriques des objets combinatoires. Les séries génératrices peuvent par exemple nous aider à les dénombrer (combinatoire énumérative). Une autre application possible est la génération aléatoire efficaces d'objets combinatoires, comme les graphes. Elle peut être utilisée dans des algorithmes probabilistes sur ces structures.
Descriptions des exposes
Combinatoire des representations du groupe symetrique
Orateur : Valentin Feray
La représentation régulière du groupe symétrique définit une mesure de probabilité sur les diagrammes de Young d'une taille n donnée, qui converge vers une forme limite quand n tend vers l'infini. On peut étudier cette convergence en regardant les puissances d'une matrice contenant des permutations. Ceci se fait par une approche combinatoire liée aux chemins de Dick et aux statistiques usuelles sur les permutations (nombres de cycles,...).Combinatoire des surpartitions
Orateur : Olivier Mallet
Les surpartitions sont une généralisation des partitions d'entiers. Dans cet exposé, on présente divers résultats relatifs à la combinatoire des surpartitions et d'objets voisins comme les paires de surpartitions et les surpartitions n-colorées.A venir
Orateur : Janvier Nzeutchap
A venirJeux de coloration
Orateur : Adrien Guignard
La résolution des jeux combinatoires à deux joueurs, ou jeux sans hasard, consiste à rechercher un ensemble absorbant dans le \\"graphe d'états\\" du jeu qui, dans notre cas, est sans cycle (on ne peut revenir à une position antérieure). Cet ensemble absorbant est l'ensemble des états (ou positions) perdants pour le joueur suivant.Nous verrons plusieurs exemples de jeux de coloration de sommets, où la règle de base est:
- Partant d'un graphe G et d'un nombre k de couleurs, on colorie le graphe avec les k couleurs
- Le premier joueur ne pouvant plus colorier de sommet est déclaré perdant.
Si l'on se limite à deux joueurs, le problème est de classer les graphes en deux familles: ceux qui offrent au joueur A la possibilité de gagner, et les autres. Nous utiliserons la fonction de Grundy, qui permet de savoir si A peut gagner, qui permet de déterminer les stratégies de jeu, et qui s'exprime en fonction des valeurs de Grundy des composantes connexes du graphe. Comme la résolution de ce problème est exponentiel en fonction de la taille du graphe, et comme aucune heuristique n'est satisfaisante, on se limitera à rechercher des familles dont la fonction de Grundy est soit connue (périodique) , soit calculable en temps polynômial.
Enfin, nous verrons que, dans d'autres jeux de coloration, la fonction de Grundy n'est pas utilisable, et donc la résolution de ceux-ci est encore plus difficile.
Logique lineaire differentielle et concurrence
Orateur : Lionel Vaux
La correspondance de Curry-Howard constitue une voie d'échange majeure entrela théorie de la démonstration et l'informatique théorique, en établissant une
relation forte entre d'un côté les programmes et leurs types, et de l'autre les
preuves et les formules. Tous les paradigmes de calcul ne sont cependant pas
couverts. En particulier, jusqu'à récemment, les primitives de programmation
associées à la théorie de la concurrence, telle qu'exprimée par le pi-calcul
de Milner, sont restées hors du champ de la correspondance preuve-programme.
Des travaux récents ont cependant montré que la logique linéaire de Girard
offrait un cadre pertinent pour tenter d'étendre cette correspondance au
domaine de la concurrence. En particulier, les réseaux différentiels d'Ehrhard
et Regnier permettent de coder la dynamique d'un fragment significatif du
pi-calcul. Ce résultat établi récemment par Ehrhard et Laurent n'est
toutefois pas entièrement satisfaisant d'un point de vue logique: les réseaux
qui codent les processus ne sont pas nécessairement corrects, c'est-à-dire
qu'ils ne représentent pas des preuves.
Il est cependant possible de faire ressortir dans une extension du
lambda-calcul (ce que le pi-calcul n'est décidemment pas) certains
comportements calculatoires caractéristiques de la concurrence dans les
réseaux différentiels. Cette exploration du versant fonctionnel de
l'approche différentielle a pour but de découvrir des calculs
concurrents qui seraient corrects d'un point de vue logique,
c'est-à-dire qui fourniraient une notion de processus concurrents
satisfaisante dans un paradigme des processus comme preuves analogue à
la correspondance de Curry-Howard.
Differential nets : a paradigm of non-determinism?
Orateur : Paolo Tranquilli
Ehrhard and Regnier's differential nets give an elegant symmetrization of Linear Logic, and almost unexpectedly introduce into computation theory seemingly distant mathematical concepts such as derivation and Taylor expansion. On the other hand, the sum (at the base of linearity and differentiation), can also be regarded as a way to treat non-determinism. As links between differential nets and non-deterministic calculi (pi-calculus the foremost one) are established, one wonders if differential Linear Logic and its language, differential nets, could prove to bring insight into non-determinism as Linear Logic and proof-nets have done for deterministic computation.Between interaction and semantics : visible acyclic nets
Orateur : Michele Pagani
Proof-nets are a graph-theoretical representation of the linear logic proofs. Recently proof-nets have been extended to differential interaction nets (DIN), introducing differential operators for the exponentials.We find out that this extension allows a surprising correspondence between cut-elimination, acyclicity and finiteness spaces (a denotational semantics at the base of DIN).
To sum up, consider a cut-free net R with exactly one conclusion C, our results prove that the following conditions are equivalent:
1. for every visible acyclic net R' with one conclusion notC, the cut between R and R' has a normal form
2. R is visible acyclic
3. R is a finitary relation in the finiteness space associated with C
These equivalences provide a generalization of the ones in the main theorems of the theory of linear logic proof-nets, namely: Bechét's theorem (1 --> 2), weak normalization theorem (2 --> 1), semantic soundness theorem (2 --> 3) and Retoré's theorem (3 --> 2). Above all, it discloses a deep unity in DIN between normalization, visible acyclicity and finiteness spaces, which was present (even if never actually remarked) only in the multiplicative fragment of linear logic.
Autour des graphes de partage
Orateur : Stephane Gimenez
Une approche neutre de la preuve de la refutation dans MALL
Orateur : Olivier Delande
Nous présentons une approche dans laquelle la recherche d'une preuve d'une formule A et d'une réfutation de A (i.e. d'une preuve de non A) sont effectuées simultanément, contrairement à l'approche habituelle de la déduction automatique qui consiste à chercher à prouver l'une des deux. Notre approche est décrite sous la forme d'un jeu à deux joueurs avec des règles symétriques.Interaction, complexite et concurrence
Orateur : Damiano Mazza
Polarity and sequentiality in linear logic proofs nets
Orateur : Paolo di Giamberardino
Schemas de formules et de preuves en deduction automatique
Orateur : Vincent Aravantinos
Nous utilisons des techniques de schématisation de termes afin de schématiser des formules du premier ordre. Les intérêts de cette approche sont doubles : tenter d'améliorer l'efficacité des démonstrateurs automatiques ; et surtout tenter d'apporter plus de structure dans les preuves générées par ces démonstrateurs. Cette seconde vision est particulièrement intéressante car l'un des plus gros problèmes de la déduction automatique réside dans le fait que les preuves obtenues sont en général imbuvables par un humain.Acycylicite d'hypergraphes et theoremes de preservation par extension
Orateur : David Duris
Une classe de structures satifait le théorème de préservation par extension si, sur cette classe, tout énoncé du premier ordre est préservé par extension ssi il est équivalent à un énoncé existentiel. On considère différentes notions d'acyclicité pour les hypergraphes ($\gamma$, $\beta$ et $\alpha$-acyclicité ainsi que l'acyclicité pour des quotients d'hypergraphes) et on évalue leur influence sur la validité du théorème de préservation par extension sur des classes de structures finies. Plus précisément, on montre que les classes $\gamma$-acycliques satisfont le théorème de préservation alors que les classes $\beta$-acycliques ne le satisfont pas. On étend aussi la validité du théorème de préservation par extension à une généralisation de la $\gamma$-acyclicité qui est le fait d'avoir un $-quotient $\gamma$-acyclique. Les méthodes utilisées sont principalement une réduction des structures finies à leurs $-quotient et des arguments combinatoires sur les hypergraphes $\gamma$-acycliques.Presentation algebrique de strategies
Orateur : Samuel Mimram
Nous introduisons une sémantique de jeux pour la logique propositionnelle du premier ordre et donnons une présentation monoïdale des stratégies définissables du modèle.Reecriture des circuits orthogonaux
Orateur : Pierre Rannou
Orthogonal diagrams represent decompositions of orthogonal matrices, corresponding to isometries of Rn , into elementary ones: 1-dimensional symmetries and 2-dimensional rotations. A convergent rewrite system for this structure was introduced by the first author.One of the rules, which is similar to the Yang-Baxter equation, involves a map h : [0, Pi[3 -> [0, Pi[3 . To study the algebraic properties of h, we use the confluence of critical peaks in our rewrite system, and we introduce parametric diagrams describing the calculation of angles of rotations generated by rewriting. In particular, h satisfies the tetrahedron equation (also called Zamolodchikov equation)
Vers une approche logique de la geometrie des surfaces topologiques
Orateur : Gabriele Pulcini
La logique linéaire est caractérisée par la capacité de faire émerger les structures géométriques présentes dans la logique. Le programme de recherche présenté propose de renverser cette direction de recherche en proposant l'étude des mécanismes logiques qui sont à la base de la géométrie des surfaces topologiques.Particules, collisions et automates a compas : une approche pour les langages reguliers en dimension 2
Orateur : Gaetan Richard
Contrairement à la dimension 1, en dimension 2, il n'existe pas de notion unifié de langage régulier. En se basant sur la dynamique des automates cellulaires, nous étudierons quelques classes simples de mots bi-dimensionnels et montrerons leur lien avec une version un peu modifiée des automates à piles: les automates à compas.Facteurs d'automates cellulaires
Orateur : Pierre Guillon
Un automate cellulaire est un modèle de calcul parallèle synchrone, qui consiste en une juxtaposition d'automates d'état fini (cellules) dont l'état évolue dans le temps en fonction de celui de leurs voisins.Sa trace est l'ensemble des mots infinis pouvant être vus comme la succession des états d'une cellule particulière. Elle est liée dynamiquement au comportement de l'AC puisqu'avancer d'une lettre dans la lecture du mot correspond à appliquer une étape de l'AC. On dit qu'il s'agit d'un facteur; plusieurs propriétés en découlent.
Probabilite et complexite des fonctions booleennes dans le systeme de l'Implication
Orateur : Antoine Genitrini
L'utilisation d'expressions Booléennes basées sur un unique connecteur, l'Implication, nous permet de définir la densité asymptotique des fonctions Booléennes. Durant cet exposé, nous allons établir un lien entre la densité d'une fonction et sa complexité, définie par la taille de la plus petite expression permettant d'obtenir cette fonction.Automates cellulaires typiques
Orateur : Laurent Boyer
On s'interesse aux propriétés typiques des automates cellulaires, ou de manière équivalente aux propriétés des automates cellulaires aléatoires.On montre quelques résultats simples de densité de propriétés d'automates cellulaires. Pour cela on utilise des outils combinatoires usuels ainsi que la complexité de Kolmogorov.
Codes correcteurs d'erreurs sur des hypersurfaces maximales
Orateur : Frederic Edoukou
En 1981, V. Goppa mathématicien russe présenta pour la première fois une construction élégante de codes linéaires à patir de courbes hermitiennes. Ilobtint une estimation assez précise du taux de transmission et de la capacité de correction des erreurs pour ces codes.
Ce travail de Goppa inspira bien d’autres mathématiciens de par le monde.
En 1985 R. Tobias thèsard de I. Chakravati à l’UNC-CH en Caroline du Nord présenta l' étude des codes construits sur des surfaces hermitiennes sur
le corps fini à quatre éléments grâce à un traitement à l’ordinateur. Son
travail fut achévé en 1986 par P. Spurr à l’UNC-CH qui par un traitement informatique détermina la distance minimale ainsi que la distribution des
poids de ce code.
En 1991 A. Sørensen dans sa thèse de doctorat à Aarhus en s’affranchissant de l’outil informatique, donna une approche plus générale et plus géométrique de l' étude ce code construit sur la surface hermitienne. Il formula une conjecture sur sa distance minimale qui suscita plusieurs tentatives de résolutions quelques années plus tard.
Dans cet exposé nous allons répondre à cette conjecture. En utilisant des résultats de géométrie finie nous donnerons la distribution des poids et proposerons une généralisation de nos résultats aux codes hermitiens en dimension supérieure.
Factorisation des polynomes a plusieurs variables
Orateur : Abdessamad Belhadef
Dans cet exposé, on développe une méthode permettant de factoriser despolynômes à plusieurs variables sur un corps quelconque. Dans un premier
temps, on détermine le nombre de facteurs absolument irréductibles d’un
polynôme à plusieurs variables, ce résultat est basée sur l’utilisation d’un système d’équations aux dérivées partielles. Cela nous amène à donner une
nouvelle méthode permettant d’obtenir les facteurs absolument irr´eductibles
d’un polynôme à plusieurs variables en utilisant le résultant et en effectuant
un calcul de pgcd. On déduit de cette méthode un algorithme de factorisation
d’un polynôme à plusieurs variables.
Generation de courbes pairing-friendly
Orateur : Gaetan Bisson
Les couplages tels que celui de Weil donnent aux courbes hyperelliptiques une structure très appréciée en cryptographie. Toutefois, les courbes dont on peut évaluer le couplage en temps raisonnable sont rares ; il faut donc des algorithmes avancés pour générer celles-ci.Algo de calcul rapide de la suite des restes et des quotients via la matrice de henkel
Orateur : Skander Belhaj
Aspects structurels des pavages
Orateur : Alexis Ballier
On s'intéresse à l'étude de propriétés structurelles des pavages. Deux approches seront présentées; l'une basée sur l'apparition de motifs finis et l'autre basée sur la notion de dérivée topologique. Nous montrerons des liens entre ces deux approches et quels résultats (et quels pavages) nous pouvons obtenir en les combinant.Moments des fonctions theta
Orateur : Amadou diogo Barry
Il s'agit d'expliquer le but de ma these qui consiste en somme a montre que la fonction theta au point un en particulier n'est pas nul ou bien qu'il ne l'ai pour un certain nombre de characteres primitives ou pas.La frequence de certains modeles (m,n)-cubes dans le plan. Application au domaines estimateurs
Orateur : Mahdi Zouaoui
Cet exposé est consacré à une étude approfondie des estimateurs locaux en dimension trois, plus précisément les estimateurs locaux d'aire de la discrétisation d'un morceau d'un plan de R3 dans rZ3 (i.e. est la résolution de l'espace discret). Le but de cette étude est d'une part de trouver les poids optimaux pour de tels estimateurs et d’autre part, d'étudier leur convergence lorsque la résolution r tend vers zéro.Le résultat principal montre que les estimateurs locaux sont inexacts presque sûrement.
Selfish distributed routing and convergence to Nash equilibria in Wardrop networks
Orateur : Octave Boussaton
Calcul hyperdéterminental appliqué au calcul des puissances paires du Vandermonde
Orateur : Adrien Boussicault