Many methods have been proposed to estimate differential geometric quantities like curvature on discrete data. A common characteristics is that they require (at least) one user-given scale parameter, that smooths data to take care of both the sampling rate and possible perturbations. Digital shapes are specific discrete approximation of Euclidean shapes, which come from their digitization at a given grid step. They are thus subsets of the digital plane Z^d. A digital geometric estimator is called multigrid convergent whenever the estimated quantity tends towards the expected geometric quantity as the grid step gets finer and finer. The problem is then: can we define curvature estimators that are multigrid convergent without such user-given parameter ? If so, what speed of convergence can we achieve ? We present here three digital curvature estimators that aim at this objective: a first one based on maximal digital circular arc, a second one using a global optimisation procedure, a third one that is a digital counterpart to integral invariants and that works on 2D and 3D shapes.
Je parlerai d'un travail récent qui se trouve à l'intersection entre la logique et la complexité algorithmique. Depuis plusieurs années, de nombreux systèmes logiques capturant des classes de complexité ont été étudiés, certains obtenus comme des systèmes dérivés de la logique linéaire de Girard -- les logiques linéaires bornées. En étudiant des modèles mathématiques de logiques linéaires bornées, on peut montrer une correspondance entre une hiérarchie de classes de complexité et une hiérarchie d'objets mathématiques -- les graphages. Ce résultat ouvre la porte à l'utilisation d'invariants de cohomologie définis sur les graphages en complexité.
Weighted automata are a structure that has many applications in computer science (speech recognition, natural language processing, image processing, quantitative modelling, etc). Weighted language equivalence is one possible semantics for these weighted automata. This equivalence is decidable for automata with weights on a field, but the proof relies heavily on the properties of fields. However, weighted automata can be defined more generally on a semiring, or even on structures where the addition is defined only partially. This talk explains how the result of decidability for weighted language equivalence for automata on fields can be extended to a decidability result for a certain class of semirings and ``partial semirings''.
Je ferai une présentation rallongée de l'article LICS du même nom. Il s'agit de donner une caractérisation, pour une classe importante de modèles du lambda-calcul non typé, de la pleine adéquation pour la normalisation de tête (i.e. pour H*). On montrera en effet qu'il est pour cela nécessaire et suffisant d'être hyperimmune. L'hyperimmunité est une notion que nous introduirons qui demande à ce que les comportements mal fondés du modèle ne soient pas capturables par des fonctions récursives. Ce résultat sera notamment utilisé comme prétexte et exemple pour l'introduction d'un outil central dans ma thèse: les lambda-calculs avec tests. Il s'agit d'enrichir le lambda-calcul non typé avec des opérateurs directement issus du modèle dénotationnel impliqué afin de rendre celui-ci pleinement adéquat pour notre nouvelle syntaxe. Intuitivement, ces opérateurs vont internaliser un processus d'inférence de type possiblement divergent qui tente de typer l'arbre de Böhm d'un terme.``
We extend the definition of Christoffel words to directed subgraphs of the hypercubic lattice in arbitrary dimension that we call Christoffel graphs. Christoffel graphs when d=2 correspond to well-known Christoffel words. Due to periodicity, the d-dimensional Christoffel graph can be embedded in a (d−1)-torus (a parallelogram when d=3). We show that Christoffel graphs have similar properties to those of Christoffel words: symmetry of their central part and conjugation with their reversal. Our main result extends Pirillo's theorem (characterization of Christoffel words which asserts that a word amb is a Christoffel word if and only if it is conjugate to bma) in arbitrary dimension. In the generalization, the map amb↦bma is seen as a flip operation on graphs embedded in ℤd and the conjugation is a translation. We show that a fully periodic subgraph of the hypercubic lattice is a translate of its flip if and only if it is a Christoffel graph.
Nous présentons une construction algébrique qui a pour loi de composition l’unification de termes du premier ordre, et comment y représenter le calcul. La correspondance preuve-programme fournit alors une façon innovante de représenter les entiers binaires comme des fonctions dialoguant avec les programmes. Les machines abstraites que l’on peut y encoder (les observations) peuvent naturellement être vues comme des machines à pointeurs, qui parcourent l’entrée sans la modifier. On montre alors que ces observations sont suffisamment expressives pour caractériser l’espace logarithmique, et que décider de l’acceptation d’un mot par une observation est réductible au problème d’acyclicité d’un graphe, un problème également en espace logarithmique. (En collaboration avec Marc Bagnol [http://iml.univ-mrs.fr/ bagnol/], Paolo Pistone et Thomas Seiller [http://www.ihes.fr/ seiller/])
La ``range property'' a été conjecturée par Böhm en 1968 et a résisté 16 ans avant d'être prouvée pour quelques théories du $lambda$-calcul. En 2007, A. Polonsky a montré que la conjecture est fausse pour la théorie $H$. Je présenterai dans cet exposé des conditions nécessaires pour que cette propriété soit vraie pour la théorie $H$. Je donnerai ensuite quelques pistes pour des extensions de ces résultats à d'autres systèmes.
We propose an abstract framework for modeling state-based systems with internal behavior as e.g. given by silent or $epsilon$-transitions. Our approach employs monads with a parametrized fixpoint operator $dagger$ to give a semantics to those systems and implement a sound procedure of abstraction of the internal transitions, whose labels are seen as the unit of a free monoid. More broadly, our approach extends the standard coalgebraic framework for state-based systems by taking into account the algebraic structure of the labels of their transitions. This allows to consider a wide range of other examples, including Mazurkiewicz traces for concurrent systems. This is joint work with Filippo Bonchi, Stefan Milius and Alexandra Silva.
We study temporal properties over infinite binary red-blue trees in the setting of constructive type theory. We consider several familiar path-based properties, typical to linear-time and branching-time temporal logics like LTL and CTL*, and the corresponding tree-based properties, in the spirit of the modal mu-calculus. We conduct a systematic study of the relationships of the path-based and tree-based versions of eventually always blueness '' and mixed inductive-coinductivealmost always blueness'' and arrive at a diagram relating these properties to each other in terms of implications that hold either unconditionally or under specific assumptions (Weak Continuity for Numbers, the Fan Theorem, Lesser Principle of Omniscience, Bar Induction).
Joint work with Marc Bezem and Tarmo Uustalu.
Généralisant les systèmes dynamiques symboliques substitutifs, un système est dit $S$-adique si son langage est obtenue par itérations successives de substitutions appartenant à l'ensemble fini $S$. La suite de substitutions itérées en est alors une représentation $S$-adique et fournit des informations sur le système (minimalité, nombre de mesures ergodiques, fréquence des lettres,...). Dans cet exposé, je développerai une méthode basée sur les graphes de Rauzy et les mots de retour permettant de construire une représentation $S$-adique ``canonique''. Dans le cas des sous-shifts minimaux dont la différence première de complexité en facteur est majorée par 2 (contenant notamment les sous-shifts sturmiens, d'Arnoux-Rauzy ainsi que les codages de rotations et d'échange de 3 intervales), cette méthode fournit une caractérisation $S$-adique, où $S$ contient 5 substitutions. En particulier, cette caractérisation répond à la conjecture $S$-adique pour ce cas particulier.
Quelle structure algébrique généralise à la fois les ensembles ordonnés et les espaces métriques? La structure de catégorie enrichie dans une catégorie monoïdale $mathcal{V}$, comme l'a montré Lawvere [1973]. En effet, si on pose $(mathcal{V},otimes,I)=([0,infty]^{sf op},+,0)$, alors la théorie des $mathcal{V}$-catégories est celle des espaces métriques; et si on pose $(mathcal{V},otimes,I)=({0,1},wedge,1)$, alors la théorie des $mathcal{V}$-catégories est celle des ensembles ordonnés. Mais comment faire si on veut parler des {em ensembles ordonnés d'éléments locaux}, autrement dit, des ensembles ordonnés dont les éléments ne sont pas définis partout''? Ou, dans le même esprit, si on veut parler des {em espaces métriques partiels}, c'est à dire, des espaces métriquesdans lesquels la distance d'un point à lui-même n'est pas nécessairement zéro''? Je vais expliquer que, dans ces cas aussi, la structure recherchée est celle de catégorie enrichie---mais, cette fois, enrichie dans une bicatégorie $mathcal{W}$. De plus, pour les éléments locaux comme pour les métriques partiels, la bicatégorie $mathcal{W}$ en question est obtenue par une construction universelle sur une catégorie monoïdale $mathcal{V}$: c'est la {em la construction des diagonaux}. Donc, pour $(mathcal{V},otimes,I)=([0,infty]^{sf op},+,0)$, les $mathcal{V}$-catégories sont les espaces métriques; et pour $mathcal{W}=mathcal{D}(mathcal{V})$ (la bicatégorie des diagonaux dans $mathcal{V}$), les $mathcal{W}$-catégories sont les espaces métriques partiels. Mais bien sûr tout espace metrique ordinaire est un espace métrique partiel; et il est aussi vrai que tout espace métrique partiel détermine (au moins) un espace métrique ordinaire. Cette relation est entièrement expliquée par des {em changements de base}, c'est à dire des foncteurs particuliers, qui existent entre $mathcal{V}$ et $mathcal{W}$. Comme autre exemple de changement de base, je vais parler de l'ordre sous-jacent d'un espace métrique, et de l'espace métrique libre sur un ordre. Je vais par ailleurs indiquer comment, par le biais des changements de base, on peut formuler des questions pertinentes à propos de ces structures. Dans mon exposé, je vais éviter toute technicité (le seul prérequis étant la notion d'ensemble ordonné), car je veux surtout insister sur l'usage de bicatégories comme base d'enrichissement pour traiter spécifiquement les phénomènes décrits ci-dessus.
In this talk, we present an interactive semantics for derivations (i.e., formal proofs) in an infinitary extension of classical logic. The formulas of our language are possibly infinitary (i.e., not necessarily well-founded, and not necessarily finitely branching) trees labeled by logical connectives and propositional variables. We show that in our setting every recursive formula equation has a unique solution. As for derivations, we use an infinitary variant of the standard Tait-calculus to derive sequents. In our sequent calculus, derivations are defined to be possibly infinitary trees labeled by sequents and rules. The interactive semantics we introduce is somehow similar to Girard's ludics, inasmuch as it builds upon a suitable procedure of cut-elimination. We show a completeness theorem for derivations, that we call interactive completeness theorem.
Dans cet exposé je présenterai la notion de catégorie mu-bicomplète, et instancierai cette notion avec la catégorie des ensembles, via la notion de jeu de parité. J'expliquerai ensuite l'importance de chercher un syntaxe adéquate pour dénoter toutes les flèches d'une catégorie mu-bicomplète libre. Je proposerai donc la notion de preuve circulaire (avec la condition sur les cycles qu'elle doit satisfaire) comme une telle syntaxe ; je justifierai cette proposition par les résultats de correction et complétude (fortes, catégoriels) du calcul, par rapport à la sémantique catégorielle envisagée. Nous montrerons qu'un théorème d’élimination des coupures vaut, car on peut éliminer les coupures d'un preuve circulaire finie avec cut, pour obtenir un arbre de preuve infini sans cut. Nous montrerons comment ce processus d’élimination des coupures amène à caractériser toutes les fonctions d'ensembles qui sont l'image d'une flèche d'une catégorie mu-bicomplete libre.
Nous montrerons dans ce séminaire comment des outils mathématiques de géométrie discrète et de théorie des pavages peuvent servir à résoudre des problèmes de bio-mathématiques et en particulier de comprendre les interactions protéines-protéines. On va ainsi montrer comment ces interactions mènent à des polymères ``normaux'', à des virus ou à des fibres...
Nous introduirons dans cet exposé quelques concepts de combinatoires analytiques (méthode symbolique, Théorèmes de transfert, Transformations de Mellin) et tenterons de montrer en quoi cette approche peut être utile pour certains problèmes de géométrie discrète. Plus particulièrement, nous nous intéresserons à l'étude asymptotique du nombre de convexes discrétisés de périmètre n. Cet exposé repose sur l'article ``Asymptotic Analysis and Random Sampling of Digitally Convex Polyominoes'', travail en commun avec P. Duchon, A. Jacquot et L. Mutafchief.
We say that a subshift, i.e. a closed shift invariant subspace of the space of sequences on a finite alphabet, has bounded powers. If there is an upper bound on the powers n with which words occur in the subshift. This is a strong combinatorial property which, for Sturmian susbshifts, coincides with the fact that the slope has bounded continued fraction expansion. Approximating the subshift space by a family of graphs we obtain a family of metrics which may or may not be Lipschitz equivalent. That latter property turns out to charactise minimal subshifts which have bounded powers.
Les pavages auto-assemblants sont un modèle d'assemblage de structures moléculaires, implémentables avec de l'ADN, et capables de calcul Turing. J'expliquerai dans cet exposé deux bornes inférieures de complexité, dans le cas des systèmes d'assemblage non-coopératif (aussi appelés ``température 1'') : une sur les capacités de simulation intrinsèque du modèle, et l'autre sur la complexité d'assemblage de carrés de taille arbitraire.
Les droites discrètes en 2D sont bien connues et possèdent plusieurs définitions équivalentes (combinatoire, arithmétique, dynamique). Toutefois, en dimension supérieure, ces définitions ne sont pas équivalentes et donnent lieu à des concepts différents : les mots de billards, les codages de rotations, les échange d'intervalles, le modèle standard de la droite discrète d'Éric Andres. Aucune de ces définitions de droites discrètes 3D ne conserve toutes les bonnes propriétés des droites discrètes 2D (suite équilibrée, complexité en facteurs linéaire). L'approche que nous considérons est la construction de droites discrètes par un produit de substitutions appelé suite S-adique selon la terminologie de Vershik et Livshits (1992). La suite de substitutions est déterminée par un algorithme de fractions continues multidimensionnelles donnant une suite d'approximations diophantiennes d'un vecteur de nombres réels. De récents résultats montrent qu'on peut construire des suites équilibrées (Delecroix, Hejda, Steiner, 2013) et de complexité linéaire en facteurs (Berthé, Labbé, 2013) avec cette approche.