Ce travail présente un cadre unificateur pour les systèmes de types pour les algèbres de processus. Le cœur du système fournit une correspondance précise entre des processus essentiellement fonctionnels et des démonstrations de logique linéaire; des fragments de ce système correspondent à des connections précédemment connues entre démonstrations et processus. On montre que l'ajout d'axiomes logiques peut étendre la classe des processus typables en échange de la perte de propriétés calculatoires comme l'absence de blocage ou la terminaison, ce qui permet de voir différents systèmes connus (types i/o, linéarité, contrôle) comme des instances d'un modèle général. Cette approche suggère des méthodes unifiées pour l'extension de systèmes de types avec de nouvelles propriétés tout en restant dans un cadre bien structuré, ce qui constitue un pas vers l'étude de la sémantique dénotationnelle des processus par des méthodes de théorie de la démonstration.
Dans cet exposé, nous étudierons différentes modélisations pour le mélange d'objets alignés (des livres, des cartes, des fichiers, etc.). En particulier, l'action qui correspond à piger un élément au hasard et à le remettre au début de la liste s'avère être un point de départ intéressant pour l'étude des marches aléatoires sur le groupe symétrique. Nous verrons que l'utilisation de techniques algébriques permet l'analyse de mélanges élaborés.
Cette présentation montrera un lien théorique entre les segments de droite discrète (DSS) et la théorie probabiliste des chemins possibles. Un DSS entre deux points est généralement défini comme la meilleure approximation discrète de la droite continue sous-jacente entre les deux points. Dans cet article, nous introduisons une autre définition qui fait écho à des approches dites de tous les chemins possibles de la physique des particules. Le cosmologiste George Ellis a récemment fait remarquer, Une particule prend tous les chemins qu'elle peut, et ce que nous voyons est la moyenne pondérée de toutes ces possibilités.'' Dans une veine similaire, nous définissons un segment de droite discrète entre deux points comme l'ensemble de pixels le plus rapproché de la moyenne pondérée de tous les chemins discrets possibles de longueur minimale entre les deux points. Cette définition est uniquement destinée à démontrer une relation théorique entre la théorie probabiliste des chemins discrets possibles et les DSSs. Elle n’a pas vocation à remplacer l’algorithme standard de Bresenham (1963) comme moyen pratique pour tracer les segments de droite dans le plan, mais de le justifier par une autre approche. Nous présentons également brièvement l’extension de cette définition dans l’espace à 3 dimensions. Nous présenterons également un nouvel algorithme récursif pour tracer un type de DSS présentant une meilleure autosimilarité que la DSS standard et qui est plus rapide que l'algorithme classique de Bresenham. Pour finir, nous implémenterons l’algorithme de tous les chemins possibles au moyen des automates cellulaires que nous appelons «Mants» (M-fourmis équipées de mémoires mais non réalistes). Il s’avère que le chemin qui est localement le plus probable entre lamanthill'' et une source d'alimentation pour un individu de la colonie n’est, en général, pas identique à la trajectoire optimale pour la colonie dans son ensemble.
In denotational semantics, we have a few examples of notions which are easy to describe graphically (and generally informally), but whose algebraic axiomatisation is tedious, to say the least. Such examples include (in order of appearance) Lambek's polycategories, Girard's proof nets, and Lafont's interaction nets. The importance of algebraic axiomatisation of course resides in the induced notion of denotational model. In this work, we propose a generalisation of Joyal's analytic functors to certain presheaf categories, which we then use to directly derive algebraic axiomatisations from elementary graphical information. For concreteness, we instantiate our results on polycategories. The idea is that the pictures generally used to describe the standard operations on polycategories may be understood as a straightforward collection of finite presheaves on a certain category. Our notion of analytic functor then allows us to interpret this collection as an endofunctor on presheaves, which then freely generates a certain monad, whose algebras are precisely polycategories.
In this talk we shall recall the notion of hyperfields, i.e. fields with multivalued addition, provide a collection of examples of hyperfields, and show how they can be used to characterize Witt equivalence of fields. We shall also investigate the Witt equivalence of certain types of fields in some more detail.
Partie I (Rodolphe Lepigre) : Le développement de Patoline (un nouveau système de composition de documents) nécessite un parseur extensible d'OCaml sans contrainte, notamment sur l'analyse lexicale. Nous présentons ici un environnement de développement léger pour l'analyse syntaxique, conçu en deux mois pendant l'été 2014 pour répondre à ce besoin. Le système propose une syntaxe intuitive de type BNF, sans récursion à gauche. Les parseurs sont traduits vers des expressions OCaml utilisant DeCaP, notre bibliothèque de combinateurs monadiques, et sont donc des expressions de première classe. Pour optimiser les combinateurs, nous utilisons des continuations et une méthode de prédiction des premiers caractères acceptés par une grammaire. Sur la grammaire d'OCaml, on obtient en moyenne une analyse cinq fois plus lente qu'avec le parseur d'origine et deux fois plus rapide qu'avec Camlp4. De plus, on dispose de combinateurs inspirés de la notion de continuation délimitée pour optimiser les grammaires. Notons que nous gérons aussi les grammaires ambigües. Partie II (Christophe Raffalli) : Parser combinators are popular among functional programmers because they can be used to define languages parameterised by other languages and benefit from the strong type systems of the host language. Parser combinators have the reputation of being slow... However, with a few improvement, they become no more than five to ten times slower than stack automaton. It is easy to translate a BNF-like syntax into calls to combinators while keeping there advantages. However one main drawback remains: left recursion is forbidden. Although left recursion can easily be eliminated from a context free grammar, the presence of parametrised grammars requires more: a fixpoint combinator compatible with left recursion.
The concept of pattern within a combinatorial structure is an essential notion in combinatorics, whose study has had many developments in various branches of discrete mathematics. Among them, the research on permutation patterns and pattern-avoiding permutations has become very active. Nowadays, these researches have being developed in several other directions, one of them concerning the definition and the study of an analogue concept in other combinatorial objects. Some recent studies are presented here, concerning patterns in bidimensional structure, and, specifically, inside polyominoes. After introducing polyomino classes, I present an original way of characterizing them by avoidance constraints (namely, with excluded submatrices) and I discuss how canonical such a description by submatrix-avoidance can be. I also provide some examples of polyomino classes defined by submatrix-avoidance, and I conclude with some hints for future research on the topic.
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é.