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.
En s'inspirant de certaines constructions de la ludique, on definit une realisabilite par orthogonalite pour la semantique des jeux de la logique lineaire intuitionniste. On demontre ainsi, sans passer par l'elimination des coupures, que l'interpretation d'une preuve (y compris avec coupures) est une strategie totale (analogue de la terminaison dans les jeux).
Can we build a program that understands informal mathematical text and can we mechanically verify it's correctness? MathNat project aims at being a first step towards answering this question. We develop a controlled language for mathematics (CLM), which is a precisely defined subset of English with restricted grammar and dictionary. Like textbook mathematics, CLM supports some complex linguistic features to make it natural and expressive. A number of transformations are further applied on it to completely formalise it. In this presentation, I'll give an overview of this work and report the current state and future directions. Web: http://www.lama.univ-savoie.fr/ humayoun/phd/mathnat.html
L'étude la microstructure des matériaux granulaires nécessite souvent de séparer numériquement les grains de leurs voisins. A cause d'effets thermodynamique et mécanique, toute couche de neige non fraîche est dégradée de différentes façons. Le principal problème est donc de choisir une définition géométrique d'un ``grain'' qui soit cohérente avec la physique et la mécanique de la neige. Les images microtomographiques au rayon X de la structure de la neige ne fournissent aucune information directe sur les frontières entre les grains. Pour résoudre ce problème, nous faisons appel à une approche basée sur la géométrie discrète. En travaillant sur la surface de la structure neigeuse, il est possible de calculer sa courbure Gaussienne et moyenne. Muni de ces informations, il devient possible de séparer la surface en deux régions. En utilisant un diagramme de Voronoi, ces régions sont étendues à l'objet entier. Les voxels dans la région négative sont retirés de l'image, fournissant ainsi une segmentation en objets déconnectés. Ces objets sont alors utilisés comme graines pour un second diagramme de Voronoi.
Les travaux que je présenterai sont ceux effectués lors de ma thèse. Ils s'inscrivent dans le cadre de la géométrie discrète, une discipline ayant pour objectif de définir un cadre théorique pour transposer dans Z^n les bases de la géométrie euclidienne -- les notions discrètes définies étant le plus proche possible des notions continues que nous connaissons (telles que distance, droite, convexité, ...). De nombreuses études ont déjà été menées au sein de cette discipline, pour en définir l'espace de travail ainsi que les objets fondamentaux manipulés et en saisir leurs propriétés. Des algorithmes de reconnaissance pour ces primitives discrètes ont été développés et utilisés dans des problèmes comme la reconnaissance de formes, l'extraction de caractéristiques géométriques et bien d'autres encore. Néanmoins, la majorité des études ont été effectuées en se reposant sur la régularité des structures fondamentales de l'espace discret, souvent issues de définitions arithmétiques, et ces critères de régularité sont généralement essentiels aux différents algorithmes développés. Or, en pratique, les objets manipulés sont très souvent bruités par les méthodes d'acquisition (scanners, IRM, ...) qui suppriment ce caractère régulier des objets. Dans cet exposé, nous nous intéressons aux objets discrets 3D et proposons une primitive discrète, le morceau flou de plan discret, destinée à apporter plus de flexibilité dans les traitements, afin de concevoir des algorithmes capables de fournir des résultats satisfaisants aussi bien sur des objets réguliers que non réguliers. Avec l'emploi de cette nouvelle primitive discrète, nous définissons différents estimateurs de caractéristiques géométriques au bord d'objets discrets et montrons comment les utiliser dans des problèmes de segmentation et de polyédrisation d'objets discrets possiblement bruités.