Nous chercherons à comprendre la preuve de forte normalisation du lambda calcul simplement typé (et de certaines extensions : système T de Godel, ajout d'un produit, ...) faite par Gandy. Il semble que cette preuve utilise une mesure (entière ?) qui décroit par réduction.
Les représentations graphiques des preuves de la logique linéaire, les proof-nets, permettent de s'abstraire de contraintes inhérentes au calcul des séquents comme la syntaxe et les règles structurelles. La correction (ou prouvabilité) de tels réseaux peut se vérifier à l'aide de critères purement graphiques, comme le critère de Danos-Regnier. Sa simplicité en fait le rend très efficace mais peu compréhensible. Pour donner une preuve de complétude d'un tel critère et tenter de l'expliquer, nous utiliserons une logique différente : MILL. Dans ce système intuitionniste, les règles logiques sont des règles de typage d'un lambda-calcul et les réseaux de preuves ses arbres de syntaxe. Le critère de Danos-Regnier nous permettra de construire un lambda-terme typable à partir du réseau de preuve, assurant ainsi sa validité.
Les pavages auto-assemblants sont un modèle de calcul introduit par Winfree en 2000 afin d'étudier les phénomènes d'auto-assemblage, naturels et artificiels. Je présenterai ce modèle de calcul, d'abord sa définition, puis deux constructions importantes en programmation, le passage paramètre <-> argument (théorème s-n-m) et la récursion, dont nous verrons qu'elles sont assorties de contraintes géométriques pas toujours triviales. Nous verrons ces deux notions appliquées dans des jeux de tuiles simples, l'un qui implémente les homothéties, et l'autre qui assemble le pavage de Robinson (un pavage quasi- périodiques). Nous examinerons aussi les limites du modèle, qui sont de deux sources, l'une géométrique, avec des problèmes de type dead-lock qui rappellent le parallélisme, l'autre rattachée à la complexité Turing. Si le temps le permet, je présenterai des idées de graphes de Cayley qui permettent de s'affranchir de ces limites.
Dans cet exposé, je parlerai des automates cellulaires vus comme des systèmes dynamiques et sous l'angle de propriétés topologiques classiques comme la (non-)sensibilité aux conditions initiales et l'expansivité. Je présenterai la classification de Kurka basée sur ces propriétés dans la topologie de Cantor et son interprétation en terme de circulation de l'information. Cette classification a le défaut de ne pas être invariante par décalage ce qui la rend artificielle pour les automates cellulaires. Le reste de l'exposé sera consacré à une approche récente pour résoudre ce problème : reprendre les différents modes de circulation de l'information de cette classification mais en les étendant à toutes les directions dans l'espace-temps. Cette dernière partie contiendra des résultats de M. Sablik mais aussi une petite collection de questions ouvertes.
J'exposerai mes idées pour une nouvelle sorte de théorème prouveur, basé sur les idées suivantes: - on crée le langage de programmation avec un système de typage statique fort le plus fort possible - on étend ce langage pour en faire une logique (on n'ajoute pas la logique au dessus du langage) Le but de ce séminaire sera de démarrer un éventuel groupe de travail ...
Je presente dans mon exposé le système de type avec intersection de J. Wells qui permet de trouver le type principal d'un lambda-terme uniquement avec l'opération "substitution". Pour cela, il ajoute d'autres variables de type dites "variables d'expansion" et definit la substitution sur ces variables. Je vous présente ensuite une sémantique de réalisabilité pour ce système et un théorème de complétude pour un de ses sous systemes. Ce travail a été fait en collaboration avec F. Kamareddine et J. Wells.
Parmi les modèles de la concurrence et de la mobilité qui ont foisonné après la définition par Milner du Pi-Calcul, on rencontre deux familles très différentes: les modèles de la communication, qui prolongent directement le Pi-Calcul , et des modèles basés sur une notion spatiale de lieux ou de places, dont un exemple bien connu est les Ambients de Cardelli et Gordon. Les Bigraphes, proposés récemment par Milner, sont une tentative d'englober ces deux courants dans une structure unique. Nous proposons une introduction aux Bigraphes, basée sur le tutoriel que Milner a présenté à Paris en septembre dernier.
Le lambda-calcul a deux modèles d'implantation principaux: les machines abstraites, utilisées pour l'appel par nom, par valeur, etc., et les réseaux d'interaction, utilisés pour la réduction optimale, les évaluateurs à la Mackie, etc. La nature très distribuée des réseaux d'interaction ne permet pas, en général, de décrire précisément la stratégie qu'ils implantent et ces deux modèles d'implantation semblent complètement déconnectés. J'établis une connexion entre ces deux mondes en proposant des traductions des stratégies habituelles du lambda-calcul dans les réseaux d'interaction. Ces traductions reposent sur l'idée très simple d'introduire un jeton d'évaluation qui séquentialise certaines réductions. Les stratégies traitées sont l'appel par nom, par valeur, par nécessité et la stratégie "fully lazy".
Nous aborderons diverses méthodes de combinatoire des mots appliquées aux mots de Sturm. En particulier, nous démontrerons des théorèmes de base de la combinatoire des mots comme le lien entre complexité et périodicité, l'équivalence entre plusieurs définitions des mots de Sturm et enfin des résultats sur les graphes des mots (graphes de De Bruijn ou de Rauzy) et la dynamique de ces graphes pour les mots de Sturm.
TBA. Slogan: comment utiliser la machine de Krivine pour linéariser les lambda-termes et rapport avec la propriété d'uniformité du lambda-calcul diff.
On définit une sémantique de réalisabilité inspirée des candidats de réductibilité de J.Y. Girard et adaptée par M. Parigot pour le cas classique. On prouve un lemme de correction pour cette sémantique. On montre ensuite la complétude pour une classe de type notée D^+. Cette classe est formée des types qui ne contiennent pas de quantificateurs à droite d'une flèche (i.e. les quantificateurs ne sont qu' à gauche des flèches). Elle contient donc, en particulier, les types de données. C'est une sous classe des types forall positifs pour lesquels la complétude n'est pas vraie (on fournit un contre exemple).
Nous montrons comment le dédoublement de la règle d'axiome du calcul des séquents de Gentzen permet de mettre en évidence un noyau de calcul qui exprime de manière syntaxique la dualité entre les notions standard d'appel par nom et d'appel par valeur. D'un point de vue théorie de la démonstration, on en conclut que l'appel par valeur est intrinséquement partie prenante de l'interprétation calculatoire du calcul des séquents. D'un point de vue théorie du calcul, on débouche sur un nouveau formalisme basé sur une profonde symétrie entre termes et contextes d'évaluation.
Les codes identifiants ont été introduits pour modéliser un problème de détection de défaillances dans des réseaux multiprocesseurs [1]. C'est un sujet récent de théorie des graphes, qui, dans une de ses variantes, se définit comme suit : étant donné un graphe G=(V,E), un code t-identifiant de G est un sous-ensemble de sommets C de V tel que tout sous- ensemble d'au plus t sommets de G soit identifié de façon unique par la trace de C sur son voisinage fermé. Formellement, C est un code t-identifiant de G si et seulement si on a N[X]cap C neq N[Y]cap C pour toute paire (X, Y) de sous-ensembles distincts d'au plus t sommets de G, où N[X] désigne l'union de X et des voisins de X dans G. Ce sujet peut être vu comme un cas particulier de problème de couverture par tests sur un ensemble structuré. Les problèmes de couverture par tests sont une large classe de problèmes combinatoires, englobant le fameux problème des fausses pièces ou les jeux populaires de devinettes. Lorsqu'un tel code existe, le problème d'optimisation discrète sous-jacent consiste à déterminer un code t-identifiant de cardi- nalité minimum. Au niveau algorithmique, ce problème est NP- difficile [2] . Dans [1], des bornes générales sont données. On peut s'intéresser à l'aspect extrémal de ce problème, en particulier on peut étudier le problème suivant : étant donné un entier n, quels sont les graphes admettant un code t-identifiant de cardinalité minimum parmi les graphes à n sommets ? Dans cet exposé je vais présenter différentes approches pour aborder cette question de combinatoire extrémale. J'exposerai tout d'abord une approche probabiliste, utilisant la notion de graphe aléatoire, qui nous permet d'obtenir une borne supérieure proche de la borne inférieure générale de [1]. Ensuite, j'expose- rai les liens étroits que l'on peut établir entre les codes identifiants et d'autres types de codes, en particulier les codes superimposés, ce qui nous permettra d'obtenir une borne inférieure améliorant celle de [1]. Enfin, je présenterai des constructions basées sur des plans projectifs. Références : [1] M. G. Karpovsky, K. Chakrabarty, L. B. Levitin, On a New Class of Codes for Identifying Vertices in Graphs, IEEE Transactions on Information Theory 44(2), 599-611 (1998). [2] I. Charon, O. Hudry, A. Lobstein, Minimizing the size of an identifying or locating-dominating code in a graph is NP-hard, Theoretical Computer Science 290(3), 2109-2120 (2003).
Les automates cellulaires sont des systèmes dynamiques discrets composés de cellules agencées régulièrement et qui interagissent localement. Bien que les interactions locales soient très simples à décrire, le comportement du système dans son ensemble est très difficile à prévoir. Dans cet exposé, je présenterai d'une part une approche formelle, basée sur des pré-ordres de simulation, pour comparer et classifier les dynamiques globales de ces objets. Je montrerai comment des classes d'automates définies par des propriétés dynamiques classiques se traduisent dans la structure de ces pré-ordres. Je présenterai également une construction qui permet d'obtenir divers ordres-induits remarquables de certains pré-ordres de simulation, ainsi qu'un automate cellulaire intriguant, capable de simuler le comportement d'une machine de Turing avec un nombre fini arbitrairement grand de têtes de calcul, mais qui interdit la cohabitation simultannée d'un nombre infini de têtes. J'aborderai d'autre part les automates cellulaires comme des objets syntaxiques et étudierai la densité de diverses propriétés de ces objets. Je montrerai comment une contrainte syntaxique locale permet de définir une classe (les automates cellulaires captifs) dans laquelle les propriétés monotones suivent une loi zéro-un. En particulier je montrerai que, dans cette classe, la propriété d'être intrinsèquement universel a une densité 1 tout en étant indécidable.
La logique quantique, qui est une composante importante des travaux visant à la compréhension du monde quantique, reste mal comprise et difficilement utilisable en pratique. Grâce à la mise en évidence de l'importance de notions "classiques" comme les points de vue ou la connaissance partielle, nous montrons comment il est possible d'obtenir de nouvelles pistes pour l'étude de ce type de logique, avec en particulier des méthodes de recherche automatique de preuves. Dans cet exposé, nous présenterons un ensemble de résultats nous effectuerons une présentation de la logique quantique ainsi que le modèle usuel de cette logique, à savoir les treillis orthomodulaires. Ensuite, nous exposerons une approche utilisant les "systèmes de représentation" (développés par l'auteur durant sa thèse de doctorat, voir bibliographie) basée sur les notions de connaissance partielle et de points de vue qui permet de fournir une caractérisation purement classique et non probabiliste (basée sur l'utilisation d'algèbres booléennes). Nous montrerons enfin comment cette caractérisation permet d'envisager la logique quantique d'une nouvelle manière, et fournir de nouveaux outils pour son étude. En particulier, nous présenterons un fragment décidable de cette logique, sous forme de calcul des séquents. Références: http://www-leibniz.imag.fr/~obrunet
Dans cet exposé nous présenterons deux formalismes de réécriture d'ordre supérieur permettant l'utilisation de filtrage "à la ML". Le premier de ces formalismes, le lambda P calcul, est une extension du calcul lambda sigma traitant de manière complètement explicite les notions de substitution et de filtrage. Nous montrerons qu'il possède les propriétés de normalisation forte sur les termes typés et de confluence. Le second formalisme est un formalisme de réécriture d'ordre supérieur fondé sur les (S)ERS. Ce formalisme autorise la définition de systèmes de réécriture utilisant la notion de filtrage. Nous donnerons un critère syntaxique de confluence pour de tels systèmes.
On considère un polyèdre, on définit alors le billard polyédral de la facon suivante: On part d'un point d'une face, on se donne une direction et on se déplace dans cette direction jusqu'à rencontrer une autre face. On obtient un nouveau point, la direction est alors réfléchie orthogonalement par rapport à cette face. Pour étudier cette application on repère chaque face par une lettre, l'orbite d'un point devient une suite de lettres. C'est ce qu'on appelle un mot. Le but est d'étudier ces mots grace en autre à leurs fonctions de complexité. Nous présenterons les estimations connues pour un polyèdre général, et nous nous intéresserons plus précisemment au cas du cube.
Dans cet exposé, on développera une interprétation de la logique linéaire en termes de processus concurrents. On utilise pour cela une variante du pi-calcul, munie d'une notion paramétrable d'observation (divergence, may- ou must-testing...), d'où l'on déduit une notion abstraite de comportement. La structure de ces comportements mène à la définition de connecteurs logiques, inspirés des logiques spatiales et temporelles, qui décrivent les propriétés fondamentales des processus. Le système obtenu est une forme de logique linéaire qui définit pour le pi-calcul un système de type qui garantit de bonnes propriétés comme la terminaison et l'absence de blocage. D'autre part, ce système de type établit une correspondance à la Curry-Howard entre la concurrence et diverses variantes de logique linéaire, qui s'intègre bien aux précédentes études sur la décomposition du calcul fonctionnel dans les calculs concurrents.
Dans cet exposé, je présenterai la structure de polygraphe, une sorte de complexe cellulaire, à travers ses liens avec la réécriture et la logique. Dans la première partie, nous verrons comment tout système de réécriture de termes peut être traduit sous la forme d'un polygraphe, vu ici comme un système de réécriture de circuits. Sur un exemple, je montrerai comment construire des ordres de terminaison adaptés à ces objets. Dans la seconde partie, nous traduirons le calcul propositionnel et ses démonstrations en un polygraphe : cela permet d'obtenir des représentations bidimensionnelles pour les formules et tridimensionnelles pour les démonstrations. Enfin, si le temps le permet, je parlerai d'une piste menant à une autre description polygraphique des démonstrations classiques, toujours en trois dimensions.