Rencontre du projet ANR
Invariants algébriques des systèmes informatiques


Strasbourg, 9 novembre 2006
à l' Institut de Recherche Mathématique Avancée


Cette rencontre est associée à la conférence Operads 2006 .

Programme

9h30-10h Accueil des participants
10h-11h Eric Goubault (CEA - Saclay),
      Static Analysis of Concurrent Programs: A Geometric Approach, and Perspectives
11h-11h30 Pause
11h30-12h30 Albert Burroni (Université Paris 7),
      Algèbres graphiques et leur réécriture
12h30-14h Pause déjeuner
14h-15h François Métayer (PPS - Université Paris 7),
      n-catégories libres et cofibrantes
15h10-16h10 Yves Lafont (Institut de Mathématiques de Luminy - Université de la Méditerranée),
      Opérades et réécriture
16h10-16h40 Pause
16h40-17h40 Philippe Malbos (Institut Camille Jordan - Université Lyon 1),
      Les deux conditions de convergence de Squier
17h40 - Discussion sur le futur du réseau.
          - Finalisation du projet éditorial (discussion animée par Y. Lafont).

Résumés

Algèbres graphiques et leur réécriture (Albert Burroni)

La réécriture est le prototype de toute forme de calcul. Dans un article de 1993, nous avons montré qu'une notion générale de réécriture en dimensions supérieures couvre des types de calculs comme la réécriture de mots et la réécriture de termes (qui relèvent respectivement des dimensions 1 et 2). Un autre exemple en dimension 2, qui en fait est lié au précédent (dans les deux cas il s'agit de calcul en logique équationnelle), est le calcul fait dans les catégories cartésiennes. On peut résumer la nature de ces réécritures comme une manière combinatoire d'aborder les problèmes de présentations de catégories en dimensions supérieures. (c'est à dire les notions qui sont l'analogue dans le cas de la réécriture de mots --- présentation des -- --monoïdes --- des notions de « générateurs et relations »).
Mais ces réécritures ne couvrent pas toutes les formes de calculs classiques. Par exemple, les calculs de la logique qui, en plus des connecteurs, s'expriment avec des quantificateurs. Par exemple encore, les calculs de la logique linéaire ou encore ceux effectués en lambda-calcul. Ce dernier cas, exprimé sous la forme de calcul dans les catégories cartésiennes fermées (donc en ne se limitant plus au seul aspect cartésien) est typique de ces calculs qui relèvent d'une forme plus riche de réécritures, quelques fois apparues dans la littérature sous la forme vague de réécriture conditionnelle (une réécriture est permise sous conditions).
Pour comprendre la nature de ces nouvelles réécritures, reprenons l'analyse du cas de la réécriture en dimension 2. Plus précisément, la réécriture de termes. En fait, une autre manière de dire les choses est de dire qu'il s'agit du calcul de T-algèbres où T est une monade (monade de rang finitaire) sur la catégorie des ensembles.
La réécriture que nous proposons comme cadre général des cas cités ci-dessus et qui sont non couvert par la réécriture en dimensions supérieures (du moins telle qu'elle a été caractérisée ci-dessus), est un calcul dans les T-algèbres où T est cette fois une monade sur la catégorie des graphes. A ces T-algèbres nous avons donné le nom générique d'« algèbres graphiques » (en écho à l'expression « algèbres ensemblistes », plus familièrement connues sous le nom d'« algèbres universelles » [sic]). Ces calculs sont ceux qui prennent la forme de réécriture de diagrammes.
La catégorie des graphes est particulièrement adaptées pour des calculs finitaires (il est facile de montrer que ce ne serait pas le cas pour une catégorie comme, par exemple, la catégorie des catégories), d'autant que dans la quasi totalité des cas intéressants, ces monades graphiques T sont finitaires.

Static Analysis of Concurrent Programs: A Geometric Approach, and Perspectives (Eric Goubault)

Dans cet expose, je vais montrer ce qui, de la théorie de l'homotopie dirigée, a été pour l'instant utilisé en pratique, dans un analyseur statique de code (ALCOOL), à des fins de validation automatique de programmes. Je terminerai mon exposé en montrant ce qu'on souhaiterait avoir comme résultats nouveaux, qui permettraient à l'analyseur actuel d'être encore bien meilleur.

Opérades et réécriture (Yves Lafont)

Nous proposons d'utiliser la syntaxe "graphique" et les méthodes de la réécriture, notamment le calcul des paires critiques, pour étudier les algèbres de Hopf et les bigèbres généralisées au sens de Loday.

Les deux conditions de convergence de Squier (Philippe Malbos)

Des conditions de finitude homologique et homotopique pour l'existence de présentations convergentes et finies de monoïdes furent introduites par Squier. Je présente une approche permettant d'unifier ces deux conditions de finitude.

n-catégories libres et cofibrantes (François Métayer)

Nous définissons une notion de cofibration pour les n-catégories : les objets cofibrants sont alors exactement les n-catégories librement engendrées par un polygraphe.