Entretien avec Thomas Ehrhard, co-lauréat du Prix Alonzo Church 2024

Cette année, le prix Alonzo Church ¹⁾, a récompensé Thomas Ehrhard, directeur de recherche du CNRS à l'IRIF et Laurent Regnier, professeur à Aix-Marseille Université et membre de l'Institut de Mathématiques de Marseille. Ce prix distingue cinq de leurs articles et reconnait l'importance du travail qu'ils ont mené sur le lambda calcul.
Rencontre avec Thomas Ehrhard, co-lauréat du Prix Alonzo Church 2024 et directeur de recherche à l'IRIF.

Je travaille sur des choses proches de la logique linéaire depuis le début des années 90'. C'est après ma thèse que j'ai commencé à m'intéresser à ce sujet.

Avec Laurent Regnier, co-auteur de quatre des cinq articles récompensés, nous partagions le même bureau à l’I2M (anciennement l'Institut de Mathématiques de Luminy) à Marseille. Un jour, je lui ai raconté que j'avais remarqué qu'il était possible de dériver les lambda-termes syntaxiquement et ça nous a tous les deux convaincus. C'est comme ça que l'on a commencé à travailler ensemble à partir de 2001 jusqu'à la fin 2005 début 2006.

Pour commencer, le lambda-calcul est un formalisme qui est à l'interface de la logique et de l'informatique, dans le sens où il permet à la fois de représenter des preuves ainsi que des programmes. Il est à l'origine de la correspondance de Curry-Howard, qui exprime un lien très étroit entre preuves et programmes.

Ce travail prend naissance dans la sémantique dénotationnelle inventée en 1969, qui permet de donner une représentation mathématique des programmes et des preuves et, en particulier, celles de la logique linéaire qui est née en 1986 grâce à la découverte de Jean-Yves Girard. La sémantique dénotationnelle permet de voir les preuves et des programmes dans un cadre qui relève de ce qu'on appelle l'algèbre linéaire en mathématiques. J'ai donc mené un travail à la fin des années 90' sur des modèles de la logique linéaire, qui sont très proches de cette intuition d'algèbre linéaire où il est devenu naturel de calculer des dérivées de programmes, ce qui n'était pas intuitif jusqu'alors. C'est novateur, car l'opération de dérivation relève de l'analyse, qui est une branche des mathématiques assez éloignée, à priori, de la logique. C'est donc à partir de ce point de vue, mis en place par la logique linéaire, qu'avec Laurent Regnier nous avons eu l’idée d'introduire cette opération de dérivation à l'intérieur du lambda calcul et de la logique linéaire, puisque que ce sont deux formalismes très proches.

Les articles sont tous liés entre eux et développent le sujet à travers différentes perspectives. Ils prennent tous cette idée de dérivation et ils essaient d'en tirer les conséquences exploitables. On est dans un cadre calculatoire vraiment opérationnel, c'est à dire que l'on peut écrire sur un ordinateur. On tente de comprendre ce que veux dire la dérivation, donc la différentiation, qui est une opération relevant plutôt d'un domaine assez éloigné de la programmation, et on réfléchit ce que ça veut dire du point de vue de la programmation.

L'idée de calculer des dérivées de programmes n'est pas complètement neuve, elle était déjà apparue dans les années 80' pour l'analyse numérique. Aujourd’hui, calculer des dérivées de programmes reprend de l’importance, puisque que ça apparaît de façon cruciale en intelligence artificielle, dans le machine learning avec notamment les algorithmes de rétro propagation de gradient (le lien entre cette notion de dérivée de programmes - au sens de l'analyse numérique - et celle que nous avons introduite en logique avec Laurent Regnier est encore assez mystérieux et doit encore être compris). Nous ne sommes pas les inventeurs de cette idée, mais nous l'avons vu apparaître de manière spontanée dans un cadre logique. C’est d'ailleurs ce que j'aime dans la science, que des choses apparaissent et s'imposent naturellement. Il ne s'agit pas d'importer quelque chose d'un domaine A vers un domaine B, il s'agit plutôt de voir les structures qui apparaissent naturellement. Dans la logique linéaire, la dérivation est en quelque sorte apparue de cette manière.

Je travaille toujours sur ces sujets d'étude, je dirige actuellement la thèse d'Aymeric Walch qui travaille sur une nouvelle façon de regarder le sujet.

Ce travail a donné des outils théoriques en théorie de la démonstration. Dans la théorie du lambda-calcul, ça a apporté de nouveaux outils théoriques en particulier pour ce qui est de la théorie de l'approximation finie des preuves et des programmes.
Nous avons pu démontrer de nouveaux résultats et trouver des preuves plus simples de résultats déjà connus. Pour ce qui est des vraies applications en informatique, ça permet essentiellement de donner de nouvelles intuitions en particulier sur la façon dont les programmes interagissent entre eux ou plutôt la façon dont un programme interagit avec son argument, lorsqu'il utilise ce dernier pour produire un résultat.
La sémantique, mon domaine de recherche, reste un sujet assez théorique, qui entretient toutefois des liens étroits avec la conception et l'implémentation des langages de programmation et l'analyse des programmes, du point de vue par exemple de leur complexité. On peut espérer que cette approche différentielle donnera de nouvelles idées dans le développement de langages de programmation.

Ce prix pour moi salue cet effort collectif, pas seulement le travail réalisé avec Laurent Regnier, mais tout le travail de la communauté, composée d'un groupe international de chercheurs, principalement localisés en France, en Italie, au Royaume Uni et au Canada, qui se sont emparés de nos idées pour développer de nouvelles approches et qui ont fait naître des développements.
Ce travail collaboratif intense s'est notamment développé à partir de 2015 dans l'IRN (International Research Network) de logique linéaire dont nous avons pris l'initiative avec mon collègue Lorenzo Totora de Falco de l'Université Roma Tre, dans un groupe de recherche CNRS qui a été renouvelé et qui a duré 8 ans.
Je souhaite également souligner l'importance du travail fondateur de Jean-Yves Girard, qui a apporté les concepts clés à l'origine de ce travail.

–

Les papiers récompensés sont les suivants :

Thomas Ehrhard. “Finiteness spaces”. In: Mathematical Structures in Computer Science 15.4 (2005), pp. 615–646. doi: 10.1017/S0960129504004645

Thomas Ehrhard and Laurent Regnier. “The differential lambda-calculus”. In: Theoretical Computer Science 309.1-3 (2003), pp. 1–41. doi: 10.1016/S0304-3975(03)00392-X

Thomas Ehrhard and Laurent Regnier. “Uniformity and the Taylor expansion of ordinary lambda-terms”. In: Theoretical Computer Science 403.2-3 (2008), pp. 347–372. doi: 10. 1016/j.tcs.2008.06.001

Thomas Ehrhard and Laurent Regnier. “Böhm Trees, Krivine’s Machine and the Taylor Expansion of Lambda-Terms”. In: Logical Approaches to Computational Barriers, Second Conference on Computability in Europe, CiE 2006, Swansea, UK, June 30-July 5, 2006, Proceedings. Ed. by Arnold Beckmann et al. Vol. 3988. Lecture Notes in Computer Science. Springer, 2006, pp. 186–197. doi: 10.1007/11780342_20

Thomas Ehrhard and Laurent Regnier. “Differential interaction nets”. In: Theoretical Computer Science 364.2 (2006), pp. 166–195. doi: 10.1016/j.tcs.2006.08.003