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.
Etant donné un vecteur non nul n de R^d et deux réels mu et w, le plan discret de vecteur normal n, de décalage mu et d'épaisseur omega, noté P(n,mu,omega), tel que défini par J.-P. réveillès, est l'ensemble des points de Z^d satisfaisant la double inégalité 0 <= <n,x> + mu < omega où <.,.> désigne le produit scalaire usuel dans R^d. Pour k dans {0,...d-1}, deux points distincts x et y de Z^d sont des k-voisins s'ils ont au moins k coordonnées communes et leurs coordonnées diffèrent d'au plus 1. Lorsque x et y sont représentés par des cubes unités centrés sur les coordonnées entières, ces cubes partagent alors une facette de dimension au moins k. Une partie S de Z^d est k-connexe, si pour toute paire de points x et y dans S, il existe dans S un chemin x=x_1,...,x_q=y formé de k-voisins. Le problème qui nous intéresse est, étant donnés un vecteur normal n et un décalage mu, de déterminer l'ensemble des valeurs de l'épaisseur omega pour lesquelles le plan P(n,mu,omega) est k-connexe. Nous nous intéressons plus particulièrement au cas où k=d-1, c'est à dire à la connexité par face. Cet ensemble est alors un intervalle infini à droite dont la borne inférieure est appelée épaisseur de connexité de n avec décalage mu et notée Omega(n,mu). Cette épaisseur peut être calculée grâce à un algorithme simple connu sous le nom d'algorithme totalement soustractif (Fully Subtractive Algorithm). Par définition, le plan P(n,mu,omega) est non connexe si omega < Omega(n,mu) et connexe si omega > Omega(n,mu). La question qui se pose alors est celle de la connexité de P(n,mu,Omega(n,mu)). Ce plan est presque toujours non connexe mais peut être connexe si la suite de vecteurs calculée par l'algorithme a une certaine propriété déterminée par Kraaikamp et Meester et qui n'est satisfaite que pour les vecteurs appartenant à un certain fractal de mesure nulle. La question de la connexité de P(n,mu,Omega(n,mu)) lorsque n appartient à ce fractal a été résolue dans un cas particulier en collaboration avec V. Berthé, D. Jamet et X. Provençal. Nous résolvons ici le cas général. Le déroulement de l'algorithme peut être décrit par un mot infini Delta sur l'alphabet {1,...,d}. A partir de ce mot, nous construisons une suite de sous-ensembles de Z^d qui, entre autres propriétés, sont connexes. Nous montrons que la limite de cette suite, appelée clôture palindromique géométrique itérée de Delta, est en fait P(n,0,Omega(n,0)) prouvant ainsi que ce plan est connexe. Nous exhibons également certaines valeurs particulières du décalage mu pour lesquelles P(n,mu,Omega(n,mu)) est non connexe. Le cas général lorsque mu est quelconque reste une question ouverte. (E. Domenjoud & L. Vuillon)
My research focuses on distributed programming models, more precisely using objects and components. In this area, I provided tools easing the programming of large-scale distributed applications and verifying their correct behaviour. To facilitate the programming of distributed applications, I contributed to the design and the development of languages with a high level of abstraction. My work aims to provide a strong model of programming languages, libraries, and runtime environments to the developer, and to guarantee the safe behaviour of distributed applications. In the OASIS team, we contributed to the definition of a distributed component model - the GCM (Grid Component Model) -, to its formalisation, and to its use for programming adaptive or autonomous components. After a short introduction to the principles of distributed computing and to the use of formal methods in this area, this talk will provide an overview of those aspects focusing on the programming models. I will conclude with a focus on a couple of my current research topics that include distributed algorithms for peer-to-peer systems, and programming on multicore and distributed architecture.
Dependant Linear PCF (dlPCF) was introduced by Dal Lago and Gaboardi as a type system characterising the complexity of PCF programs. It is parametrised by a an equational program, which is used to express some complexity annotations for types. This enables a modular complexity analysis, and the main strength of the system is to be relatively complete: any terminating PCF program is typable in dlPCF (and its complexity is thus determined) assuming that the equational program is expressive enough. We have designed a type inference algorithm for this system: given a PCF program, it computes its type in dlPCF (and thus a complexity bound for the program) together with a set of proof obligations that ensures the correctness of the type, following the same scenario as the computation of weakest preconditions in Hoare logic. Checking formally the proof obligations generated by the type checker then amounts to a formal proof that the complexity bound is correct. In this talk I will explain how the type system dlPCF can be turned into a tool for formal certification of the complexity of functional programs.
À venir
A series of recent papers introduces a coalgebraic semantics for logic programming, where the behavior of a goal is represented by a parallel model of computation called coinductive tree. This semantics fails to be compositional, in the sense that the coalgebra formalizing such behavior does not commute with the substitutions that may apply to a goal. We suggest that this is an instance of a more general phenomenon, occurring in the setting of interactive systems (in particular, nominal process calculi), when one tries to model their semantics with coalgebrae on presheaves. In those cases, compositionality can be obtained through saturation. We apply the same approach to logic programming: the resulting semantics is compositional and enjoys an elegant formulation in terms of coalgebrae on presheaves and their right Kan extensions.
Dans un travail antérieur avec Damien Pous, on définit une sémantique pour CCS, qui peut être vue à la fois comme une sémantique de jeux non-déterministe et comme une sémantique de préfaisceaux innocents. Les résultats d'adéquation obtenus pour cette sémantique reposent sur le fait que les parties du jeu forment une catégorie fibrée, au sens de Grothendieck, au-dessus des positions. On s'attaque ici à poursuivre notre approche dans le cadre du pi-calcul. Or, s'il est facile de concevoir un jeu pour pi dans l'esprit de celui pour CCS, il est beaucoup moins évident que les parties sont fibrées au-dessus des positions. On montrera qu'elles le sont, en utilisant un outil catégorique bien connu: les systèmes de factorisation.
Il est en général indécidable de tester si une définition récursive est bien fondée, mais il existe de nombreux tests pour décider des conditions suffisantes pour la bonne fondation. Le principe du ``size-change'' de A. ben Amram, N.D. Jones et C.S. Lee est particulièrement simple (il s'agit simplement d'examiner certaines boucles dans le graphe d'appels des fonctions récursives), élégant (il repose sur le théorème de Ramsey) et puissant. C'est ce principe qui a été étendu et implanté dans le language PML. Les extensions vont dans deux directions : - autoriser la taille des arguments à augmenter localement, - utiliser la structure du langage (constructeurs / filtrage). Un point important est que ces extensions ne rendent pas le test plus compliqué à implanter.
In a recent paper (Girard 2011b), Girard uses the geometry of interaction in the hyperfinite factor (Girard 2011a) in an innovative way to characterize complexity classes. The purpose of this paper is two-fold: to give a detailed explanation of both the choices and the motivations of Girard’s definitions, and – since Girard’s paper skips over some non-trivial details and only sketches one half of the proof – to provide a complete proof that co-NL can be characterized by an action of the group of finite permutations. We introduce as a technical tool the non-deterministic pointer machine, a concrete model that computes the algorithms represented in this setting.
À venir
Cellular Automata can be characterized as the translation-invariant continuous functions, where continuity is with respect to a certain distance over the set of configurations. This distance, and its properties, easily extend from grids to Cayley graphs. As a consequence, Cellular Automata also extend from grids to Cayley graphs. Cayley graphs have a number of useful features: the ability to graphically represent finitely generated group elements and their equality; to name all vertices relative to a point; the fact that they have a well-defined notion of translation, and that they can be endowed with such a compact metric. But they are very regular. We propose a notion of graph associated to a language, which conserves or generalizes these features. These associated graphs can be arbitrary, although of a bounded degree. We extend Cellular Automata to these Generalized Cayley graphs, so that they define a local dynamics over time-varying graphs.
Dans le cadre de la réalisabilité classique telle qu'elle est introduite par Krivine, les réalisateurs |A| d'une formule A peuvent être vus comme des défenseurs de la formule face à une pile choisie parmi l'ensemble ||A|| de ses adversaires. Dans la continuité de cette interprétation, Krivine explique comment une formule arithmétique (∃xn, ∀yn, ... ∃x1, ∀y1 f(x, y)=0 ) peut être vue comme un jeu entre deux joueurs (∃ et ∀), un réalisateur étant alors une stratégie gagnante pour le jeu correspondant. Dans sa thèse, Guillermo montre que tout réalisateur universel est bien un stratégie gagnante. On montre ici que la réciproque est vraie : une stratégie gagnante est aussi un réalisateur universel. On s'intéresse ensuite à la relativisation des formules à différents types de données (et l'on montre qu'il existe dans le plus dur des jeux une stratégie gagnante valable pour toute formule vraie) et au lien entre formules d'atome f(x,y)=0 et f(x,y)<>0.
Les automates cellulaires probabilistes ou non-déterministes sont souvent étudiés à travers des exemples ou aspects particuliers (alpha-asynchronisme, automates bruités, transitions locales probabilistes, etc). Nous proposons au contraire de les formaliser dans un modèle général qui se prête à une étude systématique. Partant de là nous abordons deux problématiques importantes largement développées dans la théorie des automates cellulaires déterministes : les simulations et l'universalité intrinsèque d'une part, la décidabilité des propriétés globales en fonction des descriptions locales d'autre part.