Institut de Mathématiques de Luminy

SÉMINAIRES 2009
Logique et Interactions

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

lundi 23 novembre
à 16h
Luigi Santocanale (LIF, Marseille) :
Le treillis des permutations

Homepage: http://www.lif.univ-mrs.fr/~lsantoca/

Résumé : Rappelons que le groupe des permutations sur n éléments est engendré par des involutions. C'est pour cette raison que son graphe de Cayley est non orienté. Ce graphe admet une orientation canonique si l'on demande qu'une arête augmente la longueur d'une permutation. Le graphe dirigé ainsi obtenu est le diagramme de Hasse d'un ensemble ordonné qui est, en plus, un treillis: tout sous ensemble admet une plus petite borne supérieure et une plus grande borne inférieure.
Dans cet exposé nous allons présenter les propriétés d'ordre de ce treillis, le treillis des permutations sur n éléments. Nous allons d'abord représenter une permutation par son ensemble d'inversions, et puis l'ordre par le relation d'inclusion. Puis, après avoir représenté les permutations sup-irréductibles (et inf-irréductibles), nous aborderons le représentation de ces treillis en tant que treillis de concepts et treillis engendré par sa base canonique.

jeudi 12 novembre
Lionel Vaux (IML, Marseille) :
Points fixes et types de données
dans le modèle relationnel finitaire

Homepage: http://iml.univ-mrs.fr/~vaux/

mardi 27 octobre
Kazushige Terui (Kyoto) :
Cut elimination and algebraic completion
in substructural logics

(Joint work with A. Ciabattoni, N. Galatos and L. Strassburger)
Homepage: http://www.kurims.kyoto-u.ac.jp/~terui/

Abstract: In proof theory, one transforms Hilbert axioms into Gentzen rules to obtain cut-elimination theorems. In algebra, one embeds a given algebra into a complete one for various purposes. It is not surprising that these two are deeply related, since both are concerned with conservative extension. The connection is, however, even tighter than expected. For one thing, the passage from Hilbert axioms to Gentzen rules plays a crucial role for algebraic completion too. For another thing, Maehara-Okada cut-elimination can be construed as generalization of Dedekind-MacNeille completion.
To illustrate the situation, we introduce a hierarchy on nonclassical axioms. One of our goals is then to identify a boundary in the hierarchy, below which proof theory (cut-elimination) works well and above which one finds negative algebraic results (failure of completion).
Besides the general issue, I will also discuss a curious borderline case: logic for compact closed categories with binary products and coproducts. Even though the corresponding variety of lattice-ordered abelian groups is not closed under completions, it has a cut-free hypersequent calculus discovered by Metcalfe, Olivietti and Gabbay. With this example, I will illustrate how our theory works as a heuristic principle for finding a cut-free (hyper)sequent calculus, and also how it might be useful in a categorical setting as well.

jeudi 11 juin
Pierre Clairambault (PPS, Paris 7) :
Plus petits et plus grands points fixes
en sémantique de jeux

Résumé : 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 ensuite deux fonctions de gain naturelles sur les arènes à boucles, qui permettent 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.

mercredi 20 mai
à 10h30
Harry Mairson (Brandeis University, Boston) :
Linear logic and the complexity of control flow analysis
(Travail en commun avec David Van Horn)

Résumé : Static program analysis is about predicting the future: it's what compilers do at compile-time to predict and optimize what happens at run-time. What is the tradeoff between the efficiency and the precision of the computed prediction? Control flow analysis (CFA) is a canonical form of program analysis that answers questions like “can call site X ever call procedure P?” or “can procedure P ever be called with argument A?” Such questions can be answered exactly by Girard's geometry of interaction (GoI), but in the interest of efficiency and time-bounded computation, control flow analysis computes a crude approximation to GoI, possibly including false positives.
Different versions of CFA are parameterized by their sensitivity to calling contexts, as represented by a contour—a sequence of k labels representing these contexts, analogous to Lévy's labelled λ-calculus. CFA with larger contours is designed to make the approximation more precise. A naive calculation shows that 0CFA (i.e. with k=0) can be solved in polynomial time, and kCFA (k>0, a constant) can be solved in exponential time. We show that these bounds are exact: the decision problem for 0CFA is PTIME-hard, and for kCFA is EXPTIME-hard. Each proof depends on fundamental insights about the linearity of programs. In both the linear and nonlinear case, contrasting simulations of the linear logic exponential are used in the analysis. The key idea is to take the approximation mechanism inherent in CFA, and exploit its crudeness to do real computation.

à 14h
Phil Scott (University of Ottawa) :
Towards a typed Geometry of Interaction

Résumé : In this talk I will survey some of the work in the past few years by Esfan Haghverdi and me on categorical/algebraic modellings of early GoI (GoI I and II) for multiplicative and exponential linear logic. These are based on traced monoidal categories with a reflexive object (to handle the execution formula), satisfying various algebraic equations. The original GoI has further structure: the categories are enriched (the homsets have sigma-additive structure) along with abstract notions of orthogonalities. More recently, we have moved away from the untyped reflexive object, to a typed version of GoI, based on a new notion of partially traced category, with an appropriate orthogonality theory. This leads to new classes of models of GoI. We shall illustrate with many concrete examples.

vendredi 17 avril
à 11h
Simon Perdrix (PPS, Paris 7 + LFCS, Edinburg) :
États graphes quantiques
et la nécessité de la décomposition d'Euler

Résumé : Poursuivant le programme initié par Abramsky et Coecke, Coecke et Duncan ont introduit un formalisme catégorique pour les observables quantiques complémentaires. Nous utilisons leur langage diagrammatique pour étudier le formalisme des états graphes, une sous classe importante d'états quantiques. Nous introduisons une nouvelle équation correspondant à la décomposition d'Euler de la transformation d'Hadamard, et nous montrons que l'une des principales propriétés de ce formalisme, le théorème de Van den Nest — les graphes localement équivalents représentent la même intrication — est équivalent à cette nouvelle équation. Enfin nous montrons que cette décomposition d'Euler ne peut être dérivée à partir des axiomes existants. Ce résultat permet de raffiner le langage introduit par Coecke et Duncan et de mettre en évidence une structure fondamentale de l'intrication.

jeudi 16 avril
Lionel Nguyen Van Thé (Neuchâtel) :
Espaces métriques ultrahomogènes,
partitions et dynamique

Résumé : Existe-t-il un espace métrique séparable dans lequel tout espace métrique séparable se plonge de manière isométrique? La réponse à cette question, posée par Fréchet durant l'enfance de la géométrie métrique, date de 1925, grâce à la construction par Paul Urysohn de l'espace qui porte désormais son nom. Longtemps oublié, cet objet est devenu, depuis quelques années, un sujet actif de recherche. Le but de cet exposé est de présenter quelques résultats qui lui sont relatifs. On s'intéressera notamment au comportement combinatoire qu'il adopte lorsqu'on le soumet à un coloriage fini (propriétés de Ramsey), ainsi qu'aux propriétés de point fixe que sa structure induit sur certaines actions de groupes topologiques.

jeudi 9 avril
Yves Guiraud (Loria, Nancy), avec Philippe Malbos (Lyon 1) :
n-catégories de type de dérivation fini

jeudi 26 mars
à 14h, sur le grand escalier de la gare St Charles
Rémi Morin (LIF, Univ. Aix-Marseille 1) :
Systèmes à mémoires partagées: une question ouverte

Résumé: Nous introduirons un modèle simple de systèmes à mémoires partagées, à base d'automates, ainsi que la description formelle de leur exécutions sous forme d'ordres partiels.
Après l'exposé de résultats récents qui généralisent le théorème de Buchi reliant regularité et logique monadique dans ce cadre, nous présenterons une question liée à la caractérisation des langages reconnus par ces systèmes.

vendredi 20 mars
Beniamino Accattoli (Univ. La Sapienza, Rome) :
Jumping boxes - representing λ-calculus boxes
with jumps (and consequences on linear logic)

Abstract: Boxes are a key tool introduced by linear logic proof nets to implement lambda-calculus beta-reduction. In usual graph reduction instead there is no need of boxes: the part of a shared graph that may copied or erased is reconstructed on the fly when needed. Boxes play however a key role in controlling the reductions of nets and in the correspondence between nets and terms with explicit substitutions.
We show that boxes can be represented in a simple and efficient way by adding a jump, i.e. an extra connection, for every explicit sharing position (exponential cut) in the graph. The nets obtained in this way are connected and can be characterized by a variant of the correctness criterion proposed by Lamarche for essential nets. The direct correspondence between explicit substitutions and jumps simplifies and clarifies the already known correspondence between explicit substitutions and proof net exponential cuts, and suggests a new useful and powerful framework for designing and proving properties of new calculi for explicit substitutions.

mercredi 11 mars
à 10h30

Michel Hirschowitz (CEA, Saclay) :
Contraction-free proofs and games for linear logic

Abstract: In the standard sequent presentations of Girard’s Linear Logic (LL), there are two ”non-decreasing” rules, where the premises are not smaller than the conclusion, namely the cut and the contraction rules. It is a universal concern to eliminate the cut rule. We show that, using an admissible modification of the tensor rule, contractions can be eliminated, and that cuts can be simultaneously limited to a single initial occurrence. This view leads us to a neutral (in the sense of Delande-Miller) game model for LL with exponentials, where each play is finite. This game yields a notion of validity which is consistent and sound w.r.t. LL provability.

jeudi 26 février
Samuel Mimram (PPS, Paris 7) :
Une sémantique de jeux asynchrones
pour la logique linéaire

Résumé : La sémantique des jeux a été introduite afin de caractériser le comportement interactif des preuves et des programmes. Dans ce type de sémantique, un programme est vu comme une stratégie décrivant la façon dont il va réagir aux informations fournies par son environnement. Habituellement, les stratégies considérées en sémantique des jeux sont alternées : les deux protagonistes jouent chacun à leur tour. Cette propriété n'est plus désirable pour des programmes utilisant des constructions concurrentes, car les interactions ne peuvent plus être synchronisées (et en particulier les preuves de MLL décrivent de tels comportements). L'extension des notions fondamentales de sémantique des jeux à un cadre non-alterné n'est pas directe et nous a demandé de repenser en profondeur la définition des stratégies. Je montrerai comment les sémantiques de jeux asynchrones permettent de réaliser cette tâche et ainsi d'élaborer un modèle de logique linéaire dans lequel on peut reconstruire de nombreux modèles préexistants.

jeudi 12 février
Yves Lafont (IML) :
Homotopie en dimension supérieure

vendredi 30 janvier
Marie-Renée Fleury-Donnadieu (IML) :
La Ludique, cadre pertinent pour la formalisation des interactions dialogiques, des actes de langage,...

 

EL, le 22 novembre 2009