Pure, or type-free, linear lambda calculus is Turing complete once reduction is considered as computation. We introduce modal impredicativity as a new form of impredicativity causing reduction to be problematic from a complexity point of view. Modal impredicativity occurs when, during reduction, a residual of a box b interacts with the body of another residual of b. Technically speaking, superlazy reduction is a new notion of reduction that allows to control modal impredicativity. More specifically, superlazy reduction replicates a box only when all its copies are opened. This makes the overall cost of reducing a (linear) lambda-term finite and predictable. Specifically, superlazy reduction applied to any pure proof nets takes primitive recursive time. Moreover, any primitive recursive function can be computed by a lambda-term via superlazy reduction.
Dans cet exposé, nous allons d’abord présenter les logiques modales plates de point fixe (flat modal fixpoint logics). Chaque logique de ce type est une extension de la logique modale K et, au même temps, un fragment du $\mu$-calcul modal propositionnel. Nous aborderons le problème de trouver, de façon uniforme, une axiomatisation de ces logiques qui soit complète par rapport à leur interprétation standard sur les modèles de Kripke.
Nous verrons comme certaines idées de l’algèbre, de la coalgèbre, et de la théorie des catégories, sont fondamentales pour notre but: la dualité, par la notion de modalité de couverture, les adjoints, avec la généralisation aux O-adjoints, les objets libres, la notion de point fixe constructif, les rétractés. Ainsi, nous serions en mesure de proposer une axiomatisation complète pour chaque logique plate de point fixe. (Travail en collaboration avec Yde Venema).
Voir la page dédiée.
Je dirai où en est PML, notamment, l'algorithme de typage et le proof-checking. Je montrerai les premiers exemples de programmes prouvés en PML.
The aim of this talk is to present the problem of enumerating terms in untyped lambda calculus. The very first idea was to compute the asymptotic density of strongly normalizing closed lambda terms among all closed terms of a given size. However, the preliminary task of counting lambda terms turned out to be already non-trivial and challenging and this is therefore as the main theme. I will show recent results which were obtained due to cooperation between universities in Chambery, Versailles and Krakow.
Les sémantiques de jeux ont été introduites pour capturer le comportement interactif des preuves en interprétant les formules par des jeux sur lesquels les preuves induisent des stratégies. L'une des difficultés majeures lors de la définition de telles sémantiques, est de les rendre précises, c'est-à-dire de caractériser les stratégies définissables, qui sont l'interprétation d'une preuve (ou d'un programme par la correspondance de Curry-Howard). L'extension des caractérisations habituelles à des langages de programmation comportant des constructions concurrentes nécessite de repenser en profondeur les définitions habituelles de sémantique des jeux, en menant une analyse fine de la structure dépendances entre les coups dans les stratégies. Nous présentons ici deux approches axiomatiques pour décrire cette structure : l'une externe, fondée sur la présence de certaines tuiles de permutation de coups dans les stratégies, l'autre interne, décrivant la catégorie des stratégies comme une structure algébrique libre.
Voir la page dédiée.
Au début des années 60, Wang a introduit un modèle de pavage du plan à l'aide de tuiles orientées de taille unitaire aux bords colorées pour résoudre des problèmes de logique. Ce modèle a été montré Turing-équivalent par Berger qui montra qu'un jeu de tuiles pouvait simuler une machine de Turing. Nous nous intéressons a la calculabilité de ce modèle en introduisant des outils sur les pavages permettant d'obtenir des résultats plus généraux sur les jeux de tuiles. A l'aide de notions de simulation, nous obtenons une première approche de l'universalité puis, nous montrons quelques uns des théorèmes fondamentaux de la calculabilité (Kleene, Rice...), dans le cadre des pavages, toujours relativement à certaines notions de simulation. Ces résultats nous permettront d'obtenir dans un premier temps de nouvelles preuves sur des théorèmes classiques des pavages et dans un deuxième temps de construire un cadre de construction de jeux de tuiles apériodiques.
Dans cet exposé, nous commencerons par résumer les résultats connus sur les modèles classiques de piles de sable (SPM, IPM(k)) et sur quelques-unes de leurs extensions. Nous verrons que l'approche combinatoire a des limites, justifiant ainsi leur étude au travers d'un nouveau système dynamique discret, les automates de sable.
Nous définirons ce système, en rappelant en permanence les liens existant entre celui-ci et un autre système dynamique mieux connu, les automates cellulaires. Puis, après avoir rappelé quelques-une des propriétés basiques des automates de sable, nous définirons des propriétés dynamiques à l'aide d'une topologie compacte inspirée de celle utilisée pour l'étude des automates cellulaires.
Ces propriétés permettent une étude plus globale de la dynamique d'un modèle donné, avec des techniques topologiques puissantes. Nous verrons ainsi comment classer les automates selon leur ``chaoticité'', en s'inspirant de la classification pour les automates cellulaires 1D de Kůrka. Ces résultats permettent de souligner que les automates de sable sont un système intermédiaire entre les automates cellulaires de dimension d et d+1.
La logique linéaire s'interprète dans les espaces vectoriels, même si les exponentielles posent problème (on obtient des espaces de dimension infinie). Dans le cas fini, cette interprétation est malheureusement un peu dégénérée car l'interprétation d'une formule (un espace vectoriel) est isomorphe à celle de sa négation (l'espace des formes linéaire sur cet espace). Christine a récemment proposé une solution : en plus de l'espace vectoriel, on rajoute une notion de totalité. Typiquement, une fonction linéaire de A dans B est totale ssi elle envoie les vecteurs totaux sur des vecteurs totaux. Algébriquement parlant, la totalité est un sous-espace affine de l'espace vectoriel considéré.
Christine introduira tout ça avec un peu plus de détails, et expliquera comment obtenir un premier résultat de complétude : complétude d'un calcul booléen basé sur la traduction habituelle du type Bool => Bool dans la logique linéaire. Pierre poursuivra avec un second résultat toujours de complétude : complétude d'une logique linéaire sans exponentielles. (Ça, c'est si la preuve ne « devient » pas fausse d'ici là...)
Le premier résultat ne nécessite aucune connaissance en logique linéaire (si si, c'est vrai), et le second présuppose un modicum de logique linéaire pour comprendre le pourquoi (mais pas le comment). Des connaissances de base en algèbre linéaire sont nécessaires, mais rien de compliqué, et seulement en dimension finie.
Dans le modèle des automates cellulaires, la non-linéarité est omniprésente. Une voie pour étudier ces objets peut être la théorie du chaos déterministe. Elle a déjà été largement empruntée dans la littérature (avec les travaux de P. Kurka notamment), mais pratiquement toujours en se restreignant à la dimension 1. En ce concentrant sur certaines propriétés autour de la sensibilité aux conditions initiales, nous montrerons dans une première partie de cet exposé que cette restriction n'est pas neutre : une nouvelle classe de comportements dynamiques (les automates cellulaires non sensibles aux conditions initiales mais sans point d'équicontinuité) apparaît à partir de la dimension 2. De la démonstration de l'existence de cette classe, nous tirerons d'autres résultats montrant que la complexité de certaines propriétés fait un bond lorsque l'on quitte la dimension 1.
Dans une seconde partie d'exposé, nous prendrons un peu de recul sur la question de la variation de complexité des propriétés en fonction de la dimension. Nous poserons un cadre logique formalisant ce que l'on peut appeler la ``dynamique topologique'' dans les automates cellulaires. Nous aborderons alors le problème suivant : étant donnée une propriété (une formule dans notre théorie), quel est la complexité de l'ensemble des automates cellulaires qui la satisfont ? cet ensemble est-il arithmétique ? à quelle hauteur dans la hiérarchie ? comment cette hauteur varie avec la dimension ?
Selon la vitalité de l'orateur, le traitement de ce questionnement pour aller du simple traitement d'exemples à la démonstration d'un résultat général.
Composition of strategies is the crucial operation of game semantics. It corresponds to cut elimination in proof theory. This paper is an attempt to uncover the sheaf-theoretical nature of these two operations. We define a game semantics with a topological flavor for a variant of Multiplicative Additive Linear Logic (henceforth MALL). We show that the standard notion of strategy leads to a correct, yet incomplete model. We then introduce a new, non-standard notion of local'' strategies, which turn out to form a sheaf. <br><br> Composition of strategies is generally divided into two steps: interaction, and hiding. In our setting, interaction arises as gluing in the sheaf of local strategies. Hiding along a cut c: U -> V appears here as an instance of a more general operation,descent'' along c, which also encompasses cut elimination. Descent along c is a morphism of sheaves on V from the direct image along c of local strategies on U, into cut-free local strategies on V. It arises from a factorisation system, roughly dividing plays into their cut-only and cut-free parts.
Finally, our notion of (winning) local strategy is validated by the expected soundness and completeness results w.r.t. MALL provability.
Je parlerai des zippers : leurs principes, comment ils amènent à une notion de dérivée de type de données. On verra alors une première définition de cette dérivée par McBride, quelques problèmes et une deuxième définition pour y répondre. Puis nous passerons brièvement aux containers, une notion générale de type de données. Nous verrons comment étendre la notion de dérivée aux containers pour finir sur une formule de Taylor des containers.
Les espaces cohérents de Jean-Yves Girard et les espaces de finitude de Thomas Ehrhard sont obtenus à partir d'une base « similaire » : l'orthogonalité.
Je commencerais par rappeler comment ça marche (parce que c'est intéressant et pas très compliqué), puis je passerais à une structure mixte qui permet de générer des espaces de finitude « simples » à partir d'espaces cohérents.
Cette construction contient tous les exemples usuels d'espaces de finitude et de plus, elle commute avec les opérations logiques (⅋, ⊗, ⊕, &, ⊸, !, …) Un des aspects intéressants est l'utilisation du théorème de Ramsey infini pour démontrer certaines propriétés de cette construction.
Je finirais par expliquer comment on tombe sur une notion qui généralise les fonctions stable de Berry pour permettre d'interpréter une version simple du λ-calcul algébrique de Lionel, Thomas et consorts.
Remarques : j'essaierais, autant que possible, de ne pas supposer connue toute la logique linéaire. Les deux premiers tiers de mon exposé devraient donc être « self-contained »...
La droite réelle de Harthong-Reeb est un modèle non-standard du continu qui est à l'origine de nombreux développements en géométrie discrète (entre autre la droite discrète de Réveillès). Selon Harthong et Reeb eux-mêmes leur modèle n'est pas sans liens avec une approche constructive. Récemment à Poitiers et à La Rochelle nous nous sommes intéressés à cette question en montrant que la droite de Harthong-Reeb vérifie les axiomes de Bridges qui sont une théorie de la droite réelle constructive.
L'orateur propose un deuxième exposé, qui aura peut-être lieu l'après-midi s'il y a des volontaires :
We present a variant of the explicitly-typed second-order polymorphic λ-calculus with primitive open existential types, i.e., a collection of more atomic constructs for introduction and elimination of existential types. We equip the language with a call-by-value small-step reduction semantics that enjoys the subject reduction property. We claim that open existential types model abstract types and module type generativity. Our proposal can be understood as a logically-motivated variant of Dreyer’s RTG where type generativity is no more seen as a side effect. As recursive types arise naturally with open existential types, even without recursion at the term-level, we present a technique to disable them by enriching the structure of environments with dependencies. The double vision problem is addressed and solved with the use of additional equalities to reconcile the two views.
Voir la page dédiée.
Cours puis groupe de travail sur la réalisabilité avec Alexandre Miquel. Détails ici.
Le project MathLang a pour but de computeriser des textes de mathematiques selon des degres de formalisation differents, et sans preciser d'avance un engagement dans:
* un logique particulier (par example, sans devoir choisir comme base une theorie des ensembles, une theorie des categories, une theorie des types, etc.)
* un systeme de demonstration particulier (par example, sans devoir choisir comme systeme de demonstration Mizar, Isaeblle, Coq, PML, etc.).
MathLang laisse les choix concernant les systemes de demonstration et de la logique ouverts tant que c'est possible. En plus, MathLang permet des niveaux varies de computerisation, et n'insiste pas qu'une formalisation soit complete comme c'est fait dans les fondations de la mathematiques a la Russell et Frege ou dans les systemes de demonstration (comme initie par de Bruijn). Pendant la computerisation, le text mathematique est d'abord insere dans l'ordinateur tel qu'il est ecrit par le mathematicien sur papier. Puis un ou plusieures aspets de MathLang sont appliques au texte pour donner des versions du texte qui sont (automatiquement) controles a des niveaux differents:
1. Un aspect de base est l'extension du texte avec l'information categorique (terme, nom, adjectif, proposition, etc) ou la coherence et la structure grammaticale du texte sont controlees automatiquement.
2. Un autre aspect partage le texte en parties annotees par des relations (e.g., Corollaire A utilise Theorem B) et automatiquement controle la structure logique du texte (ce n'est la correction logique du texte).
3. Un autre aspect transforme le texte alors que les trous dans les preuves sont evidents.
4. D'autres aspects transforment cette version derniere en une formalisation complete (dans Coq, Mizar, Isabelle, etc).
MathLang a ete cree par Fairouz Kamareddine et J.B. Wells en 2000. Nous avons computeriser des textes dans MathLang (pas a pas) jusqu'a des formalisations completes dans Coq et Mizar (aussi Isar/Isabelle). Depuis 2002, 4 etudiants de theses (Manuel Maarek, Kryztof Retel, Robert Lamar et Christoph Zengler) et des dizaines d'etudiants de master et de BSc ont contribue au design et a l'implantation de MathLang et a son utilisation pour la computerisation des textes de Maths.
S'il reste du temps, Fairouz pourra enchaîner sur un exposé plus orienté lambda-calcul:
Titre: Parametres dans le lambda calcul type.
Les fonctions dans le lambda calcul sont toujours d'ordre superieur. Traditionellement, les fonctions en maths sont d'ordre inferieur. Ici, on donne le lambda calcul avec des fonctions d'ordre inferieur et on divise le cube de Barendregt en 8 sous-cubes qui permettent des meilleures representations des constructeurs dans les languages ML, LF et Automath.
C'est un travail commun avec Twan Laan et Rob Nederpelt.
La théorie des pavages par tuiles de Wang a été inventée par (surprise) Hao Wang afin de proposer un problème combinatoire concret correspondant au pouvoir d'expressivité d'un fragment de la logique du premier ordre. La théorie des pavages s'est en fait révélée comme une théorie élégante s'exprimant facilement logiquement, et a ainsi apporté de nombreux résultats en logique mathématique.
Il s'agit dans cet exposé de proposer une présentation des liens entre pavages et logique. On analysera en particulier comment deux des théorèmes fondamentaux sur les pavages se traduisent :
- Par l'existence d'une théorie complète finiment axiomatisable et superstable [Makowsky, Poizat]
- Par le fait que le fragment AEA de la logique du premier ordre forme une classe de réduction conservative [Büchi, Kahr-Moore-Wang]
tout en expliquant bien entendu ce que signifient les nombreux mots potentiellement obscurs des phrases précédentes.
Aucune connaissance sur les pavages n'est nécessaire. Une connaissance rudimentaire de la logique du premier ordre sera appréciée.