Séminaire Logique et interactions

Circuits de rétroaction dans les réseaux génétiques de régulation intercellulaires [mémoire]

Sur l'expressivité des réseaux d'interaction et de leurs variantes non-déterministes [diaporama]

Quels types de processus de calcul peut-on exprimer dans les réseaux d'interaction ? On analysera cette question à l'aide des structures d'événements, un outil qui permet de décrire assez précisement plusieurs aspects fondamentaux de la structure dynamique d'un processus calculatoire (e.g. causalité, parallélisme, non-déterminisme). On trouvera ainsi un nombre de résultats, principalement négatifs, concernant l'expressivité des réseaux d'interaction et de leurs variantes non-déterministes. Notamment, on verra qu'il n'existe pas de codage suffisamment "fidèle" du pi-calcul dans les réseaux d'interaction différentiels.

The Geometry of Interaction purpose is to give a semantic of proofs or programs accounting for their dynamics. The initial presentation, translated as an algebraic weighting of paths in proofnets, led to a better characterization of the lambda-calculus optimal reduction. Recently Ehrhard and Regnier have introduced an extension of the Multiplicative Exponential fragment of Linear Logic (MELL) that is able to express non-deterministic behaviour of programs and a proofnet-like calculus: Differential Interaction Nets.

This paper constructs a proper Geometry of Interaction (GoI) for this extension. We consider it both as an algebraic theory and as a concrete reversible computation. We draw links between this GoI and the one of MELL. As a by-product we give for the first time an equational theory suitable for the GoI of the Multiplicative Additive fragment of Linear Logic.

NL-complétude de la correction M(E)LL (travail réalisé avec P. Jacobé de Naurois) [diaporama]

Je donnerai un nouveau un critère de correction très simple pour les structures de preuves de MLL (et par extension, de MELL). Avec ce n-ième critère nous prouvons que décider la correction de ces structures de preuves est NL-complet.

Unions de familles de réducibilité pour le lambda-calcul et la réécriture [diaporama]

Les techniques de preuve les plus flexibles pour la normalisation forte (d'extensions) de lambda-calculs types reposent sur des interprétations de types, parmi lesquelles on distingue les candidats de réducibilité de Girard, les ensembles saturés de Tait, et les interprétations basées sur la biorthogonalité. Dans cet exposé nous comparons ces interprétations par rapport à leur prise en compte de la réécriture et à leur stabilité par union.
Nous commençons par proposer un généralisation de la notion de terme neutre qui permet de définir les candidats de Girard de manière générique. Concernant la stabilité par union, nous rappelons qu'il existe des systèmes de réécriture confluents qui n'admettent pas de famille de réducibilité stable par union. Nous présentons une condition nécessaire et suffisante pour que les candidats de Girard soit stables par union ainsi qu'une condition nécessaire et suffisante pour que la clôture par union d'une famille de biorthogonaux soit un candidat de réducibilité. La seconde condition est strictement plus forte que la première et permet de définir des ensembles saturés de Tait de manière uniforme. De plus, nous montrons que les candidats de Girard sont clos par union pour la réécriture orthogonale basée sur des constructeurs.

Comment la ludique vient au web : une autre lecture d'opérations usuelles [diaporama]

Le web (sous l'angle de sites ou de services) apparaît comme un cadre trivial d'interaction. En définir une interprétation en termes de la ludique de J.-Y. Girard peut se poser, avec l'objectif concret de mieux savoir définir les types associés aux programmes en jeu (donc de leur contrôle). Nous indiquerons comment interpréter le cadre des sites web en termes d'interaction, nous rappellerons comment passer des services web via les processus CCS à des arbres d'actions, puis à une reconstruction des types en ludique. Nous nous attarderons sur quelques éléments spécifiques liant théorie et pratique : non uniformité (bouton back ou reload !), asymétrie (client-serveur).

On propose une nouvelle démonstration, plus simple et avec une meilleure complexité, de la décidabilité de la logique du premier ordre de (omega^{omega^i},+) et de la logique monadique du second ordre de (omega^i,<). Notre algorithme utilise les automates d'arbres et une nouvelle représentation des (ensembles d') ordinaux par des arbres (infinis). On donnera des extensions à certains ordres linéaires dispersés.

Modèles non concrets du lambda-calcul [diaporama]

Les modèles du lambda-calcul pur peuvent être définis soit comme des objets réflexifs dans des catégories Cartésiennes fermées (modèles catégoriques) soit comme des algèbres combinatoires satisfaisant les cinq axiomes de Curry et l'axiome de Meyer-Scott (lambda-modèles). En ce qui concerne les modèles catégoriques, on montre que tout modèle catégorique peut être présenté comme un lambda-modèle, même si la ccc (catégorie Cartésienne fermée) sous-jacente n'a pas assez de points, et on donne des conditions suffisantes pour qu'un modèle catégorique vivant dans une ccc ``cpo-enriched'' arbitraire ait H* pour théorie équationnelle. On construit un modèle catégorique qui vit dans une ccc d'ensembles et relations (sémantique relationnelle) et qui satisfait ces conditions. De plus, on montre que le lambda-modèle associé possède des propriétés algébriques qui le rendent apte à modéliser des extensions non-déterministes du lambda-calcul.

Nous présentons une notion d'automate d'arbres dont l'ambition est d'étudier la décidabilité du fragment multiplicatif et exponentiel de la logique linéaire (MELL). Ces automates, "automates d'arbres d'addition de vecteurs" (VATA) (de Groote, Guillaume, Salvati 2003), peuvent se voir comme une extension pour les arbres des automates d'additions de vecteurs (VAS) qui ont servi à Kosaraju pour démontrer la décidabilité du problème de l'accessibilité dans les réseaux de Petri. Du fait que l'obtention des VATA à partir des VAS est similaire à l'obtention de la notion d'automate d'arbres à partir des automates d'états finis pour les mots, les VATA sont une notion naturelle d'automate. Nous esquisserons la démonstration du fait que le problème de la vacuité du langage d'un VATA est Turing-équivalent à l'existence d'une démonstration pour un séquent de MELL.

Les techniques mises en oeuvre par Kosaraju concernant les VAS ne s'étendent pas immédiatement aux VATA. Cependant les VATA permettent de faire simplement le lien entre la décidabilité de MELL et celles d'autres problèmes. Nous montrerons à titre d'exemple comment les VATA permettent de montrer que la décidabilité des grammaires minimalistes (Stabler 96) est équivalente à celle de MELL.

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.

Autour de la dualité du calcul [diaporama]

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é.

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.

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).

Variétés et espaces algébriques dans le contexte localement ordonné

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.

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.

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.

Faut pas le dire, mais l'enseignement supérieur des sciences (à Nice?), ça marche pas top (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.

Séminaire LOGIQUE ET INTERACTIONS

Archives 2007-2008