Bienvenue sur le site du projet ANR Logoi!
Présentation
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 d'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é.