Institut de Mathématiques de Luminy
SÉMINAIRES 2007
Logique et Interactions

Organisateur :
Yves Lafont (téléphone : 04 91 26 96 37)
Lieux : IML, Bâtiment TPR2- CNRS :
Salle de Séminaires : 3ème étage (304-306).
Horaire : en règle générale le jeudi, à 14h.

jeudi 29 novembre
Claudia Faggian (PPS, Jussieu) :
Ludics and true concurrency

Abstract: In this talk we present an overview of recent work developed in collaboration with Pierre-Louis Curien and Mauro Piccolo. Our aim is to bridge between structures which appear in Proof Theory, Game Semantics and Concurrency Theory. In particular, we explore the relation between Ludics [Girard 01], Event structures [Nielsen-Plotkin-Winskel 81], and a typed process calculus. Ludics has been introduced by Girard as an abstract game semantical model; event structures are a standard model of true concurrency.
Our approach relies on the setting of Ludics, where a key role is played by the notion of name (addresses). Moreover, we integrate both proof-net technology and geometrical ideas on causality which underly models of true concurrency. We show that the class of confusion-free event structures can be seen as a generalization of Ludics strategies, and we provide a common presentation for composition in both settings. We show that names in Ludics have the same role as process calculus channels, and actually follow the same discipline of names in Sangiorgi's internal calculus. To make precise the correspondence with process calculi, we analyze in game-semantical terms an asynchronous typed pi-calculus introduced by Yoshida, Honda, and Berger, and show that Ludics is a fully complete and fully abstract model of the finitary linear pi-calculus.

jeudi 22 novembre
François Métayer (PPS, Jussieu) :
n-catégories cofibrantes

Résumé : Dans de nombreuses situations familières, les objets construits librement sont projectifs, c'est-à-dire qu'ils possèdent la propriété de relèvement à gauche par rapport aux épimorphismes.
Nous verrons d'abord, sur des exemples très simples, pourquoi il n'en est pas toujours ainsi. Dans ces cas, de nature géométrique, la bonne généralisation de la surjectivité n'est plus la notion d'épimorphisme, mais celle de fibration acyclique, et les objets cofibrants sont par définition ceux qui ont la propriété de relèvement à gauche par rapport aux fibrations acycliques. Je montrerai que dans le cadre des catégories de dimensions supérieures ce sont exactement les objets librement engendrés par un polygraphe.

jeudi 15 novembre
Hugo Herbelin (INRIA, LIX) :
Autour de la dualité du calcul

Résumé : Le calcul mu-mu-tilde est un cadre syntaxique simple permettant d'exhiber deux dualités fondamentales du calcul :
- une dualité terme / contexte évaluation, dont l'interaction donne naissance au calcul;
- une dualité appel par nom / appel par valeur, selon que le calcul est sous contrôle du contexte d'évaluation ou du terme.
Le calcul mu-mu-tilde peut être vu comme une syntaxe pour la partie purement structurelle (d'une variante) du calcul des séquents de Gentzen. En particulier, il permet une représentation originale des preuves du calcul des séquents sous forme de pure dérivation de formule (sans mention explicite du contexte).
Nous présenterons le calcul mu-mu-tilde et ses extensions. Nous discuterons probablement de sa relation avec LL et avec LC. Nous digresserons certainement sur la relation entre modèle de jeux de la logique et la structure des preuves du calcul des séquents et aborderons peut-être la connexion entre appel par valeur et dialogues de Lorenzen. Enfin, le rôle des délimiteurs de continuations dans l'obtention de certaines propriétés de complétude de la logique classique sera évoqué.

jeudi 8 novembre
Kazushige Terui (
Sodenkai, Japon) :
On space efficiency of Krivine Abstract Machine
and Pointer Abstract Machine

Abstract: Our ultimate goal is to reconstruct the computational complexity theory fully based on logic and types. In this talk, we in particular discuss the space efficiency of evaluation in lambda calculus. It is well known that composition of two Turing machines (TM) has to be done in an interactive (game semantic) way. This motivates us to study game-like evaluation mechanisms such as Krivine's Abstract Machine (KAM) and Pointer Abstract Machine (PAM) of Danos-Regnier.
We show that:
i) KAM space-efficiently simulates TM. Hence the space hierarchy theorem implies that there is no uniformly (i.e. for all terms) and significantly (eg. quadratically) more efficient way of evaluation than KAM.
ii) PAM evaluates every simply typed term up to rank 3 in PSPACE. This conforms to Schubert's theorem that normalization of rank 3 terms is PSPACE-complete. Hence there is no exponentially more efficient way of evaluation than PAM for rank 3 terms (unless PSPACE = LOGSPACE).

vendredi 26 octobre
Krzysztof Worytkiewicz (
Ecole Polytechnique, LIX) :
Variétés et espaces algébriques dans le contexte localement ordonné

Résumé : La motivation pour étudier certaines interactions entre une topologie et une strucutre d'ordre locale sur un ensemble vient en grande partie de la concurrence. Comme mis en avant notamment dans les travaux d'Eric Goubault et coauteurs, on peut voir un espace localement ordonné comme cadre où évoluent des sytèmes de processus parallèles. La structure continue represente alors le temps "objectif" ou "global" alors que l'ordre représente le temps "local" autrement dit la "progression" d'un système. Un calcul s'apparente dans ce cadre à un chemin croissant alors que l'exclusion mutuelle de n processus est modélisée par des trous n-dimensionels.
Bien evidement, les notions classiques d'homotopie et d'homologie doivent être revisitées de manière détaillée afin de tenir compte de la structure d'ordre. Il existe cependant une alternative si l'on choisit un point de vue légèrement moins classique. En effet, il est possible d'identifier les espaces localement ordonnés d'intérêt comme certaines sous-catégories d'un certain topos de Grothendieck. Ceci revient à se placer dans un "contexte géométrique" (l'expression est due à B. Toen) et exploiter la machinerie existante à ce niveau de généralité, ainsi que les analogies avec les autres contextes géométriques tel celui des variétés differentielles où ceux des schémas.
Après un rappel sur les faisceaux et les topologies de Grothendieck, mon exposé portera essentiellement sur la construction du contexte géométrique des espaces localement ordonnés. Si le temps le permet, j'aborderai de manière informelle ses "théories d'intervalles" et les structures de modèles associées.

jeudi 11 octobre
Richard Lassaigne (
Univ. Paris 7) :
Vérification probabiliste et approximation

Résumé : Cet exposé présente un état de l'art de résultats récents concernant deux types d'approximation qui peuvent être utiles dans le contexte de la vérification pour réduire la complexité en temps et en espace. Dans le premier cas, on introduit une notion d'approximation sur les données, c'est-a-dire sur le modèle à verifier, définie à l'aide d'une distance. Il est alors possible de concevoir des algorithmes probabilistes permettant de décider, en temps indépendant de la taille du modèle, si la propriété considérée est satisfaite ou si elle est loin, à epsilon près au sens de la distance, de l'être. Dans le second cas, on définit une méthode d'approximation pour la vérification de propriétés quantitatives sur des systèmes probabilistes. Les algorithmes probabilistes d'approximation ainsi obtenus permettent de réduire de manière exponentielle la complexité en espace. Ce type d'algorithme a été implémenté de manière distribuée dans un model checker probabiliste qui s'est révélé être un outil de vérification et de simulation très efficace.

jeudi 4 octobre
Report de la séance

jeudi 27 septembre
Michele Basaldella (
Università di Siena) :
Exponentials in Ludics: How and at what price

Abstract: Ludics is a research project introduced by J-Y Girard in 2001 and it also provides a (fully complete) Game Semantics for Multiplicative Additive Focalized Linear Logic. We want to explain how to extend Ludics framework by adding exponential constructions which preserve Analytical Theorems (in particular Separation Theorem). We also show that exponential isomorphisms are preserved in our setting and we introduce the notion of "uniform" and "non-uniform" exponentials, which are structures that naturally arise from our architecture. Unfortunately, Correctness Theorem with respect to Focalized Linear Logic holds only in a weak form

mercredi 5 septembre
André Hirschowitz (
Laboratoire J.-A. Dieudonné, Univ. Nice) :
Enseigner les preuves avec Coqweb

Résumé : Faut pas le dire, mais l'enseignement supérieur des sciences (à Nice?), ça marche pas trop (taper Objectif70 dans Google). Faut pas le dire, mais nous, les universitaires (niçois?), on n'a pas trop le temps de s'occuper de ce problème, on est débordés. Et les autres, ministres et recteurs, gare à eux s'ils s'avisaient de se mêler de nos affaires. Par exemple on ne cherche pas trop à enseigner la rigueur autrement que par la méthode dite de Léo Lacroix ("faites comme moi"), qui a largement fait ses réfutations. Ceux qui essaient de faire autrement, forcément, ils y arrivent pas du premier coup, et ils se font casser bien avant d'y arriver.
Coqweb (à taper dans Google pour voir) propose une nouvelle méthode. C'est une interface web pour Coq, principalement développée par Loïc Pottier pour l’enseignement. Il permet aux enseignants de proposer des énoncés sous une forme suffisamment familière. Les étudiants sont invités à démontrer ces énoncés essentiellement en cliquant. Des indications peuvent être données en langage naturel, et dans ce cas, l’interface vérifie que l’étudiant a bien compris l’indication. On dira un peu de ce qu'il ne faut pas dire, puis on racontera comment Coqweb marche bien et ce qu'on a fait avec.

mardi 26 juin
Yves Lafont (
IML) :
Catégories enrichies, division à gauche
et calculs … homotopiques

Résumé : Si on remplace systématiquement les identités algébriques par des calculs, puis les identités entre calculs par d'autres calculs, et si on poursuit ce mécanisme de résolution jusqu'à l'infini, on se retrouve naturellement dans une omega-catégorie, qui est aussi une catégorie enrichie sur elle-même. On introduit alors une notion d'homotopie en termes de connexions réversibles. Le lemme de division à gauche (et à droite) permet de démontrer un théorème de transport pour ces connexions. Ces techniques sont utilisées pour construire une nouvelle catégorie de modèles (de l'algèbre homotopique). Il s'agit d'une collaboration avec François Métayer et Krzysztof Worytkiewicz.

mardi 19 juin
Esfandiar Haghverdi (
Indiana University) :
Categorical trace and geometry of interaction

Abstract: In this talk I will explain my work on Geometry of Interaction (GoI) from a categorical point of view. I will discuss the significance of the notion of categorical trace due to Joyal, Street and Verity in modelling the execution formula of GoI. More specifically, I will discuss a GoI semantics for MELL based on traced unique decomposition categories and show that Girard´s operator algebraic approach in GoI 1 is captured in this categroical setting. Most of the talk will be based on my joint paper with P.J. Scott published in Theoretical Computer Science vol. 350, 2006.

mardi 29 mai
Alain Prouté (
Paris 7) :
Sur quelques liens entre théorie des topos
et théorie de la démonstration

Résumé : C'est en travaillant à la réalisation d'un logiciel de formalisation des mathématiques (délibérément) fondé sur la théorie des topos, que j'ai été amené à explorer cette structure d'un point de vue calculatoire. Les liens entre catégories cartésiennes fermées et normalisation forte du lambda-calcul sont maintenant bien connus, et c'est donc sur le contenu calculatoire du classifiant du foncteur des sous-objets que porte cet exposé. On aboutit ainsi à une conception de la correspondance preuve-programme beaucoup moins symétrique que celle proposée par les concepts Martin-Löf/Curry-Howard, mais certainement plus proche des mathématiques usuelles, et où on reparle d'axiome du choix et d'indiscernabilité des preuves.

mardi 22 mai
Anne Crumière (
IML) :
Circuits positifs et différentiation spatiale

Résumé : L'expression des gènes est contrôlée par un ensemble complexe de régulations, modélisé par un graphe dirigé signé appelé graphe de régulation génétique. Une fois ce graphe établi, on s'intéresse à ses propriétés dynamiques. Le biologiste R. Thomas dans les années 80 a énoncé la règle générale suivante : une condition nécessaire pour la multistabilité est la présence d'un circuit positif dans le graphe de régulation. La multistabilité correspond à un important phénomène biologique, appelé processus de différentiation cellulaire
Durant cette dernière décennie, de nombreux chercheurs ont proposé et démontré cette règle dans un cadre différentiel et plus récemment dans un cadre discret, notamment Elisabeth Remy et Paul Ruet. Mais quelque soit le formalisme, la règle de Thomas n'a été prouvée que dans la cas d'une seule cellule, plus précisement quand les gènes en jeu dans le graphe de régulation appartiennent à la même cellule, on s'intéresse uniquement à des circuits positifs intracellulaires. J'ai étendu cette règle à des systèmes intercellulaires (les interactions entre gènes peuvent être entre deux gènes d'une même cellule ou entre deux gènes de deux cellules voisines) en établissant des connections entre différentiation spatiale et l'existence de circuits positifs. J'ai étudié deux configurations : les cellules sont localisées sur une grille à une dimension, puis à deux dimensions. Je vous exposerai ces résultats.

vendredi 20 avril
Guillaume Malod (
Univ. Mons-Hainaut, Belgique) :
Circuits avec deux opérations

Résumé : Valiant a defini des classes de complexité pour les suites de polynômes, en utilisant le modèle des circuits arithmétiques calculant sur un corps. On peut voir les circuits comme un modèle général pour étudier les calculs avec deux opérations. Je présenterai la théorie de Valiant dans ce cadre général, ainsi que les résultats principaux, les problèmes ouverts et les liens avec d'autres branches de la complexité.

mardi 10 avril
Sylvain Lippi (I3S,
Univ. Nice) :
Combinateurs d'interaction dure

Résumé : Les systèmes d'interaction durs, une sous-classe des réseaux d'interaction, se présentent sous la forme de systèmes de re-étiquetage de graphes fortement confluents. Nous présentons un système d'interaction dur universel avec quatre symboles et sept règles dans lequel on peut traduire tous les autres systèmes durs. On montrera en particulier comment faire du calcul booléen avec un tel système.

mardi 3 avril
Stephen Lengrand (
PPS et Univ. St Andrew, UK) :
Un calcul des séquents pour la recherche
de preuve en théorie des types

Résumé : Basé sur la deduction naturelle, le formalisme des Systèmes de Types Purs (PTS) capture une grande varieté de théories des types. De nombreux assistants à la preuve (par exemple, Coq et Lego) sont basés sur celles-ci, et c'est pourquoi nous nous intéressons à la recherche de preuve dans les PTS. Nous introduisons pour cela les Pure Type Sequent Calculi (PTSC) en enrichissant le calcul des séquents LJT, adapté à la recherche de preuve et fortement lié à la déduction naturelle. Comme les PTS, les PTSC satisfient la Subject Reduction et sont confluents. Un PTSC est logiquement équivalent au PTS correspondant, et l'un est fortement normalisable si et seulement si l'autre l'est. Nous montrons comment les règles de conversions peuvent être integrées aux autres règles, afin que les tactiques primitives de recherche de preuve (comme dans Coq) deviennent simplement l'application "bottom-up" des règles d'inference des PTSC. La formalisation de tactiques plus complexes motive l'extension du formalisme avec des méta-variables (pour représenter des preuves incomplètes) ainsi que des contraintes d'unification (que l'instantiation finale de ces meta-variables devra satisfaire). Cette fois-ci, l'application bottom-up des règles d'inference permet d'exprimer des algorithmes d'énumeration des habitants d'un type (Dowek, Munoz), ainsi que l'unification d'ordre supérieur (travail en cours).

mardi 27 mars
Ugo dal Lago (
Univ. Bologne) :
Context semantics
and implicit computational complexity

Abstract: Implicit Computational Complexity aims at giving machine-independent characterizations of complexity classes based on mathematical logic. Context semantics has been introduced as a model of Geometry of Interaction and has been shown useful in proving correctness of optimal reduction algorithms. Interestingly, the intensional nature of context semantics can be exploited in (re)proving correspondences between logical systems and complexity classes. We illustrate some of these results, namely some correspondences between subsystems of Godel's T and MELL on one side and complexity classes on the other side. Then, we will comment on the possibility of using the same techniques in the quantitative analysis of sharing graph reduction.

mardi 13 mars
Nadia Creignou (
Univ. Méditerranée, LIF) :
Satisfaction de contraintes d'appartenance
et complexité
Joint work with V. Chepoi, M. Hermann, G. Salzer.

Abstract: We study the complexity of membership constraint satisfaction problems over finite domains, i.e., the satisfiability of formulas in conjunctive normal form with literals expressing the membership of a value in a given subset of the finite domain. Given a family of subsets S we denote by S-formulas those whose literals are built upon the sets belonging to S. We show that the satisfiability of S-formulas with three or more literals per clause is either trivial or NP-complete, depending on a nonempty intersection of all sets from the family S. For bijunctive S-formulas the complexity depends on the Helly property of the family S, i.e., the satisfiability problem for bijunctive S-formulas is decidable in polynomial time if S is a Helly family, otherwise it is NP-complete. We also present a polynomial-time algorithm deciding if a given family S satisfies the Helly property. Finally we discuss the application of our result for several well-known examples of Helly families in discrete mathematics.

mardi 20 février
Frédéric Ruyer (
Univ. Savoie, LAMA) :
Modèles pour le calcul et la logique

Résumé : Nous présentons une classe de modèles du lambda-calcul et de la logique du second ordre. Les modèles sont basés sur des treillis et interprètent la réduction, ainsi que la relation de réalisabilité, à l'aide de la relation d'ordre. Nous tenterons de dégager les liens avec les algèbres de Heyting et les modèles à base de cpo du lambda-calcul.

mardi 13 février
Ian Mackie (
Ecole polytechnique, LIX) :
Linearity and Optimality

Résumé : In this talk I will present some new ideas and partial solutions on implementing the lambda calculus. We first re-examine notions of optimality for the linear case, and then show a variety of methods that can be used to extend these results to the general case. This work is leading towards a new theory of optimal reduction for the lambda calculus based on geometry of interaction style implementations.

mardi 30 janvier
Gilles Dowek (
Ecole polytechnique, LIX) :
Les algèbres de valeurs de vérités
et la normalisation des preuves

Résumé : 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.

mardi 23 janvier
Yves Lafont (
IML) :
Le problème du mot pour les nuls

Résumé : Problème du mot : Soit G un groupe présenté par un nombre fini de générateurs et de relations. Peut-on savoir si un mot écrit avec ces générateurs définit l'unité de G ?
Version topologique : Soit X défini en collant un nombre fini de polygones sur un graphe fini. Peut-on savoir si deux chemins parallèles sont homotopes dans X ?
L'indécidabilité de ce problème a été démontrée il y a cinquante ans par Novikov puis Boone, en utilisant des traductions compliquées. Aujourd'hui, on peut expliquer la preuve assez simplement en utilisant la réécriture de mots. Il n'y a pas de prérequis particulier.

mardi 16 janvier
Samuel Hym (
Univ. Denis Diderot, PPS) :
Typage et contrôle de la mobilité

mardi 9 janvier
Paul Ruet (
IML) :
Dynamique discrète et structure
des réseaux de régulation génétique

EL, le 7 novembre 2007