****************************************************** * Journées de l'ANR INVAL * Invariants algébriques des systèmes informatiques * ****************************************************** Lieu : Université de Lyon 1, Bâtiment Braconnier, Campus de la Doua, salle Fokko du Cloux (1er étage) ****Jeudi 25 septembre 8h30 - Accueil en salle Fokko du Cloux 9h - 9h45 Philippe Gaucher (PPS - Université Paris 7) Combinatoire des étiquetages des automates parallèles 10h15 - 11h Sanjeevi Krishnan (CEA-Ecole Polytechnique) Directed topology and rewriting 11h30 - 12h15 François Lamarche (INRIA Lorraine) Homotopie par chemins dans les catégories et les d-catégories Repas 14h30 - 15h15 Timothy Porter (University of Wales, Bangor) OPLUS: la somme des ordinaux et ses applications. 15h30 - 16h Tom Hirschowitz (Université de Savoie) Un jeu graphique pour MALL 16h30 - 17h15 Paul-André Mellies (PPS - Université Paris 7) Enriched groupoids and logical duality 17h30 - 18h Samuel Mimram (PPS - Université Paris 7) Présentation d'une sémantique de jeux pour la quantification du premier ordre ****Vendredi 26 septembre 9h - 9h45 Jean-Louis Loday (CNRS, Strasbourg) La théorie des opérades 10h15 - 11h Guillaume Bonfante (INRIA Lorraine) Complexité implicite des calculs: un cas d'étude, les interprétations polynomiales sur les termes 11h30 - 12h15 Yves Guiraud (INRIA Lorraine) Complexité des programmes polygraphiques (avec G. Bonfante) Repas 14h - 14h45 Jean-Louis Loday La théorie des opérades 15h - 15h45 Yves Guiraud n-Catégories de type de dérivation fini (avec P. Malbos) 16h - 16h45 Nicolas Tabareau (PPS - Université Paris 7) Calcul de modèles libres sur des théories T-algébriques ***************************************************** Résumés : ********** Guillaume Bonfante Complexité implicite des calculs: un cas d'étude, les interprétations polynomiales sur les termes La complexité implicite des calculs vise à établir des caractérisations des classes de complexité en évitant la notion de machine. Dans les dernières années, un foisonnement de résultats a montré que la terminaison était un outil très riche dans ce domaine. Nous brossons un tableau de la situation dans le cadre des systèmes de réécriture avec les interprétations polynomiales. ********** Philippe Gaucher Combinatoire des étiquetages des automates parallèles Je vais parler des phénomènes combinatoires sous-jacents à l'étiquetage des transitions de haute dimension dans les automates parallèles. ********** Yves Guiraud Complexité des programmes polygraphiques (avec G. Bonfante) Les programmes (3-)polygraphiques sont une généralisation des programmes fonctionnels du premier ordre, une variété de systèmes de réécriture de termes. Ils forment un modèle de calcul Turing-complet. En se basant sur la structure de 3-catégorie, on peut utiliser des dérivations pour prouver leur terminaison et obtenir des bornes de complexité, dans le même esprit que les interprétations polynomiales de termes. En particulier, on obtient une nouvelle caractérisation de la classe FPTIME (celle des fonctions calculables en temps polynomial par une machine de Turing déterministe). ********** Yves Guiraud n-Catégories de type de dérivation fini (avec P. Malbos) La propriété de type de dérivation fini (TDF) a été introduite par Craig Squier pour les présentations de monoïdes (ou systèmes de réécriture de mots), que nous verrons comme des 2-polygraphes. C'est un invariant de nature homotopique du monoïde présenté (resp. de la 2-catégorie présentée) : il correspond au caractère finitaire du nombre de « trous » de l'espace de réduction, c'est-à-dire de choix effectués au cours du calcul. Squier a montré que, si le 2-polygraphe est fini et convergent, alors il est TDF. Le cas des 3-polygraphes (et au-delà) a un intérêt puisqu'il contient les systèmes de réécriture de termes. Au vu des exemples de tels objets, la généralisation du résultat de Squier aux dimensions supérieures était une question ouverte. Nous montrerons un contre-exemple naturel : un 3-polygraphe fini et convergent mais qui n'a pas la propriété TDF. ********** François Lamarche Homotopie par chemins dans les catégories et les d-catégories Il y a déjà quelque temps j'ai parlé de la possibilité de définir l'homotopie dans Cat au moyen d'un endofoncteur des chemins, comme on fait dans les espaces de Kelley. Ce foncteur n'est pas uniquement défini. J'en ai maintenant quatre versions, qui donnent lieu au même théorème fondamental sur le groupoïde universel. Un en particulier semble avoir les meilleures propriétés du point de vue pratique. Ils ouvrent la possibilité de donner une définitions *élémentaire* d'équivalence faible de catégories. Cette technologie peut être adaptée à l'homotopie dirigée, pour laquelle je définis le concept de d-catégorie. Le choix du terme provient du fait qu'il semble s'agir de la version combinatoire des d-spaces définis par Marco Grandis et améliorés par Fajstrup-Rosicky. La catégorie des d-catégories est complète et co-complète. Elle est aussi équipée d'un foncteur de réalisation géométrique. Comme je crois que c'est le le cas avec les travaux récents de Grandis, le foncteur des chemins dirigés est un endofoncteur, ce qui permet d'itérer et de définir l'espace cubique de l'homotopie d'ordre supérieure. ********** Jean-Louis Loday La théorie des opérades La notion d'algèbre, originellement algèbre associative, se décline suivant plusieurs types: algèbre de Lie, de Poisson, dendriforme. Chacun de ces types est géré par une opérade. De meme, la notion d'opérade, originellement opérade symétrique, se décline suivant plusieurs types: opérade non symétrique, permutade, propérade, opérade modulaire, etc. Chacun de ces types est géré par une computade, et ca continue ? ********** Nicolas Tabareau (PPS - Université Paris 7) Calcul de modèles libres sur des théories T-algébriques Un des points clés de la sémantique catégorique de Lawvere est que toute théorie algébrique (monoïde, algèbre de Lie) induit une construction libre (monoïde libre algèbre de Lie libre) calculée par extension de Kan. Malheureusement, ce principe ne marche plus lorsque qu'on considère des variantes linéaires des théories algèbriques, comme les PROs, les PROPs ou les PROBs. Nous allons étudier la notion de T-théorie algébrique enrichie, pour une pseudomonade T -- une légère généralisation des doctrines équationelles -- afin de décrire différents types de "theories T-algébriques" et opérades enrichies. Ensuite nous formulons deux conditions (la première combinatoire, la seconde algébrique) qui assure que le modèle libre d'une théorie T-algébrique existe et est calculé par une extension de Kan enrichie. Ces conditions sont axiomatisées le cadre des équipements en distributeurs, c'est à dire une bicatégorie dont certains morphismes ont des adjoints à droite dont l'exemple principal est la bicatégorie des distributeurs de Bénabou. Nous montrerons en fin d'exposé comment notre approche permet d'appréhender autrement le travail de Vallette sur les monoïdes libres (et sa récente reformulation par Lack). Enfin nous montrerons comment appliquer notre théorie pour calculer des exponentielles libres dans les espaces de cohérence et les jeux de Conway.