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.
En théorie des catégories, une fibration représente une forme d'indexation d'une catégorie par une autre. On rappellera comment une telle structure peut être utilisée pour modéliser une logique (représentée par la catégorie indexée) au dessus d'une théorie des types (représentée par la catégorie index). On portera alors notre attention sur les types inductifs et coinductifs et comment capturer leurs schémas d'induction et de coinduction respectif dans les fibrations.
We introduce bisimulation up to congruence'' as a technique for proving language equivalence of non-deterministic finite automata. Exploiting this technique, we devise an optimisation of the classical algorithm by Hopcroft and Karp which, as we show, is exploiting a weakerbisimulation up to equivalence'' technique. The resulting algorithm can be exponentially faster than the recently introduced ``antichain algorithms''.
Les catégories à trace ont été utilisées dans le domaine de la sémantique dénotationnelle (en logique comme en informatique) pour modéliser des situations de rétroaction raisonnables''. La construction G(.) permet, à partir d'une catégorie à trace, d'obtenir une nouvelle catégorie dont la composition peut être vue comme unerétroaction parallèle''. Les machines synchrones'' ont été utilisées pour donner une sémantique des langages de programmation synchrones (Lustre, Esterel...) en termes d'automates. Dans ces sémantiques, la mise en parallèle de deux programmes est modélisée par une construction appeléeproduit synchrone''. On verra que les machines synchrones peuvent être vues comme une catégorie à trace S et que le produit synchrone de deux machines correspond à leur composition dans G(S).
Le système de types input/output induit du sous-typage dans le pi-calcul. De manière un peu surprenante, le sous-typage se prête mal à une adaptation à des calculs proches (le calcul des fusions, le pi-calcul à mobilité interne). On construit une modification du calcul des fusions dans laquelle le mécanisme du sous-typage s'applique, ce qui permet d'en éclairer certains aspects.
Seely’s paper Locally cartesian closed categories and type theory contains a well-known result in categorical type theory: that the category of locally cartesian closed categories is equivalent to the category of Martin-Löf type theories with Π, Σ, and extensional identity types. However, Seely’s proof relies on the problematic assumption that substitution in types can be interpreted by pullbacks. Here we prove a corrected version of Seely’s theorem: that the Bénabou-Hofmann interpretation of Martin-Löf type theory in locally cartesian closed categories yields a biequivalence of 2-categories. To facilitate the technical development we employ categories with families as a substitute for syntactic Martin-Löf type theories. As a second result we prove that if we remove Π-types the resulting categories with families are biequivalent to left exact categories.
It is well known that the real numbers arise from the metric completion of the rational numbers, with the metric induced by the usual absolute value. We seek a computational version of this phenomenon, with the idea that the role of the rationals should be played by the affine lambda-calculus, whose dynamics is finitary; the full lambda-calculus should then appear as a suitable metric completion of the affine lambda-calculus. We propose a technical realization of this idea: we introduce an affine lambda-calculus, based on a fragment of intuitionistic multiplicative linear logic; the calculus is endowed with a notion of distance making the set of terms an incomplete metric space; we show that the completion of this space yields an infinitary affine lambda-calculus, whose quotient under a suitable partial equivalence relation is exactly the full (non-affine) lambda-calculus. We also show how this construction brings interesting insights on some standard rewriting properties of the lambda-calculus (finite developments, confluence, standardization, head normalization and solvability).
Introduced as symmetric types for pi-processes, session types have been developed into a large theory for verification of message-passing programs. Their main principle is as follows: a global type describing the expected interactions inside a network is projected into several local types: if every agent abides to its local type, the whole network abides to the global specification. I will present the Multiparty Session Types theory through recent developments: full-abstract embedding into the pi-calculus, nested protocols, automatic monitor generation, session types with multisession assertions.
On regardera les programmes que l'on peut extraire des preuves du théorème de Ramsey infini. On ira jusqu'à extraire un programme SML pour le ``happy ending problem'', qui trouve P sommets d'un polyogone convexe à partir de N points du plan si N est assez grand (http://fr.wikipedia.org/wiki/Happy_Ending_problem). On regardera aussi le programme que donne la preuve de Ramsey par l'ultrafiltre par rapport à la preuve classique. Enfin, on se posera des questions sur les liens possibles entre la compléxité des programmes liés à Ramsey et des bornes sur la fonction de Ramsey.
We study distributed algorithms on massive graphs where links represent a particular relationship between nodes (for instance, nodes may represent phone numbers and links may indicate telephone calls). Since such graphs are massive they need to be processed in a distributed and streaming way. When computing graph-theoretic properties, nodes become natural units for distributed compu- tation. Links do not necessarily represent communication channels between the computing units and therefore do not restrict the communication flow. Our goal is to model and analyze the computational power of such distributed systems where one computing unit is assigned to each node.
We discuss a complete axiomatization of Monadic Second-Order Logic (MSO) on infinite words (or streams). By using model-theoretic methods, we give an alternative proof of D. Siefkes’ result that a fragment with full comprehension and induction of second-order Peano’s arithmetic is complete w.r.t. the validity of MSO-formulas on streams. We rely on Feferman-Vaught Theorems and the Ehrenfeucht-Fraisse method for Henkin models of MSO. Our main technical contribution is an infinitary Feferman-Vaught Fusion of such models. We show it using Ramseyan factorizations similar to those for standard infinite words.
Nous considérons la famille des problèmes reliés au comptage des mots sur un alphabet fini engendrés par intervalles, y compris les mots sturmiens, des mots de rotation et les mots engendrés par l'échange de trois intervalles. Nous discutons des méthodes géométriques et combinatoires de comptage.
Hedlund et Morse ont introduit et développé la dynamique symbolique vers 1938. La combinatoire des mots leur doit beaucoup, car ils ont mis en évidence de nombreux concepts important mais semblent avoir ignoré les trajectoires exponentielles de Rufus Oldenburger...
I will talk about two novel models of Petri nets with boundaries and characterise them using a calculus of combinators.
The algebraic lambda calculus and the linear algebraic lambda calculus are two extensions of the classical lambda calculus with linear combinations of terms. They arise independently in distinct contexts: the former is a fragment of the differential lambda calculus, the latter is a candidate lambda calculus for quantum computation. Their operational semantics differ in the treatment of applications and algebraic rules. We show how these two languages can simulate each other using an algebraic extension of the well-known call-by-value and call-by-name CPS translations. We prove that the simulations are sound and complete. Joint work with Ali Assaf, Alejandro Díaz-Caro, Christine Tasson and Benoît Valiron.