La structure fine des systèmes formels de démonstration et leurs interprétations calculatoires – FISP

Le projet FISP s'inscrit dans la prolongation du projet STRUCTURAL (2011-2013), qui avait pour objectif général d'étudier la structure des systèmes formels de démonstration et les interprétations calculatoires associées. Il se concentre sur le développement des axes de recherches qui se sont révélés les plus fructueux dans le projet STRUCTURAL : l'inférence profonde, le epsilon-calcul Hilbert et les formules de Herbrand. Il a pour objectif premier la construction de nouvelles interprétations calculatoires des preuves basées sur ces techniques.

Le projet est mené par un consortium de quatre équipes, deux Françaises et deux Autrichiennes, toutes reconnues internationalement pour leurs travaux en théorie de la démonstration structurelle, mais représentant deux traditions différentes de la théorie de la démonstration. D'une part, il y a une tradition venant des mathématiques, qui s'intéresse principalement à la logique du premier ordre et étudie par exemple, le théorème de Herband, le epsilon-calcul de Hilbert et l'interprétation Dialectica de Gödel. D'autre part, il y a une tradition tournée vers l'informatique, qui s'occupe s'occupe principalement de systèmes propositionnels et étudie par exemple, l'isomorphisme de Curry-Howard, les sémantiques algébriques, la logique linéaire, les réseaux de preuves et l'inférence profonde. Le socle commun de ces deux traditions est le rôle primordial joué par les preuves analytiques et la notion d'élimination des coupures.

Le projet FISP fait partie d'un projet à long terme ambitieux dont l'objectif est d'appliquer des techniques puissantes et prometteuses de la théorie de la démonstration structurelle -- en particulier, l'inférence profonde, le epsilon-calcul Hilbert et les formules de Herbrand -- à des problèmes relevant de l'informatique pour lesquels ils n'ont pas été utilisés auparavant : en particulier le contenu calculatoires des preuves, l'extraction de programmes à partir de preuves et le contrôle au niveau logique d'opérations calculatoires sophistiquées. Jusqu'ici, la plupart des travaux réalisés dans le domaine des interprétations calculatoires des systèmes logiques sont basés sur le travail fondateur de Gentzen, qui au milieu des années trente, a introduit le calcul des séquents, la déduction naturelle et la procédure d'élimination des coupures. Mais cette approche a montré ses limites quand il s'agit de l'interprétation calculatoire de la logique classique ou de la modélisation du calcul parallèle. Le but de ce projet, basé sur la complémentarité des compétences des différentes équipes, est de dépasser ces limites en utilisant les techniques mentionnées précédemment. Par exemple, l'inférence profonde possède des propriétés que les systèmes habituels de déduction ne possèdent pas, à savoir la symétrie complète et l'atomicité, qui ouvrent de nouvelles possibilités au niveau calculatoire,

Le projet STRUCTURAL a montré que l'approche choisie et les directions de recherche retenues étaient appropriées et l'expertise combinée des équipes a permis de faire des progrès remarquables dans les trois thèmes retenus pour le projet FISP, qui ouvrent de nouveaux champs de recherche d'intérêt majeur. Il a été démontré, par exemple, que les interprétations calculatoires de l'inférence profonde peuvent fournir un typage adéquat du lambda- calcul avec partage explicite ainsi que des réseaux d'interaction. Il a également été démontré que, de façon surprenante, le non-déterminisme des interprétations calculatoires de la logique classique peut être contrôlé par des formules de Herbrand.

Ces résultats montrent le potentiel considérable et la pertinence des techniques retenues. L'objectif du projet FISP sera à la fois de continuer le développement théorique de ces techniques et d'en donner de nouvelles applications en terme de modélisation logiques des opérations calculatoires. La modélisation logique des machines abstraites et des calculs parallèle et distribué constitueront des cibles privilégiées.