Le séminaire de l’équipe Labo est sous la responsabilité de Michel Raibaut.
Options : Voir par date croissante . Masquer les résumés.
Autres années : 2003, 2004, 2005, 2006, 2007, 2008, 2009, 2010, 2011, 2013, 2014, 2015, 2016, 2017, 2018, toutes ensemble.

Année 2012

Jeudi 13 décembre 2012 à 14h Pierre Etienne Meunier (LAMA, Université de Savoie),
Les automates cellulaires comme modèle de complexités parallèles.

Résumé : (Masquer les résumés)
Dans ma thèse, j'ai étudié les liens entre deux notions différentes de la complexité. La complexité algorithmique, d'une part, qui mesure la difficulté de réaliser une tâche automatiquement. La complexité de systèmes, d'autre part, qui est le degré d'intrication des actions des agents du système. Cette approche est relativement nouvelle, à la fois dans les deux théories, et offre des perspectives enthousiasmantes pour parler des grandes conjectures de la complexité. En particulier, nous avons réussi à développer une méthode générique pour construire des bornes inférieures de complexité, et des conditions nécessaires relativement élémentaires sur notre modèle de calcul, ce qui est souvent considéré comme une question difficile en théorie de la complexité. D'autre part, mon travail propose une définition alternative de classes de complexité, basée sur des automates cellulaires, et étudie les relations avec les définitions classiques. Enfin, la dernière partie de mon travail a consisté à utiliser les méthodes de la théorie de la complexité pour ouvrir de nouvelles pistes sur une conjecture ancienne en automates cellulaires, à savoir l'existence d'un automate universel par facteur. J'ai soutenu ma thèse le 26 octobre 2012 à Santiago, au Chili, mais je suis heureux de vous convier à cet exposé, sans doute plus informel, sur les travaux que j'ai effectués pendant ces quelques années au LAMA.

Vendredi 12 octobre 2012 à 14h30 Matthieu Simonet (LAMA, Université de Savoie),
Mots de retour dans les plans sturmiens

Résumé : (Masquer les résumés)
Les mots sturmiens sont une façon de coder les droites discrètes apériodiques. Ils ont été étudiés depuis la fin du 19ème siècle et disposent de nombreuses caractérisations. L'une d'elles, obtenue par Vuillon, est centrée sur la notion de mot de retour. Cette thèse a pour objet l'étude des mots sturmiens en dimension 2 vus comme codages des plans discrets apériodiques. L'objectif est d'aller vers une caractérisation des mots sturmiens bi-dimensionnels analogue à celle obtenue par Vuillon en dimension 1. Mais des problèmes propres à la dimension 2 rendent cette étude délicate, tels l'absence de concaténation de mots ou la difficulté à localiser un facteur au sein d'un mot. Afin d'y faire face, nous introduisons en dimension 2 les notions de motifs, motifs pointés, mots de localisation et mots de retour. Nous obtenons ainsi un prolongement à la dimension 2 d'un théorème de Morse et Hedlund concernant certains mots de retour dans un mot sturmien. Ce résultat nous permet d'établir un nouvel algorithme de fractions continues et nous permet de proposer, dans un cadre restreint, une notion de suite dérivée.

Jeudi 28 juin 2012 à 14h M. Putinar (University of California at Santa Barbara),
La quantification de l'ellipse

Résumé : (Masquer les résumés)
Lorsque l'on interprète l'équation quadratique d'une ellipse au niveau des opérateurs de l'espace d'Hilbert, on découvre une anomalie entre la sous-normalité (des opérateurs) et la positivité hermitienne (des polynômes). Mais lorsqu'on analyse de près la même quantification, on découvre que l'ellipse se singularise par deux propriétés : ses opérateurs respectifs possèdent une matrice diagonale triple et le problème de Dirichlet admet des solutions polynomiales. Cette présentation se veut accessibles à des étudiants de Master et s'efforcera de ne pas rentrer dans des aspects trop techniques.

Jeudi 14 juin 2012 à 10h, ANNECY Fédération de recherche (MSIF) Olivier Laffitte (Département de Mathématiques, Institut Galilée, Université Paris 13),
Quantification et taux de croissance des instabilités en hydrodynamique classique

Résumé : (Masquer les résumés)
Il est connu depuis lord Rayleigh que certaines instabilités hydrodynamiques (essentiellement les instabilités de Rayleigh-Taylor, instabilité de Couette) peuvent être prises en compte par une équation différentielle ordinaire faisant intervenir le taux de croissance de l'instabilité (qui s'appelle selon les cas Orr-Sommerfeld ou Rayleigh). Mikaélian a remarqué que l'équation de Rayleigh pouvait se réécrire de manière équivalente comme une équation de Schrodinger (Phys Rev E 53, 1996). Avec C. Cherfils dans un cas particulier (Phys Rev E 62, 2000) puis avec B. Helffer dans le cas général pour l'équation de Rayleigh, nous avons démontré que le taux de croissance de l'instabilité de Rayleigh-Taylor linéarisée n'étaitpas unique, mais suivait une suite quantifiée (valeurs propres d'un opérateur classique), et nous démontrons que cette remarque permet la construction d'un mode instable pour le problème de Rayleigh-Taylor dans le cas non linéaire.

Jeudi 31 mai 2012 à 14h Hervé Le Ferrand (Université de Bourgogne),
Fractions continues algébriques : la contribution de Robert de Montessus de Ballore

Résumé : (Masquer les résumés)
En mathématiques, dans le domaine de l'Approximation Rationnelle, en particulier les fractions continues, approximation au sens Padé, il n'est pas rare de rencontrer parmi les publications récentes le nom Montessus de Ballore. Par exemple, en 2009 paraît dans Found Comput Math Convergent Interpolation to Cauchy Integrals over Analytic Arcs, de Laurent Baratchart et Maxim Yattselev, dans lequel le théorème de convergence de Robert de Montessus est donné en référence. En 2010, A. Sidi publie dans Comput. Methods Funct. Theory, A de Montessus type convergence study of a least-squares vector-valued rational interpolation procedure II, dans lequel une généralisation du résultat de Robert de Montessus est donnée. Ainsi, à quoi tient la pérennité de ce résultat ?
Robert de Montessus fut lauréat en 1906 d'un Grand Prix de l'Académie des Sciences et en 1917, il rentre au comité de rédaction du Journal de Mathématiques Pures et Appliquées alors dirigé par Camille Jordan. C'est au cours de l'année 1902 que Robert de Montessus de Ballore (1870-1937) prouva son fameux théorème [3] sur la convergence d'approximants de Padé de fonctions méromorphes [2]. Pour la démonstration, il utilisa en particulier des résultats de J. Hadamard sur ce que l'on appelle aujourd'hui les polynômes de Hadamard. Jusqu'en 1909, Robert de Montessus publia des travaux sur les fractions continues algébriques.
Nous cherchons à comprendre comment son théorème s'est diffusé et examinons aussi les autres résultats qu'il a obtenus. Nous disposons en particulier de toute une correspondance scientifique que nous avons recueillie auprès de sa famille et qui fait l'objet d'un archivage à l'Université Pierre et Marie Curie [1]. Certaines de ces lettres permettent d'expliquer la genèse du théorème de 1902. Nous en projetterons des fac-similés. En particulier, Henri Padé et Robert de Montessus ont correspondu durant les années 1901-1902. Nous verrons aussi que le résultat de 1902 est rapidement cité par des mathématiciens comme Van Vleck, Nörlund ou encore O. Perron avant la première guerre mondiale, puis Wilson et surtout J.L. Walsch entre les deux guerres.

[1] Fonds Robert de Montessus de Ballore (Université Pierre et Marie Curie, Paris, archivage en cours).
[2] Claude Brezinski, History of continued fractions and Padé approximants, Springer Verlag, Berlin, (1991).
[3] R. de Montessus de Ballore, Sur les fractions continues algébriques, Bull. Soc. Math. France 30 (1902), pp 28-36.
[4] Biographie de R. de Montessus de Ballore sur Mac Tutor : lien.

Jeudi 02 février 2012 à 15h30, TLR Boris Kolev (Université de Provence),
Un principe universel de la mécanique d'après Jean-Marie Souriau

Résumé : (Masquer les résumés)
« div(T) = 0, c'est la mécanique ! » . À partir de cette expression attribuée à Einstein, Jean-Marie Souriau a formulé une équation universelle de la mécanique, dont dérive la plupart des modèles de la mécanique des milieux continus. Cet exposé propose de présenter cette formulation géométrique, élégante et encore mal connue.

Jeudi 19 janvier 2012 à 14h Gilles Lebeau (Laboratoire Dieudonné de Nice),
Algorithme de Metropolis

Résumé : (Masquer les résumés)
L'algorithme de Metropolis est un algorithme permettant de tirer un point au hasard pour une probabilité donnée. Il a été introduit en 1953 par N. Metropolis, A.-W. Rosenbluth, M.-N. Rosenbluth, A.-H. Teller, E. Teller, dans l'article '' Equations of State Calculations by Fast Computing Machines, Journal of Chemical Physics 21 (6) 1087--1092. Il a ensuite été généralisé en 1970 par W.-K. Hastings dans ``Monte Carlo Sampling Methods Using Markov Chains and Their Applications'', Biometrika 57 (1) 97?109. Cet algorithme, et ses variantes, est un des plus utilisés du calcul scientifique, voir par exemple ``top ten algorithms of the century'' sur google. Son étude mathématique est par contre très loin d'être achevée et pose des problèmes fort intéressants de géométrie, de théorie spectrale, d'analyse, et bien sur de probabilités. Dans cet exposé, je commencerai par introduire l'algorithme sous sa forme historique : Comment choisir N disques de rayon r (sans recouvrement ) au hasard dans un carré? et j'indiquerai quelques résultats et problèmes ouverts sur ce modèle. Dans une deuxième partie, je montrerai comment les plus simples des algorithmes de Metropolis, associés à des marches aléatoires à ``petits pas'', conduisent à l'étude d'opérateurs qui généralisent les opérateurs du calcul pseudodifférentiel semiclassique usuel.

Mercredi 18 janvier 2012 à 15h Muhammad Humayoun (LAMA, LIMD),
Developing the System MathNat for Automatic Formalization of Mathematical texts

Résumé : (Masquer les résumés)
There is a wide gap between the language of mathematics and its formalized versions. The term ``language of mathematics'' or ``mathematical language'' refers to prose that the mathematician uses in authoring textbooks and publications. It mainly consists of natural language, symbolic expressions and notations. It is flexible, structured and semantically well-understood by mathematicians. However, it is very difficult to formalize it automatically. Some of the main reasons are: complex and rich linguistic features of natural language and its inherent ambiguity; intermixing of natural language with symbolic mathematics causing problems which are unique of its kind, and therefore, posing more ambiguity; and the possibility of containing reasoning gaps, which are hard to fill using the current state of art theorem provers (both automated and interactive). One way to work around this problem is to abandon the use of the language of mathematics. Therefore in current state of art of theorem proving, mathematics is formalized manually in very precise, specific and well-defined logical systems. The languages supported by these systems impose strong restrictions. For instance, these languages have non-ambiguous syntax with a limited number of possible syntactic constructions. This enterprise divides the world of mathematics in two groups. The first group consists of a vast majority of mathematicians whose rely on the language of mathematics only. In contrast, the second group consists of a minority of mathematicians. They use formal systems such as theorem provers (interactive ones mostly) in addition to the language of mathematics. To bridge the gap between the language of mathematics and its formalized versions, we may ask the following gigantic question: Can we build a program that understands the language of mathematics used by mathematicians and can we mechanically verify its correctness? This problem can naturally be divided in two sub-problems, both very hard: 1. Parsing mathematical texts (mainly proofs) and translating those parse trees to a formal language after resolving linguistic issues. 2. Validation of this formal version of mathematics. The project MathNat (Mathematics in controlled Natural language) aims at being the first step towards solving this problem, focusing mainly on the first question. For that, first, we develop a Controlled Language for Mathematics (CLM) which is a precisely defined subset of English with restricted grammar and lexicon. To make CLM natural and expressive, we support important linguistic features such as anaphoric pronouns and references, rephrasing of a sentence in multiple ways, the proper handling of distributive and collective readings and so on. The coverage of CLM at the moment is yet rather small and to be improved as the project keeps evolving in future. Second, we develop MathAbs (Mathematical Abstract language). It is a prover independent formal language to represent the semantics of CLM texts preserving its logical and reasoning structure. MathAbs is designed as an intermediate language between CLM and the formal languages of theorem provers, allowing proof checking. Third, we propose a system that can automatically translate CLM to MathAbs, giving a precise semantics to CLM. We consider that formalizing mathematics automatically in such a formal language that has a precise semantics is an important progress even if it can't always be proof-checked. This brings us to the second question for which we report a very limited work. We only translate MathAbs to the first-order formulas. If we feed these formulas to the automated theorem provers (ATPs), then fundamentally the ATPs should be able to validate them sometimes. In other words, the resulting MathAbs document is not completely verifiable for the moment, but it represents an opportunity for the mathematician to write mathematical text (mainly proofs) without becoming expert of any theorem prover. Keywords: Computational linguistics, Controlled languages, Formalization, Formal systems, Verification, Proof checking.

Le séminaire de l’équipe Labo est sous la responsabilité de Michel Raibaut.
Options : Voir par date croissante . Masquer les résumés.
Autres années : 2003, 2004, 2005, 2006, 2007, 2008, 2009, 2010, 2011, 2013, 2014, 2015, 2016, 2017, 2018, toutes ensemble.