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.
La suite de Kolakoski, introduite - comme son nom ne le dit pas - par R. Oldenburger en 1939, est une suite auto-descriptive simple. Il s'agit de la suite 'w' sur l'alphabet {1,2} qui est égale à son propre ``run-length-encoding'' RLE(w). La ième lettre de RLE(w) est la taille du ième bloc de 'w', un bloc étant une répétition d'une même lettre. Cette suite commence donc par 12211212212211... Malgré sa définition simple, beaucoup de conjectures concernant cette suite sont ouvertes depuis une trentaine d'années. Il y a notamment la conjecture que la densité de 1 dans 'w' est 0.5. Concernant cette conjecture, la meilleure borne supérieure de 0.50084 a été donnée par V. Chvátal en 1993. Dans cet exposé, on verra cette suite comme un point fixe d'un transducteur. En prenant les puissances de ce transducteur, on obtiendra une nouvelle borne sur la densité. Cela nous permet également d'avoir un algorithme qui a permis d'explorer les 10^19 premières lettres de la suite. On finira par quelques nouvelles conjectures et questions sur cette suite.
This paper proposes a new interpretation of the logical contents of programs in the context of concurrent interaction, wherein proofs correspond to valid executions of a processes. A type system based on linear logic is used, in which a given process has many different types, each typing corresponding to a particular way of interacting with its environment and cut elimination corresponds to executing the process in a given interaction scenario. A completeness result is established, stating that every lock-avoiding execution of a process in some environment corresponds to a particular typing. Besides traces, types contain precise information about the flow of control between a process and its environment, and proofs are interpreted as composable schedulings of processes. In this interpretation, logic appears as a way of making explicit the flow of causality between interacting processes. Joint work with Virgile Mogbil.
Le parsing et le pretty-printing sont des opérations omniprésentes en informatique : communications entre machines ou entre processus, interfaces homme-machine, etc. Il semble évident que les parser et pretty-printer sont liés par une relation de cohérence, mais elle n'a jamais été mise en évidence. En conséquence, pour faire une preuve formelle utilisant un parser et un pretty-printer (par exemple d'un protocole de communication), il faut deviner une relation vérifiée par cette paire avant la prouver, ce qui rend la preuve difficile. Dans cet exposé, on donnera une définition de la cohérence entre un parser et un pretty-printer et on esseaira de la motiver.
Ce travail est une contribution à la sémantique de jeux des langages de programmation. Il présente plusieurs méthodes nouvelles pour construire une sémantique de jeux pour un lambda-calcul de continuations. Si les sémantiques de jeux ont été développées à grande échelle pour fournir des modèles de langages fonctionnels avec références, en appel par nom et par valeur, ou pour différents fragments de la logique linéaire, certains de ses aspects demeurent cependant très subtils. Cette thèse s'intéresse spécifiquement à la notion d'innocence et à la combinatoire mise en jeu dans la composition des stratégies innocentes, en donnant pour chacune une interprétation via des constructions catégoriques standards. Nous reformulons la notion d'innocence en terme de préfaisceaux booléens sur une catégorie de vues. Pour cela, nous enrichissons la notion de parties dans notre sémantique de jeux en ajoutant des morphismes entre parties qui vont au-delà du simple ordre préfixe habituel. À partir d'une stratégie, donnée par les vues qu'elle accepte, on calcule son comportement sur toutes les parties en prenant une extension de Kan à droite. La composition des stratégies innocentes s'appuie sur les notions catégoriques habituelles de systèmes de factorisation et de foncteurs polynomiaux. Notre sémantique permet de modéliser l'interaction entre deux stratégies comme une seule stratégie dont il faut parvenir à cacher les coups internes, grâce à une technique d'élimination des coupures : cette étape est accomplie avec une version affaiblie des systèmes de factorisation. La composition elle-même entre stratégies repose pour sa part sur l'utilisation de la théorie des foncteurs polynomiaux. Les propriétés essentielles, telles que l'associativité ou la correction de la sémantique, proviennent d'une méthode de preuve presque systématique donnée par cette théorie.
We give here an effective proof of Hilbert's nullstellensatz and Krivine-Stengle's positivestellensatz using the cut elimination theorem for sequent calculus. The proof is very similar to the current techniques in constructive algebraic geometry by Henri Lombardi, but seems more modular. In the case of the positive stellensatz, we think we prove a more general result than the original one, thanks to a new notion of justification of positiveness: PBDD (polynomial binary decision digram). It allows both to recover Krivine-Stengle's justification, but also another one which seems to require lower degree. We apply the same techniques to the nullstellensatz for differentially closed field and show that the proof is almost unchanged. Remark: here we do not provide bound, but an effective algorithm (implemented in OCaml) to build the wanted algebraic equality. Nevertheless, we discuss how bound could probably be obtained. We also do not deal effectively with the axiom of algebraic/real closure. Those are eliminated using standard model theory.
A benefit of abstract computability – which is the main subject matter of this talk – is that it allows the explicit unification of complexity and computability. Understanding the broader geography of these subjects is important for a number of reasons: it brings new perspectives to an old subject and it allows new tools to be brought to bear on old problems.
Abstract computability defines timed sets''. Significantly, this mimics precisely what complexity theorists actually do. The abstract approach, however, has the advantage of removing conceptual clutter and clarifying the structure of what is happening. <br><br> Abstract computability is based round the notion of a Turing category: the talk will introduce this and the necessary related structures. <br><br> References:<br> Robin Cockett, Joaquin Diaz-Boïls, Jonathan Gallagher, Pavel HrubesTimed Sets, Functional Complexity, and Computability''
Robin Cockett, Pieter Hofstra ``Introduction to Turing Categories''
A notion of test for intuitionistic type theory has been recently introduced by Peter Dybjer. It is meant to be the foundation for automatic testing tools that could be implemented in proof assistants such as Coq or Agda. Such tools would provide a way to test, at any time during the construction of a proof, if the current goal is typable in the context. The failure of such a test would mean that the goal is impossible to prove, and its success would corroborate the partial result. We investigate the possibility of extending the testing procedure to classical systems, and propose an interpretation of the testing procedure in term of Krivine's classical realizability.
Les transformations rigides (obtenues par composition de rotations et translations), lors qu’elles sont appliquées sur les imagesnumériques, sont généralement appliquées dans leur espace continu associé, nécessitant ensuite le recours à un procédé de digitalisation afin d’obtenir un résultat sur Z². Alternativement, nous proposons d'étudier ces transformations rigides dans un cadre totalement discret. En particulier, cette étude consiste à modéliser par une structure combinatoire (nommé, DRT graph) tout l'espace de paramètres de ces transformations sur les sous-ensembles de Z² de taille N × N. Ce graphe a une complexité spatiale de O (N^9). Nous décrivons cette structure combinatoire, et proposons également un algorithme permettant de la construire en temps linéaire par rapport à sa complexité spatiale. Le DRT graph peut être utilisé dans des applications de traitement d'images numériques, par exemple lors de procédures de recalage. Nous proposons ainsi des conditions pour lesquelles les images discrètes 2D préservent leurs propriétés topologiques pour toute transformation rigide. Nous en dérivons un procédé algorithmique permettant de vérifier l'invariance topologique des images par transformation rigide dans Z², où cette préservation n'est plus garantie contrairement à R². Cette étude est basée d'une part sur la notion de DRT graph, et d'autre part la notion de point simple. L'utilisation conjointe de ces deux notions permet notamment d'aboutir à une complexité en temps linéaire.