Cet exposé est divisé en deux parties distinctes présentant deux sujets de recherche autour de la Logique Linéaire. Bien qu'abordés il y a longtemps, ces sujets présentent toujours des questions ouvertes intéressantes. L'exposé pose plus de questions qu'il ne donne de réponses.
Le premier sujet concerne la notion de structure en Logique Linéaire. De nombreuses extensions de la Logique Linéaires ont été proposées dans le passé pour introduire une forme de structure qui dépasse celle de multi-ensemble: logique cyclique, logique non commutative, calcul de Lambek non associatif (qui en fait prédate la Logique Linéaire)... Un cadre général, appelé ``Logiques Linéaires Colorées'', a été proposé pour capturer les mécanismes communs à toutes ces extensions, et permettant d'en construire d'autres à l'infini, respectant automatiquement les propriétés essentielles d'élimination de la Coupure et de focalisation (ce travail montre d'ailleurs que ces deux propriétés sont intimement liées). La question ouverte est de comprendre quels critères supplémentaires permettent de séparer, dans cette infinité potentielle de systèmes, le bon grain de l'ivraie, avec l'idée sous-jacente que la Logique devrait avoir un caractère de nécessité, et ne pas laisser place à l'arbitraire.
Le deuxième sujet concerne un paradigme de programmation fondé non pas sur la réduction des coupures dans les réseaux de preuves mais sur la construction de réseaux de preuves en Logique Linéaire. La construction de réseaux, comme la réduction, peut se faire en parallèle, mais, contrairement à la réduction, il y a des séquentialisations irréductibles, qu'exprime la nécessité de respecter le critère de correction. Le paradigme résultant est très proche de celui, plus pragmatique, des systèmes transactionnels, issus du monde des bases de données, mais dont les mécanismes sont aujourd'hui présents dans les couches intergicielles de toutes les grandes applications réparties. Un mécanisme de construction incrémental de réseaux de preuves a été proposé dans le passé dans le cadre du fragment strictement multiplicatif de la Logique Linéaire. Les questions ouvertes sont ici de savoir si ce mécanisme est optimal pour le fragment visé d'une part et d'autre part s'il peut être étendu à des fragments plus larges, voire au système complet.
Deuxième séance du groupe de lecture sur le livre de Kohlenbach ``Applied Proof Theory''.
Developing effective reasoning techniques for languages with higher- order constructs is a challenging problem, made even more challenging with the presence of concurrency and mobility. In this talk I will present a practical and effective reasoning methodology for such a language, which employs first-order reasoning and handles examples in a straightforward manner. There are two significant aspects to this theory. The first is that higher-order inputs are treated in a first- order manner, hence eliminating the need to reason about arbitrarily complicated higher-order contexts, or to use up-to context techniques, when establishing equivalences between processes. The second is that we use augmented processes to record directly the knowledge of the observer. This has the benefit of making ordinary first-order weak bisimulation fully abstract w.r.t. contextual equivalence. It also simplifies the handling of names, giving rise to a truly propositional Hennessy-Milner characterisation of higher-order contextual equivalence. I will illustrate the simplicity of the approach with example equivalences and inequivalences, and use it to show that contextual equivalence in a higher-order setting is a conservative extension of the first-order pi-calculus.
``Bounds on the product of the first two non-trivial frequences of a free membrane'' In this talk we are interested in the eigenvalue problem of a free membrane represented as a bounded simply-connected planar domain D with Lipschitz boundary. The aim of this talk is twofold. First, we give a positive answer to the following conjecture of Iosif Polterovich: the product of the first two non-trivial Neumann eigenvalues of the laplacian on D (frequencies of the free membrane D) is upper bounded by the value of the same quantity for the disk with same area as D. This estimate is sharp and the equality occurs if and only if D is a disk. Secondly, we consider the class of n-sided convex polygons and establish an isoperimetric inequality for the product of some moments of inertia. As an application, we obtain an explicit nice upper bound for the product of the first two non-trivial frequences of a free membrane represented as a n-sided convex polygon.
L’indice radial d’une 1-forme sur un ensemble singulier est une généralisation de l’indice de Poincaré-Hopf. On considère différentes classes d’ensembles semi-analytiques fermés dans qui contiennent dans leur lieu singulier et nous relions l’indice radial d’une 1-forme en sur ces ensembles à des indices de Poincaré-Hopf en de champs de vecteurs définis sur .
En 1932, Paley et Zygmund démontrent que les séries trigonométriques aléatoires sur le tore sont presque surement plus régulières que ce a quoi on s'attendrait. Ce type de résultat a par la suite été étudié par de nombreux auteurs dans un contexte d'analyse harmonique (Pisier et Kahane notamment). Curieusement, pendant longtemps, les spécialistes des EDP ne se sont pas interessés à ce type de questions. L'objet de cet exposé est précisement de montrer quelques applications des idees directement inspirées de Paley et Zygmund, au contexte des EDP. Plus précisément, on montrera que pour certaines équations des ondes et de Schrodinger, pour des données initiales aléatoires, la situation est bien meilleure en termes d'existence et de comportement en temps longs, que pour des données initiales fixées. Il s'agit de travaux en collaboration avec N. Tzvetkov (Cergy) et L. Thomann (Nantes).
La séance précédente était consacrée aux algèbres de Boole et aux notions de filtre, d'idéal et d'ultrafiltre. Cette séance sera consacrée à la définition de la notion de modèle Booléen (en insistant sur les problèmes soulevés par cette définition) et à l'étude de ses propriétés: validité, complétude, etc. Je présenterai les principales constructions attachées aux modèles booléens: produit, quotient, ultraproduit, ultrapuissance. Je terminerai en montrant comment la théorie peut être appliquée à la construction des modèles de l'analyse non standard.
I prove that a set of non-properness of a dominant polynomial mapping f : X -> Y is always a k-uniruled hypersurface. As application, we see that a set of fixed points of unipotent group acting on affine variety is k-uniruled.
Voir la page dédiée.
La théorie des équations différentielles stochastiques rétrogrades (EDSRs) permet, entre autre, de donner une représentation probabiliste d'EDPs semi-linéaires. Dans cet exposé nous nous intéresserons à des EDSRs en horizon infini qui nous fournissent un outil alternatif pour l'étude de problèmes de contrôle optimal ainsi que certains problèmes de Neumann semi-linéaires associés à des phénomènes ergodiques et étudiés par G. Barles et F. Da Lio dans leur article ``On the boundary ergodic problem for fully nonlinear equations in bounded domains with general nonlinear Neumann boundary conditions'' (2005).
Let (X,\omega) be blown-up CP^2 equipped with some symplectic form. I show that Lagrangian isotopy classes of spheres in (X,\omega) can be indexed by conjugacy classes of certain generators in the group G of connected components of the symplectomorphism group of (X,\omega). Then I show that this group is isomorphic to the fundamental group G of the complement to certain divisor D in (Cp^2)^k parametrising certain constellations of k points in CP^2. I describe a presentation of the group G and compute it for certain special case. As the result, I show that for a special choice of the Kähler form in CP^2 blown-up in 5 points the Lagrangian isotopy classes of spheres representing a given homology class are paramtrized by integer 2x2-matrices in Gl(2,Z) conjugated to the matrix
| 1 2 |
| 0 1 |.
En combinatoire des mots et plus précisément dans l'étude des mots unidimensionnels, la notion de mot de retour a joué un rôle important, en particulier dans la caractérisation des mots sturmiens. Ces mots servant de représentation pour les droites discrètes, il est tout naturel de se poser la question d'une caractérisation en dimension supérieure, en particulier dans le cas des plans discrets. En dimension 2, on vient à considérer des mots bidimensionnels. Les notions habituelles doivent donc être adaptées. Nous verrons que le passage à la dimension 2 provoque de vrais problèmes vis à vis de définitions simples en dimension 1.
Les ensembles semi-algébriques et sous-analytiques p-adiques ont été introduits et étudiés par McIntyre, Denef et Van den Dries entre autres. Nous étudierons la géométrie des germes d'ensembles de ces catégories, tout particulièrement leurs propriétés métriques, comme l'existence de la densité locale et de cônes tangents distingués en montrant comment les propriétés géométriques des ensembles sous-analytiques réels se traduisent dans le cas valué.
Les théories de la calculabilité (que peut-on calculer ?) et de la complexité algorithmique (quelle est la difficulté intrinsèque d'un problème calculable ?) sont deux piliers de la science informatique. L'objectif de cet exposé est de donner un aperçu des concepts, des principaux résultats et des grands problèmes ouverts de ces théories. Selon le temps, nous parlerons de fonctions récursives, d'ensembles diophantiens, de pavages du plan, d'applications affines par morceaux, d'identités polynomiales, etc, avec le secret espoir de convaincre l'auditoire que la notion de calcul est avant tout protéiforme et peut s'immiscer dans de nombreux objets mathématiques ``classiques''.
Je présente un lambda calcul codant une logique intuitionniste du second ordre et permettant de programmer un ou-parallèle''. Ce calcul a les propriétés suivantes :
préservation de type'', forte normalisation'' et
unicité de représentation des données''. Il permet aussi d'écrire des programmes avec une sorte d'exception. Il est inspire du lambda-mu-{++}-calcul que j'ai introduit en 2002.
En 1962, Cohen a résolu le premier problème de Hilbert en montrant que l'hypothèse du continu est indécidable dans la théorie des ensembles de Zermelo-Fraenkel. La technique qu'il a introduite pour établir ce résultat non trivial - le forcing - est devenue aujourd'hui un outil standard en théorie des modèles. Cette technique a permis d'établir de nombreux autres résultats de cohérence relative (ou d'indépendance), comme par exemple la cohérence de l'axiome de Solovay: « toute partie de R est mesurable au sens de Lebesgue » dans une théorie des ensembles sans axiome du choix (mais avec choix dépendant).
Dans cet exposé introductif au forcing, je me propose de présenter la théorie des modèles booléens, une variante du forcing (introduite par Scott, Solovay et Vopenska dans les années 1960) qui permet de faire essentiellement les mêmes constructions que Cohen, mais dans un cadre qui est plus facile à saisir au premier abord. J'introduirai les notions de base (algèbres de Boole, ultrafiltres, modèles booléens, quotient, produit, ultraproduit et ultrapuissance) tout en illustrant mon propos par quelques exemples de constructions, notamment en lien avec l'« analyse non standard ».
La preuve de l'indépendance de l'hypothèse du continu à l'aide de ces outils fera l'objet de l'exposé suivant.
On considère la classe des systèmes de Timoshenko. L’objectif est de démontrer la stabilité à l’infini (l’énergie décroit vers zéro quand le temps converge vers l’infini) et obtenir une estimation sur le taux de décroissance. Pour cela, on distingue deux cas. 1. Les deux équations ont la meme vitesse de propagation : pour toute solution faible, on montre une estimation générale et explicite sur l’énergie ce qui donne une idée précise sur l’influence de chaque controle sur la stabilité du système. On donne quelques exemples pour illustrer notre estimation. 2. Les deux équations n’ont pas la meme vitesse de propagation : sous des hypothèses plus fortes et pour des solutions plus régulières, on montre une estimation de stabilité plus faible. L’idée de la démonstration est basée sur la méthode des multiplicateurs et quelques inégalités intégrales. Ses résultats ont été obtenus en collaboration avec S. Messaoudi (KFUPM, Dhahran, Arabie Saoudite) dont une partie va apparaitre dans Mathematical Methods in the Applied Sciences.