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.
Cette séance est consacrée au modèle booléen V^B de ZF, dont la construction est paramétrée par une algèbre de Boole complète B dans le modèle initial. Au programme: rappels de théorie des ensembles (classes et hiérarchie de Veblen), définition de la hiérarchie des B-ensembles, effondrement extensionnel, mélange de B-ensembles, principe du maximum et plénitude, conservation des propriétés Sigma_1, satisfaction des axiomes de ZFC.
Je présenterai ce qu'est une paramétrisation conforme d'une surface et son intérêt pour la géométrie discrète, en particulier la géométrie digitale, pour le plaquage de texture et le calcul des grandeurs géométriques d'une surface ou d'une courbe (normale, courbure...). Je discuterai de diffusion discrète, du laplacien discret dans le cadre des maillages et dans le cadre voxellique. La théorie de l'analyse conforme discrète qui est associée partage de nombreux points avec la théorie des surfaces de Riemann continue.
Les automates cellulaires ont cette riche dualité de pouvoir être à la fois considérés comme des systèmes dynamiques à temps et espace discret et comme des objets combinatoires simples proches des modèles de calcul de type machine. Cette dualité permet d'établir facilement des résultats de calculabilité et de complexité concernant la dynamique de ces objets. Dans cet exposé, nous abordons une propriété dynamique élémentaire : l'existence d'une période temporelle commune à toutes les configurations du système. Sans surprise, nous établissons l'indécidabilité de cette propriété. Pour établir ce résultat, les outils maintenant classiques liant pavages et automates cellulaires ne fonctionnent pas. C'est donc l'occasion d'exhiber de nouveaux outils adaptés et de redécouvrir d'anciens résultats sur les machines de Turing. Nous aborderons les notions de mortalité et de périodicité dans ce modèle de calcul, l'art et la manière de programmer dans un cadre réversible et nous montrons que le problème de l'immortalité des machines de Turing reste indécidable dans le cadre réversible. Ces travaux sont issus d'une collaboration avec J. Kari (Univ. Turku, Finlande)
Cet exposé commence par la présentation rapide de la règle Minorité stochastique et de ses particuliarités. Ensuite, je présenterai une application de cette règle pour modéliser la formation de quasi-cristaux.
Considérons un graphe où chaque sommet reçoit la couleur noire ou blanche. Une arête contient une erreur si elle relie deux sommets de la même couleur. Minorité est une dynamique stochastique minimisant rapidement l'énergie. Sous cette dynamique, un sommet, chosi aléatoirement et uniformément parmi l'ensemble des sommets, peut changer d'état si au moins la moitié des arêtes qui lui sont adjacentes sont erronées. Cette dynamique est sensible à la topologie du graphe et son analyse fine s'est révélée compliquée.
En physique, dans les annnées 70, il était conjecturé que toutes les structures ordonnées soient périodiques. En 1984, un contre-matériaux fût découvert et reçu le nom de quasi-cristal. Dès 1974, Penrose avait présenté un structure théorique ordonnée et apériodique. Le but de notre projet est de présenter un modèle pour expliquer la formation d'une telle structure. Pour cela, nous considérons le modèle des pavages par coupe et projection (qui contient le pavage de Penrose). En définissant une notion d'erreur et d'énergie sur ces pavages, la règle Minorité procédant par flips permet de converger rapidement expérimentalement vers une structure ordonnée qui selon la famille de pavages par coupe et projection considérée est soit périodique, soit apériodique. Je présenterai nos résultats expérimentaux ainsi que notre analyse de cette dynamique pour les pavages 2 vers 1 (mots sur deux lettres).
Les systèmes d'acquisition de données image en deux ou trois dimensions fournissent généralement des données organisées sur une grille régulière, appelées données discrètes. Que ce soit pour la visualisation ou l'extraction de mesures, la géométrie discrète définit les outils mathématiques et géométriques pour de nombreuses applications. Dans cet exposé, je présenterai comment adapter divers algorithmes de la géométrie discrète aux grilles irrégulières isothétiques. Ce modèle de grille permet de représenter de manière générique les structurations d'images en pixels ou voxels de taille et de position variables : les grilles anisotropes, très répandues en imagerie médicale, les décompositions hiérarchiques telles que quadtree/octree, les techniques de compression comme le run length encoding, etc. Plus précisément, je présenterai l'extension à cette représentation de plusieurs méthodologies largement étudiées pour analyser les formes discrètes: la reconstruction d'objets binaires complexes, la transformée en distance et l'extraction d'un axe médian. Je montrerai enfin comment ces outils sont employés dans diverses applications : la distinction de caractères ambigus dans un outil de reconnaissance de plaques minéralogiques, l'approximation dynamique de courbes implicites planaires et l'analyse d'objets discrets bruités.
Cette séance est consacrée au modèle booléen V^B de ZF, dont la construction est paramétrée par une algèbre de Boole complète B dans le modèle initial. Au programme: rappels de théorie des ensembles (classes et hiérarchie de Veblen), définition de la hiérarchie des B-ensembles, effondrement extensionnel, mélange de B-ensembles, principe du maximum et plénitude, conservation des propriétés Sigma_1, satisfaction des axiomes de ZFC.
Parmi les nombreuses structures ordonnées liées aux espaces topologiques, les treillis continus occupent une place importante. Ils constituent par exemple les espaces topologiques de Kolmogorov injectifs. Nous nous proposons ici de présenter ces treillis d'un point de vue algébrique au travers de la notion de monade et d'adjonction de Galois. La définition originelle d'espace topologique donnée par Hausdorff en 1914 apparaît alors de façon naturelle, et nous permet de jeter un regard neuf sur le résultat d'injectivité mentionné ci-dessus.
Voir la page dédiée.
TBA
Nous construisons une structure de modeles de Quillen pour la categorie des omega-categories strictes, a partir d'un ensemble de cofibrations generatrices et d'une classe d'equivalences faibles. Toute omega-categorie est fibrante par rapport a cette structure, alors que les omega-categories cofibrantes sont precisement les libres.