L'analyse de la langue naturelle est toujours un problème ouvert au sens où il n'a pas à ce jour d'outils disponible resolvant ce problème (qui est pourtant fini si l'on considère que la longueur des phrases est bornées par la plus longue phrase de Proust). Certaines approches reposent sur des concepts théoriques avancés (automates, théorie des types, jusqu'à MELL ou IMELL dans certains articles). Est-ce la bonne approche ? Ou bien juste le fait que l'algorithme est trop complexe pour être écrit à la main ? On va montrer que dypgen (Emmanuel Onzon) permet d'aller assez loin, sans toutefois analyser le présent résumé, en utilisant juste une juxtaposition d'idées au dessus des techniques récentes de parsing pour les grammaires hors contexte. Note: je n'expliquerai pas ce qu'il y a sous le capot de dypgen ... Pour ça, il faudra inviter Emmanuel Onzon.
TBA
A monad with arities'' is a monad T on some category K together with some extra data expressing the basicshapes'' of the operations involved in the structure of a T-algebra. There is a general result, called the nerve theorem, which in the case where K is a presheaf category, shows that the notion of monad with arities is an efficient reformulation of the notion of limit sketch''. The nerve theorem is so named because it generalises the characterisation of the simplicial sets that arise as nerves of categories. Other interesting instances of this result relevant for higher dimensional algebra involvelocal right adjoint monads'' -- such a T comes with a canonical choice of arities. These examples formalise the passage between the operadic and simplicial approaches to higher category theory.
Parmi les nombreuses suites remarquables étudiées en combinatoire des mots figurent les suites sturmiennes. Elles interviennent dans plusieurs domaines: dynamique symbolique, géométrie discrète, astronomie, cristallographie, etc. Elles sont d'autant plus remarquables par le fait qu'elles possèdent plusieurs caractérisations équivalentes. Entre autres, elles décrivent les droites discrètes de pentes irrationnelles. Parmi ces droites, la classe des (demies) droites passant par l'origine, appelées des suites sturmiennes standards, admet une caractérisation supplémentaire: il est possible de les construire en utilisant la fermeture palindromique itérative. La fermeture palindromique d'un mot fini w consiste à trouver le mot palindromique le plus court ayant comme préfixe le mot w. La fermeture palindromique itérative d'un mot fini w, noté Pal(w), est définie par Pal(a)=a et Pal(w)=(Pal(w_0...w_{n-1})w_n)^+, où u^+ désigne la fermeture palindromique et a est une lettre de l'alphabet. Ainsi, à tout mot sur un alphabet à 2 lettres, on peut lui associer une suite sturmienne standard en appliquant l'opérateur de fermeture palindromique itérative. Plus récemment, cette notion a été généralisée à des pseudopalindromes, c'est-à-dire des mots restant stables non pas sous l'opération d'image miroir, mais plutôt sous l'action d'un antimorphisme involutif.
D'autre part, certaines suites points fixes sous un opérateur se sont révélées être bien mystérieuses; il suffit de penser au célèbre mot de Kolakoski K=221121221221121122... qui est le point fixe sous l'opérateur de codage par blocs (le mot est égal à ses longueurs de blocs de lettres: 2'' lettres 2,2'' lettres 1, 1'' lettre 2,1'' lettre 1, ...). Plusieurs propriétés combinatoires de ce mot sont encore inconnues: la fréquence des lettres, la récurrence des facteurs, la fermeture de l'ensemble de ses facteurs sous l'image miroir et la complémentation, etc.
Ainsi, avec D. Jamet et G. Richomme, nous nous sommes intéressés à l'étude des points fixes sous l'opérateur de fermeture pseudopalindromique itérative. Dans mon exposé, je vais présenter certains de nos résultats concernant les propriétés combinatoires de ces mots et faisant intervenir entre autres des développements en fractions continues et des morphismes. Je terminerai en proposant certains problèmes ouverts concernant l'algébricité de la ``pente'' de certains de ces points fixes et l'existence d'exposants critiques.
Voir la page dédiée.
Un problème fondamental dans la comparaison de différents modèles du parallélisme et de la concurrence est celui de définir la notion de codage, ou de traduction. A ce jour, parmi toutes les notions universellement acceptées de codage entre modèles concurrents, il n'en existe aucune qui s'impose nettement sur les autres. Nous proposons d'étudier la notion de codage en partant de la vision du calcul comme réécriture, et en utilisant des notions venant de la théorie des catégories d'ordre supérieur et de la théorie des structures d'évenemments de Winskel.
Pure, or type-free, linear lambda calculus is Turing complete once reduction is considered as computation. We introduce modal impredicativity as a new form of impredicativity causing reduction to be problematic from a complexity point of view. Modal impredicativity occurs when, during reduction, a residual of a box b interacts with the body of another residual of b. Technically speaking, superlazy reduction is a new notion of reduction that allows to control modal impredicativity. More specifically, superlazy reduction replicates a box only when all its copies are opened. This makes the overall cost of reducing a (linear) lambda-term finite and predictable. Specifically, superlazy reduction applied to any pure proof nets takes primitive recursive time. Moreover, any primitive recursive function can be computed by a lambda-term via superlazy reduction.
Dans cet exposé, nous allons d’abord présenter les logiques modales plates de point fixe (flat modal fixpoint logics). Chaque logique de ce type est une extension de la logique modale K et, au même temps, un fragment du $\mu$-calcul modal propositionnel. Nous aborderons le problème de trouver, de façon uniforme, une axiomatisation de ces logiques qui soit complète par rapport à leur interprétation standard sur les modèles de Kripke.
Nous verrons comme certaines idées de l’algèbre, de la coalgèbre, et de la théorie des catégories, sont fondamentales pour notre but: la dualité, par la notion de modalité de couverture, les adjoints, avec la généralisation aux O-adjoints, les objets libres, la notion de point fixe constructif, les rétractés. Ainsi, nous serions en mesure de proposer une axiomatisation complète pour chaque logique plate de point fixe. (Travail en collaboration avec Yde Venema).
Voir la page dédiée.
Je dirai où en est PML, notamment, l'algorithme de typage et le proof-checking. Je montrerai les premiers exemples de programmes prouvés en PML.
The aim of this talk is to present the problem of enumerating terms in untyped lambda calculus. The very first idea was to compute the asymptotic density of strongly normalizing closed lambda terms among all closed terms of a given size. However, the preliminary task of counting lambda terms turned out to be already non-trivial and challenging and this is therefore as the main theme. I will show recent results which were obtained due to cooperation between universities in Chambery, Versailles and Krakow.
Les sémantiques de jeux ont été introduites pour capturer le comportement interactif des preuves en interprétant les formules par des jeux sur lesquels les preuves induisent des stratégies. L'une des difficultés majeures lors de la définition de telles sémantiques, est de les rendre précises, c'est-à-dire de caractériser les stratégies définissables, qui sont l'interprétation d'une preuve (ou d'un programme par la correspondance de Curry-Howard). L'extension des caractérisations habituelles à des langages de programmation comportant des constructions concurrentes nécessite de repenser en profondeur les définitions habituelles de sémantique des jeux, en menant une analyse fine de la structure dépendances entre les coups dans les stratégies. Nous présentons ici deux approches axiomatiques pour décrire cette structure : l'une externe, fondée sur la présence de certaines tuiles de permutation de coups dans les stratégies, l'autre interne, décrivant la catégorie des stratégies comme une structure algébrique libre.
Voir la page dédiée.
Au début des années 60, Wang a introduit un modèle de pavage du plan à l'aide de tuiles orientées de taille unitaire aux bords colorées pour résoudre des problèmes de logique. Ce modèle a été montré Turing-équivalent par Berger qui montra qu'un jeu de tuiles pouvait simuler une machine de Turing. Nous nous intéressons a la calculabilité de ce modèle en introduisant des outils sur les pavages permettant d'obtenir des résultats plus généraux sur les jeux de tuiles. A l'aide de notions de simulation, nous obtenons une première approche de l'universalité puis, nous montrons quelques uns des théorèmes fondamentaux de la calculabilité (Kleene, Rice...), dans le cadre des pavages, toujours relativement à certaines notions de simulation. Ces résultats nous permettront d'obtenir dans un premier temps de nouvelles preuves sur des théorèmes classiques des pavages et dans un deuxième temps de construire un cadre de construction de jeux de tuiles apériodiques.
Dans cet exposé, nous commencerons par résumer les résultats connus sur les modèles classiques de piles de sable (SPM, IPM(k)) et sur quelques-unes de leurs extensions. Nous verrons que l'approche combinatoire a des limites, justifiant ainsi leur étude au travers d'un nouveau système dynamique discret, les automates de sable.
Nous définirons ce système, en rappelant en permanence les liens existant entre celui-ci et un autre système dynamique mieux connu, les automates cellulaires. Puis, après avoir rappelé quelques-une des propriétés basiques des automates de sable, nous définirons des propriétés dynamiques à l'aide d'une topologie compacte inspirée de celle utilisée pour l'étude des automates cellulaires.
Ces propriétés permettent une étude plus globale de la dynamique d'un modèle donné, avec des techniques topologiques puissantes. Nous verrons ainsi comment classer les automates selon leur ``chaoticité'', en s'inspirant de la classification pour les automates cellulaires 1D de Kůrka. Ces résultats permettent de souligner que les automates de sable sont un système intermédiaire entre les automates cellulaires de dimension d et d+1.
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 »...