Séminaire de l'équipe
Logique, Informatique et Mathématiques Discrètes


Organisateur: Valentin Gledel.

Lien ical.

Damien Regnault, LIP, ENS Lyon. 2:00:00 30 avril 2009 10:15 limd
Minorité stochastique sur les graphes
Abstract

Nous considérons un graphe où les cellules sont caractérisées par un état qui est soit noir, soit blanc. À chaque pas de temps, une cellule, choisie aléatoirement, se met à jour et passe dans l'état minoritaire dans son voisinage. L'évolution globale de ce processus ne semble pas dépendre de la topologie du graphe: dans un premier temps des régions, pavées par des motifs dépendant de la topologie du graphe, se forment rapidement. Puis dans un deuxième temps, les frontières entre ces régions évoluent jusqu'à devenir relativement stables. Nous étudions ce processus sous différentes topologies: arbres, anneaux, grilles, cliques. Ceci nous permet de montrer que même si ce processus se comporte à priori globalement de la même manière sur n'importe quel graphe, modifier la topologie influence la façon dont les régions sont pavées (rayures, damiers), la structure et les mouvements des frontières entre les régions, l'ensemble limite, le temps de relaxation (le temps nécessaire pour que le processus atteigne une configuration de l'ensemble limite). Ainsi, Minorité entraîne des comportements riches et variés qui se révèlent difficile à analyser. Comprendre cette règle simple est néanmoins nécessaire avant de considérer des règles plus compliquées.

Guillaume Theyssier, LAMA. 2:00:00 23 avril 2009 10:15 limd
Sous-shifts et logique monadique du second ordre
Abstract

Les mots (finis ou pas, en dimension 1 ou supérieure) peuvent être vus comme des modèles de formules de la logique monadique du second ordre (MSO), une formule définissant alors un langage. Cette approche a été suivie avec succès en dimension 1 par Büchi et Elgot dans les années 60 : les langages ainsi définis sont exactement les langages rationnels. De plus toute formule MSO est dans ce contexte équivalente à une formule EMSO (quantification existentielle au second ordre suivie d'une formule au premier ordre).
Plus récemment, Giammarresi, Restivo, Seibert et Thomas ont reconsidéré ces résultats dans le cas des figures'', c'est à dire des mots bidimensionnels finis avec bords marqués : cette fois les formules EMSO définissent exactement les langagessofiques'' (projections de langages locaux), mais elles ne suffisent plus à capturer tous les langages définissable par une formule MSO.
L'objectif de cet exposé est de développer cette approche, en dimension 2, pour les sous-shifts (ensembles de configurations fermés topologiquement et invariants par décalages). Nous verrons alors que les sous-shifts sofiques (introduits par Weiss dans les années 70) ne correspondent pas aux sous-shifts définissables par formules EMSO. Nous donnerons néanmoins une caractérisation logique des sous-shifts sofiques et, inversement, nous donnerons une caractérisation ``combinatoire'' des ensembles de configurations définissables dans EMSO.

Antonino Salibra, Venise. 2:00:00 3 avril 2009 08:45 limd
Théories et Modèles du Lambda Calcul
Abstract

Je présente l'approche algébrique au lambda-calcul basée sur les algèbres de lambda abstraction et sur les algèbres de Boole, qui a permis d'étudier la structure du treillis des lambda théories et d'obtenir des résultats d'incomplétude pour le sémantique du lambda calcul. Depuis, je présente mon dernier résultat: la lambda théorie minimum extensionelle n'est pas la théorie d'une domaine de Scott réflexive.

Choco, Ottawa, PPS et LIPN. 2:00:00 2 avril 2009 10:00 limd
Séminaire Choco
Abstract

Voir la page dédiée.

Assia Mahboubi, INRIA/MSR/LIX, Paris. 2:00:00 26 mars 2009 10:15 limd
TBA
Abstract

TBA

Choco, TBA. 2:00:00 12 mars 2009 10:00 limd
Séminaire Choco
Abstract

Voir la page dédiée.

Pierre Clairambault, PPS, Paris 7. 2:00:00 5 mars 2009 11:00 limd
Plus petits et plus grands points fixes en sémantique des jeux
Abstract

On montre comment trouver de façon naturelle des solutions à de nombreuses équations récursives en autorisant des boucles dans les arènes. On équipe ensuite les arènes de fonctions de gain et on s'intéresse aux stratégies totales et gagnantes. On présente alors deux fonctions de gain naturelles sur les arènes à boucles, qui premettent de construire respectivement des algèbres initiales et des coalgèbres finales à de nombreux endofoncteurs continus. Finalement on applique ces constructions pour donner un modèle correct (et complet, en un sens faible) d'un calcul des séquents intuitionniste, étendu par des constructions syntaxiques pour les plus petits et plus grands points fixes.

Alexandre Miquel, LIP, ENS Lyon. 2:00:00 26 février 2009 10:15 limd
Projet Choco, Lisbonne, LSV Cachan, PPS Paris 7. 2:00:00 5 février 2009 10:15 limd
Séminaire Choco
Abstract

Voir la page dédiée.

Joachim Kock, Université de Barcelone. 2:00:00 29 janvier 2009 10:15 limd
Introduction to the theory of polynomial functors
Abstract

After defining polynomial functors and introducing their calculus in terms of certain bridge diagrams, I will survey some examples related to logic: Girard's normal functors, Jay and Cockett's shapely types, the containers of Abbott, Altenkirch and Ghani, multicategories after Lambek, Burroni, and Leinster, and finally trees. (This talk is based on a paper in preparation with Nicola Gambino.)

Christophe Raffalli, LAMA. 2:00:00 22 janvier 2009 10:15 limd
Analyse grammaticale du français : des concepts théoriques ou de la bidoulle ?
Abstract

L'analyse de la langue naturelle est toujours un problème ouvert au sens où il n'a pas à ce jour d'outils disponible resolvant ce problème (qui est pourtant fini si l'on considère que la longueur des phrases est bornées par la plus longue phrase de Proust). Certaines approches reposent sur des concepts théoriques avancés (automates, théorie des types, jusqu'à MELL ou IMELL dans certains articles). Est-ce la bonne approche ? Ou bien juste le fait que l'algorithme est trop complexe pour être écrit à la main ? On va montrer que dypgen (Emmanuel Onzon) permet d'aller assez loin, sans toutefois analyser le présent résumé, en utilisant juste une juxtaposition d'idées au dessus des techniques récentes de parsing pour les grammaires hors contexte. Note: je n'expliquerai pas ce qu'il y a sous le capot de dypgen ... Pour ça, il faudra inviter Emmanuel Onzon.

François de Vieilleville, LAMA. 2:00:00 15 janvier 2009 10:15 limd
Mark Weber, PPS, Paris 7. 2:00:00 18 décembre 2008 10:15 limd
Monads with arities
Abstract

A monad with arities'' is a monad T on some category K together with some extra data expressing the basicshapes'' of the operations involved in the structure of a T-algebra. There is a general result, called the nerve theorem, which in the case where K is a presheaf category, shows that the notion of monad with arities is an efficient reformulation of the notion of limit sketch''. The nerve theorem is so named because it generalises the characterisation of the simplicial sets that arise as nerves of categories. Other interesting instances of this result relevant for higher dimensional algebra involvelocal right adjoint monads'' -- such a T comes with a canonical choice of arities. These examples formalise the passage between the operadic and simplicial approaches to higher category theory.

Geneviève Paquin, LAMA. 2:00:00 11 décembre 2008 10:15 limd
Etude des points fixes sous la fermeture pseudopalindromique itérative
Abstract

Parmi les nombreuses suites remarquables étudiées en combinatoire des mots figurent les suites sturmiennes. Elles interviennent dans plusieurs domaines: dynamique symbolique, géométrie discrète, astronomie, cristallographie, etc. Elles sont d'autant plus remarquables par le fait qu'elles possèdent plusieurs caractérisations équivalentes. Entre autres, elles décrivent les droites discrètes de pentes irrationnelles. Parmi ces droites, la classe des (demies) droites passant par l'origine, appelées des suites sturmiennes standards, admet une caractérisation supplémentaire: il est possible de les construire en utilisant la fermeture palindromique itérative. La fermeture palindromique d'un mot fini w consiste à trouver le mot palindromique le plus court ayant comme préfixe le mot w. La fermeture palindromique itérative d'un mot fini w, noté Pal(w), est définie par Pal(a)=a et Pal(w)=(Pal(w_0...w_{n-1})w_n)^+, où u^+ désigne la fermeture palindromique et a est une lettre de l'alphabet. Ainsi, à tout mot sur un alphabet à 2 lettres, on peut lui associer une suite sturmienne standard en appliquant l'opérateur de fermeture palindromique itérative. Plus récemment, cette notion a été généralisée à des pseudopalindromes, c'est-à-dire des mots restant stables non pas sous l'opération d'image miroir, mais plutôt sous l'action d'un antimorphisme involutif.

D'autre part, certaines suites points fixes sous un opérateur se sont révélées être bien mystérieuses; il suffit de penser au célèbre mot de Kolakoski K=221121221221121122... qui est le point fixe sous l'opérateur de codage par blocs (le mot est égal à ses longueurs de blocs de lettres: 2'' lettres 2,2'' lettres 1, 1'' lettre 2,1'' lettre 1, ...). Plusieurs propriétés combinatoires de ce mot sont encore inconnues: la fréquence des lettres, la récurrence des facteurs, la fermeture de l'ensemble de ses facteurs sous l'image miroir et la complémentation, etc.

Ainsi, avec D. Jamet et G. Richomme, nous nous sommes intéressés à l'étude des points fixes sous l'opérateur de fermeture pseudopalindromique itérative. Dans mon exposé, je vais présenter certains de nos résultats concernant les propriétés combinatoires de ces mots et faisant intervenir entre autres des développements en fractions continues et des morphismes. Je terminerai en proposant certains problèmes ouverts concernant l'algébricité de la ``pente'' de certains de ces points fixes et l'existence d'exposants critiques.

Choco, TBA. 2:00:00 4 décembre 2008 10:00 limd
Séminaire Choco
Abstract

Voir la page dédiée.

Damiano Mazza, LIPN, Villetaneuse. 2:00:00 27 novembre 2008 10:15 limd
Réécriture, catégories d'ordre supérieur, et expressivité des modèles de calcul concurrent
Abstract

Un problème fondamental dans la comparaison de différents modèles du parallélisme et de la concurrence est celui de définir la notion de codage, ou de traduction. A ce jour, parmi toutes les notions universellement acceptées de codage entre modèles concurrents, il n'en existe aucune qui s'impose nettement sur les autres. Nous proposons d'étudier la notion de codage en partant de la vision du calcul comme réécriture, et en utilisant des notions venant de la théorie des catégories d'ordre supérieur et de la théorie des structures d'évenemments de Winskel.

Ugo Dal Lago, Bologne. 2:00:00 20 novembre 2008 10:15 limd
Taming Modal Impredicativity: Superlazy Reduction
Abstract

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.

Luigi Santocanale, LIF, Marseille. 2:00:00 13 novembre 2008 10:15 limd
Outils algébriques pour les logiques modales de point fixe
Abstract

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

Choco, IML, LAMA. 2:00:00 6 novembre 2008 10:00 limd
Séminaire Choco
Abstract

Voir la page dédiée.

Christophe Raffalli, LAMA. 2:00:00 23 octobre 2008 10:15 limd
PML, où en est-on ?
Abstract

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.