In this talk, we discuss how to model in a finite way the semantics of resource-allocating interactive programs. Surprisingly, in doing so, the notion of behavioural symmetry arises from the framework, and is necessary to recover canonical models. Behavioural symmetry expresses properties relating the semantics of a program and the available resources at each state, e.g. ``the distinguished variables x and y have the same observable effect, and swapping them does not affect the semantics of the program''. Labelled transition systems (LTSs) have been successfully used to model the semantics of interactive programming languages. Their natural equivalence relation, the so-called bisimilarity, is a fundamental tool for the study of such languages. However, when resources (e.g. memory locations) can be allocated and de-allocated along transitions, bisimilarity becomes a non-standard notion (cf. the pi-calculus). The categorical abstraction of coalgebras generalises LTSs and has an associated, general definition of behavioural equivalence, coinciding with bisimilarity for LTSs. Presheaves generalise classical sets; elements of presheaves have intensional features such as interfaces, or resources, and operations on them. By using coalgebras in a category of presheaves, bisimilarity in the presence of resource allocation is recovered from the standard categorical definition. However, the obtained transition systems become infinite state machines because of fresh resources. An equivalence between categories of presheaves and of families recovers a finite representation for memory-bound programs. An associated notion of symmetry is necessary for the equivalence to hold, and for final systems (=canonical models) to exist, giving rise to behavioural symmetry.
Cet exposé, faisant suite au précédent sur les préfaisceaux, est une introduction aux faisceaux, un autre important outil catégorique dérivé des premiers. Je rappellerai le lemme de Yoneda, puis définirai les notions de crible, topologie de Grothendieck et enfin faisceau, en m'appuyant sur des exemples et contre-exemples. Si le temps le permet, je survolerai le théorème du faisceau associé, qui construit un faisceau à partir d'un préfaisceau arbitraire (si Christophe est là, on parlera de PML). Enfin, peut-être, je raconterai en deux mots mon travail avec Damien Pous, qui repose sur une description en termes de faisceaux des stratégies dites ``innocentes'' en sémantique des jeux.
En 1998, Pestov montra que le groupe G des automorphismes des rationnels (vus comme ensemble ordonné) est extrêmement moyennable, c'est-à-dire que toute action continue de G sur tout espace topologique compact admet un point fixe. Pour ce faire, il démontra que la propriété énoncé ci-dessus est équivalente au théorème de Ramsey fini. Ce résultat constitue le point de départ des travaux de Kechris, Pestov et Todorcevic, qui établirent en fait qu'il s'agit là d'un phénomène général liant théorie de Ramsey pour certaines classes de structures finies (classes de Fraïssé) et moyennabilité extrême pour certains groupes topologiques. Le but de cet exposé sera de présenter la correspondance de Kechris-Pestov-Todorcevic ainsi que certaines de ces conséquences.
Cet exposé est une introduction aux préfaisceaux, un important outil catégorique. Je reprendrai du début: catégories, foncteurs, transformations naturelles, en considérant de nombreux exemples petits et gros. Je concluerai par le lemme de Yoneda en donnant l'exemple des graphes.
IR' is a powerful principle for in the context of dependent type-theory, for defining simultaneously a set U *inductively*, with a function T : U -> D *recursively*. D may belarge', eg the type of Sets, and a paradigm example is a universe of (codes for) sets. I will try to motivate and illustrate this principle. Using containers (a particular kind of endofunctor on Set), one can distill out the essence of IR in an extremely compact, memorable form. I will try to give a tour of the distillery.
Dans cet exposé, nous montrerons comment utiliser la combinatoire des mots et la théorie des automates afin d'étudier certaines propriétés arithmétiques des séries de Laurent à coefficients dans un corps fini. En particulier, à l'aide d'une méthode inspirée par un article d'Adamczewski et Cassaigne, nous donnerons une majoration générale de l'exposant d'irrationalité des séries algébriques. Nous illustrerons cette approche à l'aide de quelques exemples.
I shall dust off some work by Bohm, on arithmetical features of combinatory logic. The natural combinators for addition, multiplication, exponentiation and nihilation of Church satisfy some pleasing algebraic laws resembling those of ordinal arithmetic. But they also satisfy and some other ''wild'' laws (resembling nothing arithmetical) in virtue of which they are combinatorially complete. Because of that, they support a notion of logarithm (with respect to a ''base''). I may add some remarks on ''exponentiality'', which says that two ''numbers'' are the same if they have the same behaviour as exponents.
Tout le monde aime les automates cellulaires, tout le monde aime les fractales, et l'on sait bien que celles-ci peuvent être produits par ceux-là. Par exemple, le triangle de Sierpinski, comme il s'agit du triangle Pascal modulo 2, est le diagramme espace-temps limite d'un automate cellulaire correspondant à la relation C(n+1,k+1)=C(n,k)+C(n,k+1). Plus généralement, il est connu que si l'alphabet a une structure d'anneau commutatif et que l'automate cellulaire est un morphisme d'anneaux - on parle alors d'automate cellulaire linéaire - une structure fractale va émerger de ses diagrammes espace-temps. Remplaçons maintenant l'anneau par un simple groupe - non, pas un groupe simple, un simple groupe abélien fini. J'expliquerai pourquoi, à mon sens, c'est dans ce cas plus général qu'on devrait parler d'automate cellulaire linéaire, et non pas seulement dans le cas des anneaux comme on le fait habituellement ; et surtout, je tâcherai de faire comprendre pourquoi leurs diagrammes espace-temps ont aussi des propriétés fractales.
Le size-change termination principle'' est un test (correct mais forcément incomplet) pour décider la terminaison de programmes mutuellement récursifs. Ce test, dû à A. ben Amram, N.D. Jones et C.S. Lee est particulièrement simple et élégant, tout en étant relativement puissant et modulaire. Il s'agit essentiellement d'une opération de clôture transitive sur le graphe d'appels des fonctions et la preuve de correction repose sur le théorème de Ramsey infini. Quand le langage des définitions récursives est un langage avec constructeurs / destructeurs à la ML, il y a une notion naturelle de taille : le nombre de constructeurs dans une valeur. Dans ce contexte, on peut généraliser le test pour conserver plus d'information que la seule taille des arguments. Ceci permet notamment d'ignorer certains chemins du graphe d'appels qui ne correspondent à aucune suite concrète d'appels. Par contre, la preuve de correction du nouveau principe est plus complexe que l'originale. Après une rapide présentation du test original, je décrirais cette extension et donnerai certaines idées de la preuve de correction. Comme le test est implanté (en Caml) pour le langage PML, je donnerais également des exemples (etcontre exemples'') pour permettre de se faire une idée des définitions acceptées (et refusées).
Je présenterai un modèle localisé de la logique linéaire multiplicative basé sur des graphes à partir duquel il est possible d'obtenir une catégorie *-autonome ainsi que de définir une notion de vérité. Je montrerai également qu'une restriction de ce modèle à une certaine classe de graphes se plonge dans la géométrie de l'interaction hyperfinie de Girard. Ceci permet d'appréhender de manière purement combinatoire le cadre utilisant des éléments d'analyse fonctionnelle avancés introduit par Girard. J'expliquerai enfin comment adapter ce modèle pour l'étendre à la logique linéaire multiplicative-additive, et discuterai d'une extension aux exponentielles.
TBA
Les courbes frontières définissent les régions ou les formes du plan de manière compacte et descriptive. Il est bien connu que les formes doivent être étudiées à différentes échelles. Ceci a conduit au développement des pyramides régulières et irrégulières pour l'analyse des formes et la compréhension des scènes. Cependant, il n'existe pas une description analytique de la multi-résolution d'une forme numérique, contrairement au célèbre espace-échelle (scale-space) dans le monde continu. En outre, les primitives géométriques telles que les lignes, les cercles ou les polynômes ont une grande importance dans le contexte de la géométrie numérique. Les morceaux des droites numériques sont un bon moyen pour estimer les tangentes et les arcs discrets approchent la courbure. Il est donc nécessaire de les garder dans l'analyse multi-échelle des frontières numériques. Un des objectifs de cette thèse est de donner des nouveaux résultats analytiques sur la multi-résolution des droites 4-connexes et des segments de droites 4-connexes. Figueiredo est le premier qui a étudié le comportement des droites 8-connexes lors du changement de la résolution de la grille. Dans le présent travail, nous considérons une droite 4-connexe pour laquelle une description analytique est fournie lorsque la résolution de la grille est modifiée par un facteur arbitraire. En plus, nous montrons que leurs couvertures sont des droites 4-connexes. Comme les formules analytiques des segments de droite sont un problème beaucoup plus difficile, nous proposons un parcours indirect pour la multi-résolution d'un DSS en utilisant le fait qu'un segment est un morceau fini d'une droite discrète. Etant donné un DSS, nous construisons deux droites dont l'intersection le contient et dont la partie connexe principale a les mêmes caractéristiques arithmétiques, ainsi que le même nombre de motifs. Notons que nous proposons de nouveaux résultats combinatoires des intersections de droites. Nous déterminons la multi-résolution du segment en examinant la multi-résolution de l'intersection de ces deux droites. Nous donnons une nouvelle description analytique de cet ensemble avec les inégalités arithmétiques. Nous abordons également le problème du calcul des caractéristiques exactes d'un sous-segment d'une droite 4-connexe qui a des caractéristiques connues. Nous présentons deux nouveaux algorithmes SmartDSS et ReversedSmartDSS qui résolvent ce problème. Leur principe est de se déplacer dans l'arbre de Stern-Brocot de la fraction soit de manière haut-bas ou bas-haut. Dans le pire cas, leur complexité est meilleure que l'algorithme de reconnaissance DSS classique. Les deux algorithms peuvent dès lors servir à calculer efficacement la multi-résolution d'un segment. Les bruits tout au long des contours numériques ne sont pas vraiment détectés, mais plutôt annulés par l'épaississement des segments de droites 4-connexes. De plus, l'épaisseur est réglée par un utilisateur et aussi définie globalement pour le contour. Pour surmonter ce problème, nous proposons une stratégie originale pour détecter localement à la fois la quantité de bruit et les épaisseurs significatives de chaque point de contour. Ce travail se base sur les propriétés asymptotiques de segments flous d'épaisseurs différentes, et forme une alternative à l'approche multi-résolution de la détection du bruit.
La classe des mots C∞, ou facteurs lisses, est la classe des mots finis qui sont arbitrairement dérivables. Ils ont été défini par Dekking pour décrire l'ensemble des facteurs du fameux mot de Kolakoski, le mot infini point fixe du codage par plages. Nombre de conjectures sur le mot de Kolakoski et ses facteurs restent ouvertes. Nous introduisons une nouvelle représentation des mots C∞ basée sur un codage de ces mots sur un alphabet à trois lettres. Ceci permet de classifier les mots C∞ en classes d'équivalence. Ces classes d'équivalence peuvent être représentées sur un graphe infini dont nous étudions les propriétés. Nous démontrons que ce graphe peut être décrit inductivement par une fonction récursive dont la définition est totalement indépendante du contexte des mots C∞.
B. Kerautret et J.-O. Lachaud ont proposé en 2009 un estimateur de bruit local sur les contours discrets 2D. Leur méthode consiste en une analyse multi-échelle des longueurs des segments maximaux en chaque point du contour. L'étude de la courbe du profil multi-échelle et la connaissance du comportement asymptotique de ces longueurs permettent, entre autre, de détecter du bruit en chaque point du contour ainsi que l'échelle significative. Nous proposons d'étendre cette méthode à la détection de bruit local sur les contours discrets tridimensionnels. Pour cela, nous nous orientons vers une analyse multi-échelle des plans discrets maximaux couvrant chaque point du contour. Nous choisissons dans un premier temps d'étudier le critère de l'aire discrète et nous espérons observer un comportement asymptotique caractéristique. Ces travaux sont actuellement en cours.
Dans cet exposé, nous allons présenter un outil important pour la construction des mots de Sturm (et donc également pour les droites discrètes) que l'on nomme la clôture palindromique. Nous allons étendre cette notion pour atteindre des mots infinis comme les mots de Rote ou encore la fameuse suite de Thue-Morse. Enfin, nous montrerons comment calculer les diverses clôtures d'une façon efficace.
Notions of cartesian closed sketches have been proposed as a categorical approach to algebra with binding. We here consider a 2-dimensional refinement of this idea, called cartesian closed 2-signatures, as a categorical approach to higher-order rewriting, i.e., rewriting with variable binding. We sketch a general notion of standardisation in the sense of Lévy (1980).
Cellular automata are both a powerful model of computation and a continuous function on a Cantor space. So the notion of equicontinuity is naturally defined, and corresponds to the ability to block any communication. This property is most of the time considered along the line (x=0). Mathieu Sablik extended it first to all lines, and here we want to deal with automata that are equicontinuous along any curve. I’ll present a classification of cellular automata considering it, with examples, and some dynamical consequences.
Dans cet exposé, on s'intéresse aux catégories de réponse (des catégories avec les produits finis et un objet exponentiel, introduites par Selinger) sous deux aspects :
Dans cet exposé, nous cherchons à colorier proprement des graphes de sorte que deux sommets adjacents n'aient pas le même ensemble de couleurs dans leur voisinage fermé. On peut par exemple colorier de cette manière n'importe quel graphe biparti avec 4 couleurs, mais savoir si l'on peut colorier un graphe biparti avec seulement 3 couleurs est NP-complet. Nous nous interesserons aussi à une autre classe de graphes : les graphes triangulés pour lesquels nous pensons que 2*k couleurs sont suffisantes, avec k la taille de la plus grande clique. Enfin, je donnerai des relations avec le nombre chromatique et avec le degre maximum du graphe.
Dans cet exposé (très largement inspiré des travaux de Krivine présentés en juin dernier), je propose d'étudier à travers la correspondance de Curry-Howard la transformation de preuves sous-jacente à la méthode de forcing. Pour cela, je me placerai en arithmétique d'ordre supérieur (PAw) avec termes de preuves à la Curry. Je définirai d'abord la transformation qui à une proposition A associe la proposition p ||- A (où p est une condition arbitraire), puis une transformation t |-> t^ sur les termes de preuves bruts (i.e. non typés) telle que si t : A, alors t^ : p ||- A. Je montrerai alors comment le terme traduit effectue ses calculs, et en quoi il est légitime de voir cette transformation comme la mise en place d'un petit système d'exploitation.