Libraries are a major instrument of software engineering, making it possible to reuse code and to distribute labour between programmers with different areas of expertise. The sophisticated application programs we have today would not be possible without huge libraries in areas such as data structures, numerical analysis, signal processing, and computer graphics. Grammars of natural languages are a domain of a lot of expert knowledge, which it would be useful to find in software libraries. However, typical implementations of grammars are monolithic application programs, such as parsers tuned to a particular corpus. New applications typically have to build their grammars from scratch, which makes it costly to build programs such as natural-language interfaces, or to perform high-quality software localization. This talk presents an approach where grammars can be used as libraries for new grammars and for programs that involve natural language components. The approach is implemented in GF (Grammatical Framework), which is a special-purpose functional programming language for writing grammars. Several features of GF are used in an essential way: the division between abstract and concrete syntax; the module system, including parametrized modules; the type system, which is able to enforce grammar checking via type checking; and code generation that makes GF grammars usable in other programming languages, such as C, Haskell, and Java. To bring the discussion to concrete level, we introduce the GF Resource Grammar Library, which implements the basic grammars of ten languages and makes them accessible to non-linguist application programmers. As an application, we show how the library can be used in building a natural-language interface to a proof system.
Cette Thèse est la conclusion de trois ans de travail sur un projet nommé DemoNat. Le but de ce projet est la conception d'un système d'analyse et de vérication de démonstrations mathématiques écrites en langue naturelle. L'architecture générale du système se décrit en 4 phases : 1. analyse de la démonstration par des outils linguistiques ; 2. traduction de la démonstration dans un langage restreint ; 3. interprétation du texte traduit en un arbre de règles de déduction ; 4. validation des règles de déduction à l'aide d'un démonstrateur automatique. Ce projet a mobilisé des équipes de linguistes et de logiciens, les deux premières phases étant la tâche des linguistes, et les deux dernières étant la tâche des logiciens. Cette thèse présente plus en détail ce projet et développe principalement les points suivants : - définition du langage restreint et de son interprétation ; - propriétés du type principal de termes d'un lamlbda-calcul typé avec deux flèches entrant dans le cadre d'un outil linguistique, les ACGs ; - description du démonstrateur automatique.
Cette thèse porte sur l'étude théorique et pratique d'un système de typage appliqué à la preuve de programmes de style fonctionnels. Le système de base est le système ST développé par C.Raffalli; il comporte, outre le polymorphisme, du sous-typage et de l'omission de contenu algorithmique. Nous étudions tout d'abord les modèles de la théorie définie par le système de types en se basant sur des treillis complets comportant des propriétés additionnelles permettant d'interpréter types et termes;puis nous étudions diverses propriétés théoriques du système telles que la réduction du sujet ainsi que son expressivité à travers des exemples traitant de la possibilité ou de l'impossibilité de définir des notions-clés de la logique et de l'informatique théorique. Dans la suite de la thèse, plus appliquée, nous étudions des codages de types de données riches issus de l'informatique dans le Lambda-Calcul, et montrons qu'ils s'intègrent harmonieusement dans le système; la méthodologie développée dans cette partie permet d'étendre le langage de types et le langage de programmation en conservant un critère de consistance assurant la sûreté du code typé.
On propose une notion de modèle pour la logique intuitionniste, qui étend celle fondée sur les algèbre de Heyting. Cette notion de modèle permet de distinguer l'équivalence logique (si A est démontrable, alors B aussi, et vice-versa) de l'équivalence calculatoire (toute démonstration de A est une démonstration de B, et vice-versa), ce que ne permettaient pas de faire les algèbres de Heyting. On montre ensuite que cette notion de modèle peut être utilisée pour démontrer la normalisation des démonstrations dans de nombreuses théories comme l'arithmétique de Peano ou la logique d'ordre supérieur.
In this talk we present a categorical proof theory for a logic for pragmatics. The aim of this logic is to provide a framework that allows to formalize reasoninig about the pragmatic force with which a sentence may be uttered. The concept of pragmatic force comes from speech act theory and plays a crucial role also in certain branches of artificial intelligence, in particular in the developement of communication protocols for software agents. Instead of considering the full-blown theory of speech acts we focus here on speech acts that either have the pragmatic force of an assertion or the pragmatic force of an obligation, and on how these speech acts can be related to each other. In particular, we are interested in a principle proposed by Bellin and Dalla Pozza that allows the propagation of obligations through causal chains of assertions. The study of such principles from the point of view of categorical proof theory is a nontrivial task and we discuss some of the issues that need to be considered in order to get soundness and completeness results.
Conway a grandement participé à l'élaboration de la théorie des nombres surréels et à la théorie des jeux à deux personnes. Rapidement, un nombre surréel peut-être vu comme un jeu (potentiellement infini) très inintéressant. À cause de cette différence, les deux théories se sont depuis développées de manière quasi indépendante. Je présenterais d'abord le noyau commun aux nombres surréels et aux jeux. Ceci expliquera notamment comment il est possible d'obtenir la moitie d'un coup d'avance sur son adversaire. (Obtenir un tiers de coup d'avance est nettement plus complexe !) Je passerais ensuite à la théorie des jeux impartiaux (style Nim) dont la théorie, plus ancienne, est comprise dans la précédente. Le but est de présenter (prouver ?) le théorème de Sprague-Grundy ainsi que la conjecture sur les jeux octaux. Si le temps et l'assistance le permettent, je présenterai les avancées récentes autour des jeux impartiaux où l'on inverse gagnant et perdant (convention de 171 misère 187). Pour les survivants, je pourrais même parler (peut-être pendant le repas) de la catégorie de jeux due à André Joyal : c'est probablement la toute première catégorie monoidale close de jeux / stratégies. (Malheureusement, elle ne permet pas de modéliser la logique linéaire...) Je ne présenterais rien de nouveau dans cet exposé. Il s'agit en quelque sorte d'une publicité vantant les joies insoupçonnées de la combinatoire des jeux. Idéalement, une ou deux personnes auront envie de m'accompagner pour aller regarder un peu plus loin...
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).