En 1933 Lehmer enonce le problème suivant : existe-t-il une constante c > 0 telle que la mesure de Mahler M(α) de tout nombre algébrique α non nul et différent d’une racine de l’unité vérifie M(α) ≥ 1 + c. La Conjecture de Lehmer affirme que oui (C. Smyth, ”Survey”, 2014). Pour la tester de nombreuses familles de nombres algébriques tendant vers 1 ont été considérées. Il s'agit d’un problème limite et de minoration de M (ou de la hauteur pour des courbes elliptiques ou des variétés Abéliennes). Un autre problème limite ouvert est de caractériser le premier dérivé de l'ensemble des nombres de Salem T. Une première conjecture de Boyd dit que la réunion S ∪ T des ensembles des nombres de Pisot et de Salem est fermé. Une deuxième conjecture de Boyd affirme que le premier dérivé de l'ensemble des nombres de Salem est l'ensemble des nombres de Pisot. A chaque nombre algébrique réel β > 1 on peut souvent associer trois fonctions zeta dynamiques : (i) la fonction zeta d’Artin-Mazur de la beta-transformation ζ_β(z), qui provient du système dynamique de numération de Rényi-Parry, la base ́étant β; (ii) pour un polynôme P de petit hauteur s’annulant sur β, la fonction zeta de Lefshetz ζ_{L,β,P}(z), qui provient d’un automorphisme du tore n-dimensionnel, où n = deg P, et (iii) la fonction zeta d’Artin-Mazur ζ{AM,β,P}(z), qui provient de la même action sur le tore n-dimensionnel. Si (β_i) est une suite convergente de nombres algebriques, une question fondamentale est de savoir si les fonctions zeta limites peuvent apporter des solutions ou un éclairage nouveau sur ces questions ; par exemple, caractériser la limite des ensembles de pôles des fonctions ζ_{β_i}(z) lorsque i tend vers l'infini. En effet, le contrôle de la hauteur peut donner lieu à des phénomènes d'équidistribution limite de conjugués sur le cercle unité (Bilu, Petsche, Pritsker). On prendra l'exemple d'une famille F de nombres de Perron, qui tendent vers 1, racines dominantes de trinômes de hauteur 1 non réciproques, et de petite mesure de Mahler. On montrera que les développements asymptotiques (de Poincaré) des pôles des fonctions ζ_{β_i}(z) permettent d'obtenir le développement asymptotique de la mesure de Mahler et de prouver directement que la conjecture de Lehmer est vraie pour la famille F.
(Travail avec Peter Hancock) Brouwer savait déjà que les fonctions continues entre stream (avec la topologie produit habituelle) pouvaient être représentées par des arbres infinis. Peter Hancock a montré comment transformer ce théorème de représentation'' en théorie des types dépendant permettant de manipuler ces fonctions comme un type de données standard. Nous avons récemment pu généraliser ces idées à de nombreux types de données coinductifs en utilisant la notion destructure d'interaction'' (ou container indexé'' oufoncteur polynomial''). J'essaierais d'introduire les notions nécessaire au fur et à mesure : types dépendants, définitions inductives et coinductives, définitions inductive-récursives, etc.
Les réseaux de robots mobiles reçoivent depuis quelques années une attention croissante de la part de la communauté de l'algorithmique distribuée. Si l'utilisation d'essaims de robots coopérant dans l'exécution de diverses tâches est une perspective séduisante, l'analyse de la faisabilité de certaines tâches dans ce cadre émergent est extrêmement ardue, en particulier si certains robots présentent des comportements dits byzantins, c'est-à-dire arbitraires voire hostiles.
Pour obtentir des garanties formelles dans ce contexte, nous proposons un cadre mécanique formel fondé sur l'assistant à la preuve Coq et adapté aux réseaux de robots. Nous nous intéressons en particulier aux résultats d'impossibilité, fondamentaux en algorithmique distribuée en ce sens qu'ils établissent ce qui peut ou ne peut pas être réalisé et permettent de définir des bornes et, par là, l'optimalité de certaines solutions. Utiliser un assistant comme Coq travaillant à l'ordre supérieur nous permet d'exprimer aisément des quantifications sur les algorithmes, ceux-ci étant considérés comme des objets abstraits. Nous illustrons les possibilités offertes par notre développement en présentant les premières preuves formelles (et donc certifications) de certains résultats comme l'impossibilité de la convergence de robots amnésiques lorsqu'un tiers d'entre eux sont byzantins, ou encore l'impossibilité du rassemblement pour un nombre pair de robots évoluant dans R.
Ces travaux s'inscrivent dans la thématique de l'inférence géométrique dont le but est de répondre au problème suivant : étant donné un objet géométrique dont on ne connaît qu'une approximation, peut-on estimer de manière robuste ses propriétés? On se place dans le cas où l'approximation est un nuage de points ou un ensemble digital dans un espace euclidien de dimension finie. On montre un résultat de convergence multigrille d'un estimateur du Voronoi Covariance Measure qui utilise des matrices de covariance de cellules de Voronoi. Ce résultat, comme la plupart des résultats en inférence géométrique, utilisent la stabilité de la fonction distance à un compact. Cependant, la présence d'un seul point aberrant suffit pour que les hypothèses des résultats de stabilité ne soient pas satisfaites. La distance à une mesure est une fonction distance généralisée introduite récemment qui est robuste aux points aberrants. Dans ce travail, on généralise le Voronoi Covariance Measure à des fonctions distances généralisées et on montre que cet estimateur appliqué à la distance à une mesure est robuste aux points aberrants. On en déduit en particulier un estimateur de normale très robuste. On présente également des résultats expérimentaux qui montrent une forte robustesse des estimations de normales, courbures, directions de courbure et arêtes vives. Ces résultats sont comparés favorablement à l'état de l'art.
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.