École Jeunes Chercheurs En Informatique Mathématique 2008

Le programme de Géométrie de l'Interaction (GdI) visait à construire une interprétation satisfaisante sur le plan mathématique de la dynamique des programmes. Ce programme a connu une première (et inattendue) réalisation en 1988 avec l'interprétation des preuves/programmes par des isométries partielles sur l'espace de Hilbert, et celle de la dynamique au travers de la formule d'exécution qui exprime la solution d'une équation de rétroaction.

Dans les trois niveaux fondationnels de la logique:

• 1. les formules ou niveau de vérité, prouvabilité, cohérence....
• 2. les preuves ou niveau de la fonctionnalité (catégories),
• 3. la dynamique ou niveau de l'élimination des coupures

la GdI se place au plus profond, au niveau 3. D'où la question de l'articulation avec les niveaux plus traditionnels ; ainsi, comment définir la vérité en GdI?

La première GdI était muette à ce sujet. La seconde GdI s'approche davantage de l'esprit des algèbres d'opérateurs (algèbres stellaires et de von Neumann), de façon à analyser

• 1. la vérité;
• 2. l'infini (ou encore : la pérennité, i.e., les exponentielles de la logique linéaire);
• 3. la complexité algorithmique.

Ils semblent que ces trois aspects de la logique (et du calcul) dérivent d'une racine commune, la notion de point de vue, qui s'inspire de celle de mesure en mécanique quantique.

La sophistication des algèbres d'opérateurs devrait à terme induire un renouveau méthodologique dans le domaine ; telle est du moins l'ambition avouée du projet de la GdI.

Références : le Point Aveugle en général; plus particulièrement le tome II, chapitres 18-21 et aussi le cours de Tende (la partie II sera écrite dans qq mois).

Ce cours est une introduction à la théorie de Squier sur les invariants algébriques de la réécriture.

Bibliographie : Y. Lafont, Algebra and Geometry of Rewriting, à paraître dans Applied Categorical Structures

La complexité calculatoire implicite a pour objet le calcul à ressources bornées (temps, espace). Il s'agit d'étudier dans le cadre d'un calcul général (lambda-calcul, réécriture) des disciplines de programmation permettant de garantir statiquement et formellement que sur toute entrée, le programme terminera avec une certaine borne en temps ou en espace. L'exemple le plus classique est celui des programmes terminant en temps polynomial (Ptime), et cette branche de recherche s'est développée notamment à partir des travaux de Leivant, Bellantoni et Cook, Jones, Girard...

Dans ce cours nous présenterons les principales approches en complexité implicite, essentiellement pour la caractérisation de la classe Ptime, en présentant leurs fondements théoriques puis les différents critères d'analyse de programmes qu'ils permettent de définir :

• d'une part l'approche basée sur un bridage des structures de contrôle (récursion): récursion primitive ramifiée et quasi-interprétations pour la réécriture;
• d'autre part celle dérivée de la logique linéaire visant à contrôler la réutilisation de ressources: logiques linéaires light et systèmes de types pour la complexité en lambda-calcul.

Pavages, de l'apériodicité à l'indécidabilité (2h, Nicolas Ollinger)

les jeux de tuiles et les pavages du plan ; la problématique de l'apériodicité (Wang et Berger) ; construction d'un pavage apériodique (Robinson, substitution et auto-similarités) ; calculer dans des pavages, indécidabilités ; application à la dynamique des AC.

Pavages et logique (1h, Emmanuel Jeandel)

pavage comme théorie logique finie ; quasipériodicité et théories complètes ; retour aux théories logiques et au problème de décision de Hilbert ; classes syntaxiques de la logique du premier ordre ; frontière décidabilité/indécidabilité.

Complexité de Kolmogorov et logique (1h, Gregory Lafitte)

premiers éléments de complexité de Kolmogorov ; preuves élémentaires: exemple du Castor affairé ; incomplétude de Gödel à la Chaitin ; retour sur la complexité structurelle des pavages.

Le but de ce cours est de donner un aperçu de ce que nous pouvons apprendre en exploitant les structures algébriques des objets combinatoires. Les séries génératrices peuvent par exemple nous aider à les dénombrer (combinatoire énumérative). Une autre application possible est la génération aléatoire efficaces d'objets combinatoires, comme les graphes. Elle peut être utilisée dans des algorithmes probabilistes sur ces structures.