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.
Je vais vous présenter mes activités de recherche de thèse et de post-doc qui peuvent être regroupées sous le thème général de la modélisation géométrique et topologique. En particulier, je me suis intéressée au problème de la génération de maillages surfaciques et volumiques à partir d'images 3D multi-labels.
L'étude de la combinatoire des mots a mené à la caractérisation de nombreux langages. Certains admettent (ou sont fondés sur) une interprétation géométrique. En particulier, une condition nécessaire et suffisante à la convexité discrète s'énonce en termes de mots de Lyndon et de Christoffels. À partir de cette caractérisation, vient naturellement la notion de convexité minimale. Ces ``mots non-convexes minimaux'' possèdent une structure combinatoire particulière et sont reliés aux MLP (minimum length polygon).
L'axe médian est un outil de représentation d'objets binaires par ensemble de boules, et est couramment utilisé en analyse d'images. Soit (E,d) un espace métrique, et S une forme binaire incluse dans E. Une boule B (pour la distance d) est dite maximale dans S si elle est incluse dans S mais n'est incluse dans aucune autre boule incluse dans S. L'Axe Médian de S est défini comme l'ensemble des boules maximales de S [Blum 67, Pfaltz et Rosenfeld 67]. Nous présentons plusieurs nouveaux résultats concernant le calcul de l'axe médian, dans le cas de la géométrie discrète (E=Z^n), pour la distance euclidienne et les normes de chanfrein (discrétisation dans Z^n des jauges polyédrales). Nous procédons par recherche locale : nous donnons des caractérisations de voisinages de test suffisants pour calculer l'axe médian. Nous verrons comment ces voisinages dépendent de la distance considérée, ainsi que de l'épaisseur de la forme étudiée. En particulier, nous établissons des liens avec des outils bien connus de l'arithmétique, tels que les suites de Farey et le problème de Frobenius.
Dans cette présentation, nous nous intéressons à la segmentation d'images, et plus particulièrement à la segmentation de catégories d'objets. Si les modèles d'apparence par sac-de-mots donnent à ce jour les meilleures performances en terme de classification d'images et de localisation d'objets, ils ne permettent pas de segmenter précisément les frontières des objets. Parallèlement, les modèles basés sur des champs de Markov (MRF) utilisés pour la segmentation d'images se basent essentiellement sur les frontières et permettent une régularisation spatiale, mais utilisent difficilement des contraintes globales liées aux objets, ce qui est indispensable lorsqu'on travaille avec des catégories d'objets dont l'apparence peut varier significativement d'une instance à l'autre. Nous verrons comment combiner ces deux approches. Notre approche comporte un mécanisme basé sur la détection d'objets par sac-de-mots qui produit une segmentation grossière des images, et simultanément, un second mécanisme, lui basé sur un MRF, produit des segmentations précises. Notre approche est validée sur plusieurs bases publiques de référence, contenant différentes classes d'objets en présence de fonds encombrés et présentant de larges changements de points de vue.
Je présenterai deux ordres que l'on peut définir sur les pavages: un premier basé sur la dérivée topologique (le rang de Cantor-Bendixson) et un second plus combinatoire basé sur les motifs que l'on peut trouver dans un pavage. Ces deux ordres, étudiés indépendamment, permettent d'obtenir des propriétés sur les ensembles de pavages. Nous verrons comment combiner les deux pour obtenir des résultats plus précis: sous l'hypothèse de n'avoir qu'une infinité dénombrable de pavages possibles nous arrivons à montrer qu'il existe des pavages n'ayant qu'une seule direction de périodicité; nous arrivons aussi à caractériser les ensembles de pavages ayant la cardinalité du continu.
Algebraic set theory was introduced by Joyal and Moerdijk in their book from 1995 and is an approach to the semantics of set theory based on categorical logic. One of its strengths is that it gives a uniform approach to set theories of different kinds (classical and constructive, predicative and impredicative). In addition, it allows one to capture different kinds of semantics (forcing, sheaves, boolean-valued models, realizability) in one common framework. In this talk, I will give an introduction to the subject, concentrating on main ideas rather than technical details.
Dans les cours précédents, nous avons construit le modèle booléen V^B de ZF et montré la satisfaction des axiomes de ZFC. Dans cette ultime séance de cours, nous allons nous intéresser aux cardinaux dans le modèle, et construire un modèle réfutant l'hypothèse du continu. Au programme: condition de (anti-)chaîne dénombrable, ensemble de conditions, forcing et modèles booléens, réels de Cohen.
Les automates cellulaires (AC) sont des systèmes dynamiques à temps et espace discret. Ils sont l'un des modèles formels les plus utilisés pour étudier des systèmes complexes. Bien que les applications concernent principalement les AC en dimension 2 ou supérieure, les études formelles ont été menées surtout en dimension 1. Dans cet exposé je présente des résultats sur la dynamique des AC en dimension 2. Ces résultats sont obtenus par deux constructions qui permettent de considerer un AC en dimension 2 comme un AC en dimension 1.
Normalization by Evaluation (NbE) is an abstract framework for computing the full normal form of lambda-terms through an interpreter, just-in-time compiler or an abstract machine. While computational equality such as beta is part of every dependent type theory, the status of extensional laws such as eta is less clear. The reason is that eta needs a typed equality but many type theories (like Pure Type Systems) are formulated with untyped equality in order to decide equality by rewriting.
In this talk, I am arguing that NbE is the tool of choice to implement typed beta-eta equality for dependent type theory. I present typed NbE which computes eta-long normal forms, and show how to construct a model of (possibly impredicative) type theory that proves the correctness of NbE. Hence, NbE can be used to decide the built-in (``definitional'') equality of type theory with eta-rules.
The aim of this work is to provide foundational justifications of powerful type theories with beta-eta equality, such as the Calculus of Inductive Constructions.
Ce travail se situe à l'interface entre l'analyse d'images, dont l'objectif est la description automatique du contenu visuel, et la géométrie discrète, qui est l'un des domaines dédiés au traitement des images numériques. Dans ce cadre, nous avons considéré les régions homogènes et porteuses de sens d'une image, avec l'objectif de représenter leur contour au moyen de modèles géométriques ou de les décrire à l'aide de mesures. Nous nous sommes concentrés sur trois modèles géométriques discrets définis par la discrétisation de Gauss : la partie convexe ou concave, l'arc de cercle discret et le segment de droite discrète. Nous avons élaboré des algorithmes dynamiques (mise à jour à la volée de la décision et du paramétrage), exacts (calculs en nombres entiers sans erreur d'approximation) et rapides (calculs simplifiés par l'exploitation de propriétés arithmétiques et complexité en temps linéaire) qui détectent ces modèles sur un contour. L'exécution de ces algorithmes le long d'un contour aboutit à des décompositions ou à des polygonalisations réversibles. De plus, nous avons défini des mesures de convexité, linéarité et circularité, qui servent à l'introduction de nouveaux modèles dotés d'un paramètre variant entre 0 et 1. Le paramètre est fixé à 1 quand on est sûr de la position du contour, mais fixé à une valeur inférieure quand le contour est susceptible d'avoir été déplacé par un bruit d'acquisition. Cette approche pragmatique permet de décomposer de manière robuste un contour en segments de droite ou en parties convexes et concaves.