Blanc SIMI 2 - Sciences de l'information, de la matière et de l'ingénierie : Sciences de l’information, simulation

Logique et géometrie de l'interaction – LOGOI

Logique et Géométrie de l'Interaction

La logique de l'interaction et la nature du calcul

Preuves et programmes nécessitent de nouvelles fondations, centrées sur l'interaction

Le projet LOGOI se situe à l'interface entre la logique mathématique et l'informatique. Le rôle de la théorie de la démonstration dans les fondements théoriques des langages de programmation est indéniable, de même que son utilisé pour développer des outils mathématiques d'analyse des programmes. En particulier, la correspondance de Curry-Howard, qui identifie les preuves mathématiques aux programmes informatiques et la normalisation des preuves à l'exécution des programmes, a joué un rôle clé dans cette interface. <br />L'évolution de la place du calcul met en évidence de nouvelles problématiques/questions comme la coopération entre agents, l'échange de données entre processus, le partage de ressources, toutes situations où l'interaction joue un rôle de premier plan, sans oublier le développement de nouveaux paradigmes calculatoires, comme le calcul quantique. <br />Cette évolution nous confronte à une nouvelle situation : de nouveaux concepts et méthodes doivent être élaborés et la théorie de la démonstration doit s'adapter. <br /> <br />Dans ce cadre, le rôle central de l'interaction est fondamental. C'est pour cette raison que la base de LOGOI était la géométrie de l'interaction, qui trouve sa source dans la théorie de la démonstration de la logique linéaire et qui a vu d'importantes avancées ces dernières années. <br />Le coeur de la géométrie de l'interaction est une interprétation dynamique de la logique et du calcul : les processus (ou preuves, via Curry-Howard) sont définis par leur comportement interactif ce qui est particulièrement bien adapté à une analyse de comment le calcul s'exécute en prenant en compte les aspects procéduraux du calcul de même que le temps d'exécution. En outre, son fondement mathématique est la théorie des algèbres d'opérateurs qui dessine/ouvre des connexions fascinantes avec la physique quantique.

L'hypothèse de travail qui sous-tend notre projet est que la théorie de la démonstration et l'informatique peuvent trouver de nouveaux fondements mathématiques empruntant à divers champs mathématiques : de l'analyse et la géométrie à la théorie de la mesure qui ont été des sujets d'intense développements des mathématiques contemporaines, à tel point que le point du vue sur ces domaines a radicalement changé. Les développements récents en géométrie de l'interaction ont rendu cela possible et nous ont servi de base de travail.
Nous espérions/escomptions tout particulièrement de nouveaux apports en théorie de la complexité. Les nombreuses approches de la complexité calculatoire existantes manquent fondamentalement de structure : la théorie de la complexité est jusqu'ici restée essentiellement une collection de techniques ad hoc chacune utile pour un type de problèmes particulier mais sans intérêt pour d'autres questions. La quasi-totalité des caractérisations disponibles sont de nature existentielle (l'appartenance à une certaine classe est caractérisée par l'existence d'un algorithme ou d'une machine tel que…) et non pas universelle.
Un autre objectif majeur de nos recherches consistait à ouvrir la voie à une théorie de l'expressivité des langages de programmation où l'on s'intéresse non pas à ce qui est calculé mais à comment le calcul est effectué.

Toutes ces lignes ont le potentiel de conduire à des applications intéressantes.

Nos travaux ont conduit à renouveler la syntaxe des preuves et à des avancées dans le fondement d'une théorie de l'interaction. L'un des résultats principaux est l'émergence d'une approche radicalement nouvelle de la complexité où les outils et méthodes viennet de la géométrie de l'interaction et de son interprétation dans les algèbres d'opérateurs. Nous avons ainsi gagné de nouvelles intuitions sur l'expressivité des langages de programmation et des modèles calculatoire.
Nos applications concernent notamment des champs de recherches très actif, comme le calcul quantique, la concurrence ou le calcul parallèle.

Parmi les succès de LOGOI, nous soulignons particulièrement :
implication élevée d'étudiants : le projet a directement impliqué 20 doctorants et plusieurs stagiaires de M2. Neuf thèses réalisées dans le cadre du projet ont déjà été soutenues.
dissémination et visibilité: deux écoles et plusieurs workshops ont été organisés.
réseau de collaboration internationales riche et dynamique.

`Les avancées importantes obtenues dans toutes les tâches du projet constituent les bases d'une approche vraiment nouvelle. En outre, un réseau de chercheurs s'est consolidé autour de cette approche, autour duquel nous avons la ferme intention de construire de nouveaux projets. '

Publications (référées ): 44 , dont 25% multi-paretenaires

Revues Internationales: 15
Actes de conférences internationales: 28
Actes de conférences nationales: 1

Thèses de doctorat : 9

Le projet LOGOI se situe à l’interface de la logique mathématique et de l’informatique théorique ; plus précisément en Théorie de la
Démonstration, branche de la Logique Mathématique qui s'occupe des propriétés des langages, mathématiques ou informatiques. C'est donc un cadre on ne peut plus naturel pour l'étude des langages de programmation.
L’évolution de la théorie du calcul et de la programmation (coopération entre agents, échange de données, ressources partagées, calcul quantique ...) demande un renouvellement fondamental de la Théorie de la Démonstration ; il faut, en effet, élaborer les concepts permettant de répondre aux nouveaux défis. 
La Théorie de la Démonstration propose et oppose, traditionnellement, deux paradigmes de calcul basé sur les démonstrations : 
- D'une part, les Preuves comme Programmes (popularisé sous le nom d'isomorphisme de Curry Howard), où l'on calcule par explicitation (normalisation, élimination des coupures) d'une démonstration donnée à l'avance. 
- D'autre part, les Preuves comme Recherche (popularisé par la programmation logique et le langage PROLOG), où l'on calcule en cherchant à démontrer une formule donnée à l'avance. 
La Logique Linéaire, en autonomisant la dynamique logique (i.e., les calculs sous-jacents) permet de réconcilier ces deux paradigmes --- pourtant réputés incompatibles et antagonistes --- sur la base d'une approche interactive qui englobe démonstrations, programmes et instructions de contrôle dans une même catégorie de processus.
Cette unification se fait en Géométrie de l'Interaction (et aussi en Ludique, paradigme voisin issu de la même Logique Linéaire). Comme le suggère le nom, les processus (= preuves, programmes, contraintes) sont définis relativement à leur comportement vis à vis de l’ interaction. Ce cadre conceptuel nous semble ainsi particulièrement propice à l'analyse de la procéduralité du calcul : il devrait amener des réponses appropriées aux défis actuels représentés par la complexité algorithmique, le calcul quantique et la théorie de la concurrence.
Au niveau logique proprement dit, l’approche dynamique de la Géométrie de l’Interaction, si elle rend bien compte de la procéduralité et du temps de l’exécution des programmes, concerne également la notion de vérité, qui perd son caractère absolu, primitif (et pléonasmatique), pour prendre une valeur interactive, contextuelle... En accord de principe avec la "philosophie" de la mécanique quantique, un accord de principe renforcé par l'utilisation des algèbres de von Neumann (le facteur hyperfini dans la plus récente version de la Géométrie de l'Interaction).
Nous espérons trouver dans les algèbres d'opérateurs le cadre approprié permettant de dépasser les limitations théoriques du langage usuel (trop circonscrit au monde combinatoire) pour comprendre le "moteur" qui anime la complexité algorithmique, i.e., la différence entre question et réponse, trouvaille et vérification. Techniquement, cela veut dire mener à maturité l'étude des concepts novateurs introduits en Logique Linéaire : typiquement, les exponentielles allégées emblématiques de ce nouveau regard logique sur la complexité algorithmique, sans oublier les autres artefacts novateurs de la Logique Linéaire, réseaux de démonstrations ou Ludique, qui sont plus que jamais d'actualité.

Coordinateur du projet

Madame Claudia FAGGIAN (UNIVERSITE DE PARIS VII [DENIS DIDEROT]) – faggian@pps.jussieu.fr

L'auteur de ce résumé est le coordinateur du projet, qui est responsable du contenu de ce résumé. L'ANR décline par conséquent toute responsabilité quant à son contenu.

Partenaire

PPS UNIVERSITE DE PARIS VII [DENIS DIDEROT]
LIPN UNIVERSITE DE PARIS XIII
IML CNRS - DELEGATION REGIONALE PROVENCE ET CORSE

Aide de l'ANR 396 406 euros
Début et durée du projet scientifique : - 48 Mois

Liens utiles