La logique linéaire s'interprète dans les espaces vectoriels, même si les exponentielles posent problème (on obtient des espaces de dimension infinie). Dans le cas fini, cette interprétation est malheureusement un peu dégénérée car l'interprétation d'une formule (un espace vectoriel) est isomorphe à celle de sa négation (l'espace des formes linéaire sur cet espace). Christine a récemment proposé une solution : en plus de l'espace vectoriel, on rajoute une notion de totalité. Typiquement, une fonction linéaire de A dans B est totale ssi elle envoie les vecteurs totaux sur des vecteurs totaux. Algébriquement parlant, la totalité est un sous-espace affine de l'espace vectoriel considéré.
Christine introduira tout ça avec un peu plus de détails, et expliquera comment obtenir un premier résultat de complétude : complétude d'un calcul booléen basé sur la traduction habituelle du type Bool => Bool dans la logique linéaire. Pierre poursuivra avec un second résultat toujours de complétude : complétude d'une logique linéaire sans exponentielles. (Ça, c'est si la preuve ne « devient » pas fausse d'ici là...)
Le premier résultat ne nécessite aucune connaissance en logique linéaire (si si, c'est vrai), et le second présuppose un modicum de logique linéaire pour comprendre le pourquoi (mais pas le comment). Des connaissances de base en algèbre linéaire sont nécessaires, mais rien de compliqué, et seulement en dimension finie.
Dans le modèle des automates cellulaires, la non-linéarité est omniprésente. Une voie pour étudier ces objets peut être la théorie du chaos déterministe. Elle a déjà été largement empruntée dans la littérature (avec les travaux de P. Kurka notamment), mais pratiquement toujours en se restreignant à la dimension 1. En ce concentrant sur certaines propriétés autour de la sensibilité aux conditions initiales, nous montrerons dans une première partie de cet exposé que cette restriction n'est pas neutre : une nouvelle classe de comportements dynamiques (les automates cellulaires non sensibles aux conditions initiales mais sans point d'équicontinuité) apparaît à partir de la dimension 2. De la démonstration de l'existence de cette classe, nous tirerons d'autres résultats montrant que la complexité de certaines propriétés fait un bond lorsque l'on quitte la dimension 1.
Dans une seconde partie d'exposé, nous prendrons un peu de recul sur la question de la variation de complexité des propriétés en fonction de la dimension. Nous poserons un cadre logique formalisant ce que l'on peut appeler la ``dynamique topologique'' dans les automates cellulaires. Nous aborderons alors le problème suivant : étant donnée une propriété (une formule dans notre théorie), quel est la complexité de l'ensemble des automates cellulaires qui la satisfont ? cet ensemble est-il arithmétique ? à quelle hauteur dans la hiérarchie ? comment cette hauteur varie avec la dimension ?
Selon la vitalité de l'orateur, le traitement de ce questionnement pour aller du simple traitement d'exemples à la démonstration d'un résultat général.
Composition of strategies is the crucial operation of game semantics. It corresponds to cut elimination in proof theory. This paper is an attempt to uncover the sheaf-theoretical nature of these two operations. We define a game semantics with a topological flavor for a variant of Multiplicative Additive Linear Logic (henceforth MALL). We show that the standard notion of strategy leads to a correct, yet incomplete model. We then introduce a new, non-standard notion of local'' strategies, which turn out to form a sheaf. <br><br> Composition of strategies is generally divided into two steps: interaction, and hiding. In our setting, interaction arises as gluing in the sheaf of local strategies. Hiding along a cut c: U -> V appears here as an instance of a more general operation,descent'' along c, which also encompasses cut elimination. Descent along c is a morphism of sheaves on V from the direct image along c of local strategies on U, into cut-free local strategies on V. It arises from a factorisation system, roughly dividing plays into their cut-only and cut-free parts.
Finally, our notion of (winning) local strategy is validated by the expected soundness and completeness results w.r.t. MALL provability.
Je parlerai des zippers : leurs principes, comment ils amènent à une notion de dérivée de type de données. On verra alors une première définition de cette dérivée par McBride, quelques problèmes et une deuxième définition pour y répondre. Puis nous passerons brièvement aux containers, une notion générale de type de données. Nous verrons comment étendre la notion de dérivée aux containers pour finir sur une formule de Taylor des containers.
Les espaces cohérents de Jean-Yves Girard et les espaces de finitude de Thomas Ehrhard sont obtenus à partir d'une base « similaire » : l'orthogonalité.
Je commencerais par rappeler comment ça marche (parce que c'est intéressant et pas très compliqué), puis je passerais à une structure mixte qui permet de générer des espaces de finitude « simples » à partir d'espaces cohérents.
Cette construction contient tous les exemples usuels d'espaces de finitude et de plus, elle commute avec les opérations logiques (⅋, ⊗, ⊕, &, ⊸, !, …) Un des aspects intéressants est l'utilisation du théorème de Ramsey infini pour démontrer certaines propriétés de cette construction.
Je finirais par expliquer comment on tombe sur une notion qui généralise les fonctions stable de Berry pour permettre d'interpréter une version simple du λ-calcul algébrique de Lionel, Thomas et consorts.
Remarques : j'essaierais, autant que possible, de ne pas supposer connue toute la logique linéaire. Les deux premiers tiers de mon exposé devraient donc être « self-contained »...
La droite réelle de Harthong-Reeb est un modèle non-standard du continu qui est à l'origine de nombreux développements en géométrie discrète (entre autre la droite discrète de Réveillès). Selon Harthong et Reeb eux-mêmes leur modèle n'est pas sans liens avec une approche constructive. Récemment à Poitiers et à La Rochelle nous nous sommes intéressés à cette question en montrant que la droite de Harthong-Reeb vérifie les axiomes de Bridges qui sont une théorie de la droite réelle constructive.
L'orateur propose un deuxième exposé, qui aura peut-être lieu l'après-midi s'il y a des volontaires :
We present a variant of the explicitly-typed second-order polymorphic λ-calculus with primitive open existential types, i.e., a collection of more atomic constructs for introduction and elimination of existential types. We equip the language with a call-by-value small-step reduction semantics that enjoys the subject reduction property. We claim that open existential types model abstract types and module type generativity. Our proposal can be understood as a logically-motivated variant of Dreyer’s RTG where type generativity is no more seen as a side effect. As recursive types arise naturally with open existential types, even without recursion at the term-level, we present a technique to disable them by enriching the structure of environments with dependencies. The double vision problem is addressed and solved with the use of additional equalities to reconcile the two views.
Voir la page dédiée.
Cours puis groupe de travail sur la réalisabilité avec Alexandre Miquel. Détails ici.
Le project MathLang a pour but de computeriser des textes de mathematiques selon des degres de formalisation differents, et sans preciser d'avance un engagement dans:
* un logique particulier (par example, sans devoir choisir comme base une theorie des ensembles, une theorie des categories, une theorie des types, etc.)
* un systeme de demonstration particulier (par example, sans devoir choisir comme systeme de demonstration Mizar, Isaeblle, Coq, PML, etc.).
MathLang laisse les choix concernant les systemes de demonstration et de la logique ouverts tant que c'est possible. En plus, MathLang permet des niveaux varies de computerisation, et n'insiste pas qu'une formalisation soit complete comme c'est fait dans les fondations de la mathematiques a la Russell et Frege ou dans les systemes de demonstration (comme initie par de Bruijn). Pendant la computerisation, le text mathematique est d'abord insere dans l'ordinateur tel qu'il est ecrit par le mathematicien sur papier. Puis un ou plusieures aspets de MathLang sont appliques au texte pour donner des versions du texte qui sont (automatiquement) controles a des niveaux differents:
1. Un aspect de base est l'extension du texte avec l'information categorique (terme, nom, adjectif, proposition, etc) ou la coherence et la structure grammaticale du texte sont controlees automatiquement.
2. Un autre aspect partage le texte en parties annotees par des relations (e.g., Corollaire A utilise Theorem B) et automatiquement controle la structure logique du texte (ce n'est la correction logique du texte).
3. Un autre aspect transforme le texte alors que les trous dans les preuves sont evidents.
4. D'autres aspects transforment cette version derniere en une formalisation complete (dans Coq, Mizar, Isabelle, etc).
MathLang a ete cree par Fairouz Kamareddine et J.B. Wells en 2000. Nous avons computeriser des textes dans MathLang (pas a pas) jusqu'a des formalisations completes dans Coq et Mizar (aussi Isar/Isabelle). Depuis 2002, 4 etudiants de theses (Manuel Maarek, Kryztof Retel, Robert Lamar et Christoph Zengler) et des dizaines d'etudiants de master et de BSc ont contribue au design et a l'implantation de MathLang et a son utilisation pour la computerisation des textes de Maths.
S'il reste du temps, Fairouz pourra enchaîner sur un exposé plus orienté lambda-calcul:
Titre: Parametres dans le lambda calcul type.
Les fonctions dans le lambda calcul sont toujours d'ordre superieur. Traditionellement, les fonctions en maths sont d'ordre inferieur. Ici, on donne le lambda calcul avec des fonctions d'ordre inferieur et on divise le cube de Barendregt en 8 sous-cubes qui permettent des meilleures representations des constructeurs dans les languages ML, LF et Automath.
C'est un travail commun avec Twan Laan et Rob Nederpelt.
La théorie des pavages par tuiles de Wang a été inventée par (surprise) Hao Wang afin de proposer un problème combinatoire concret correspondant au pouvoir d'expressivité d'un fragment de la logique du premier ordre. La théorie des pavages s'est en fait révélée comme une théorie élégante s'exprimant facilement logiquement, et a ainsi apporté de nombreux résultats en logique mathématique.
Il s'agit dans cet exposé de proposer une présentation des liens entre pavages et logique. On analysera en particulier comment deux des théorèmes fondamentaux sur les pavages se traduisent :
- Par l'existence d'une théorie complète finiment axiomatisable et superstable [Makowsky, Poizat]
- Par le fait que le fragment AEA de la logique du premier ordre forme une classe de réduction conservative [Büchi, Kahr-Moore-Wang]
tout en expliquant bien entendu ce que signifient les nombreux mots potentiellement obscurs des phrases précédentes.
Aucune connaissance sur les pavages n'est nécessaire. Une connaissance rudimentaire de la logique du premier ordre sera appréciée.
Les exceptions sont généralement vues comme un mécanisme modifiant le flot de contrôle d'un programme. Cette vision cantonne les exceptions aux langages pour lesquels la notion de flot de contrôle est bien définie, ce qui n'est généralement pas le cas pour les langages de la théorie des types. Nous présenterons un mécanisme où les exceptions sont attachées aux valeurs plutôt qu'au flot de contrôle, ainsi qu'un système de types pour ces exceptions basé sur la notion de corruption. Nous montrerons que cette notion, utilisée à travers une relation de sous-typage, permet la détection statique d'exceptions non rattrapées, et ce sans compromettre la propagation automatique des exceptions. Nous illustrerons ce système d'exceptions dans le cadre d'une extension du Système F, utilisé ici comme une première étape vers des systèmes de types plus riches (avec pour horizon le calcul des constructions). Enfin, nous présenterons un modèle de réalisabilité pour justifier et expliquer la notion de corruption dans notre calcul.
Cf le site idoine: http://choco.pps.jussieu.fr/events.
Comme le montrent les publicités dans les magazines (multi-coeur par-ci, hyperthread par-là), la tendance des architectures des ordinateurs est à la parallélisation, et l'on commence donc dans le grand public à parler de programmation avec des threads. Du côté des machines de calcul scientifique, on mélange en fait allègrement ces technologies de manière hiérarchique pour aboutir à de véritables cathédrales, sur lesquelles on exécute une armée de threads. Cependant, pour obtenir une exécution efficace (et donc économiser du temps, des machines ou de l'énergie), il est indispensable de distribuer de manière raisonnée ces threads sur ces machines. La tâche est d'autant plus ardue que les threads peuvent en créer d'autres, éventuellement de manière irrégulière. Durant ma thèse, j'ai proposé la notion de /bulles/, qui regroupent de manière récursive les threads et apportent ainsi une certaine structure aux applications de calcul scientifique. En modélisant par ailleurs les machines de calcul sous forme d'un arbre, on ramène ainsi notre problème à la mobilité des bulles et threads sur cet arbre. Une boîte à outil permet alors d'implémenter des algorithmes de placement/redistribution pour les appliquer à des applications bien concrètes. On peut alors observer des gains de performances de l'ordre de 20 à 40% par rapport à un ordonnancement classique ! Je débuterai mon exposé en expliquant quelques détails architecturaux importants par rapport à l'efficacité de l'exécution des threads d'une application. J'introduirai alors ce que j'entends par ordonnancement'',placement'' et ``migration'' des threads et bulles. Je présenterai ensuite la boîte à outils au travers de quelques exemples, et l'on pourra discuter notamment de la ressemblance intriguante avec des ambients.
Cet exposé, est une partie d’un article en cours, en collaboration avec {\it Latifa Faouzi} (Fes et Casablanca) et se compose de deux parties indépendantes.
PARTIE I: $k$-algèbre libre sur un monoïde.
On considère un corps commutatif $k$ et un monoïde (= demi-groupe commutatif et unitaire) $M$. On désigne par $k[M]$ la $k$-algèbre sur le monoïde $M$, i.e. l’espace vectoriel sur $k$ ayant $M$ comme base, c’est alors aussi un anneau puisque $M$ est stable par produit. L’exemple type étant l’algèbre des polynômes sur $k$. Le corps $k$ étant fixé, on montre plusieurs propriétés de la classe des algèbres sur un monoïde. Par exemple $k[X] x k[Y]$ est une $k$-algèbre libre sur un monoïde. On développe aussi une classe plus large où le produit de deux élements de $M$ est soit $0$, soit un élement de $M$.
PARTIE II: Demi-treillis compact. Dans cette partie, les monoïdes ne sont pas unitaires. On considère un triplet $(L,O,.)$ où $(L,O)$ est un espace compact séparé, $(L,.)$ est un monoïde idempotent (mais sans unité). On suppose que l’application $(x,y) -> x. y$ est continue. En interprétant $x . y$ comme l’infimum de $x$ et de $y$, $(L,.)$ est un (inf-)demi-treillis et $.$ est continue. Noter que $L$ est alors un ensemble ordonné en posant $x \leq y$ ssi $x . y = x$. On montre quelques propriété de cette classe de structures. Par exemple, une telle structure possède un plus petit élément $0$ et toute partie non vide et filtrante supérieurement possède un supremum. La topologie est alors déterminée par l’ordre: une sous-base de la topologie est formée d’élements de la forme $U_x := { y \in L : y \geq x }$ et $L \setminus U_x$ où $x$ est un élément “compact” de $L$. Ces notions de demi-treillis compacts apparaissent lors de l’étude des domaines et des treillis algébriques.
PARTIE III: Le lien. Si on considère le corps $k = {0,1}$ ayant deux éléments et le monoïde $M$ idempotent, alors $k[M]$ est une algèbre de Boole, dont l’espace des ultrafiltres (ou des idéaux maximaux) est un demi-treillis compact et “réciproquement”.
Bibliographie:
[1] Bourbaki N.: Eléments de mathématiques, Algèbre, Chapitres 1--3, Hermann, 1970.
[2] Lang S.: Algebra, Addision-Wiesley Pub, 1970.
[3] Gierz, G., Hofmann K. H., Keimel K., Lawson J. D., Mislove M. and Scott D. S.: Continuous lattices and domains, Encyclopedia of Mathematics and its Applications, 93. Cambridge University Press, Cambridge, 2003, 591 pp.
L'objectif de cet exposé est de présenter le contexte et les motivations ayant conduit à mon sujet de thèse : Géométrie multirésolution des objets discrets bruités. On commencera par présenter quelques outils classiques autour des droites discrètes et leurs applications à l'estimation de quantités géométriques sur des formes discrètes. L'extension de ces outils aux formes discrètes bruitées sera ensuite abordée. On en déduira les quelques axes de recherche qui seront explorés dans ma thèse.
Ce séminaire donnera les liens entre un problème de recouvrement des entiers et la combinatoire des mots afin d'étudier la conjecture de Fraenkel. Cette conjecture a été formulée dans le cadre de la théorie des nombres il y a maintenant plus de 30 ans. Elle prétend que pour k > 2 entier fixé, il y a une unique façon de recouvrir les entiers par $k$ suites de Beatty avec des fréquences deux à deux distinctes. Ce problème peut être exprimé en termes de combinatoire des mots de la façon suivante: pour un alphabet à k lettres, il existe une unique suite équilibrée avec des fréquences de lettres deux à deux distinctes qui est exactement la suite de Fraenkel notée $(F r_k )^{omega}$ où F r_k = F r_{k-1} k F r_{k-1}, avec F r_3 = 1213121. Cette conjecture est prouvée pour k = 3, 4, 5, 6 d'après les travaux de Altman, Gaujal, Hordijk et Tijdeman ainsi que dans d'autres cas particuliers. Dans ce séminaire, nous présenterons donc une synthèse sur ce sujet et la résolution de la conjecture dans un cas particulier.
TBA
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. Malgré la simplicité de cette règle locale, des comportements très variés peuvent être observés dans l'évolution d'une population de cellules.
Nous présentons ici quelques notions topologiques décrivant ces dynamiques. Nous nous intéressons en particulier à la nilpotence, qui correspond à un comportement ultimement stable. Nous en donnons une caractérisation utilisant la trace, qui est le mot infini représentant la suite des états pris par une cellule donnée.
Voir la page web idoine.