Thomas Ehrhard et Laurent Regnier honorés pour leurs travaux novateurs sur le lambda-calcul différentiel

Au début des années 2000, Thomas Ehrhard et Laurent Regnier sont tous deux membres de l’équipe de logique créée par Jean-Yves Girard, fondateur de la logique linéaire et directeur de recherche CNRS à l’I2M. Ils partagent alors un bureau à l'Institut de mathématiques de Luminy à Marseille (désormais I2M). Un matin, le premier présente à son collègue une idée originale. Et s’il était possible de dériver syntaxiquement les termes du lambda-calcul ? Ce langage formel permet de manipuler des fonctions et des programmes comme des objets mathématiques. Inventé dans les années 1930 par le mathématicien américain Alonzo Church, il s’est depuis imposé comme crucial en théorie de la démonstration et dans la conception des langages de programmation.

En logique mathématique, les scientifiques cherchent notamment à comprendre ces objets qui représentent des fonctions. À l’époque, l’idée de dériver le lambda-calcul n’avait jamais été explorée, mais les deux chercheurs ont rapidement compris qu’elle avait du potentiel. Rappelons que la notion de dérivation de fonction en mathématiques remonte aux travaux de Leibniz et Newton au XVIIe siècle. Calculer la dérivée d’une fonction mathématique en un point consiste à calculer son accroissement local. Appliquée au lambda-calcul, elle permet d'extraire des approximations linéaires de programmes informatiques, offrant ainsi une nouvelle manière de les comprendre et de les analyser.

S’ensuit une autre idée développée par Thomas Ehrhard et Laurent Regnier sur l'expansion de Taylor. En mathématiques, le développement en série de Taylor permet de représenter une fonction par une somme infinie de monômes. « De manière analogue, dans le lambda-calcul, nous avons montré comment un programme peut être décomposé en une série d’approximations linéaires successives, chacune utilisant son argument un nombre précis de fois », décrit Laurent Regnier. Cette approche aide à concilier les notions de linéarité (comment les ressources sont utilisées par un programme), de logique (comment les propositions sont manipulées) et d’algèbre. Les quatre années de recherche sur ces sujets ont donné naissance à deux nouvelles notions : le lambda-calcul différentiel puis la logique linéaire différentielle.

Ces recherches ont plus largement permis de simplifier la compréhension des propriétés d'un programme, tant au niveau fonctionnel que sémantique. Ces résultats ont fait l’objet de cinq articles aujourd’hui récompensés par le prix Alonzo Church pour leur impact exceptionnel sur la logique et sur l’informatique. Cette récompense décernée par l'Association européenne pour la logique informatique (EACSL), l'Association européenne pour l'informatique théorique (EATCS) et le groupe d'intérêt spécial de l'ACM pour la logique et l'informatique (SIGLOG) salue le travail de toute la communauté de la logique linéaire différentielle qui s’est structurée depuis.

En effet, après 20 ans d'utilisation intensive, ces concepts se sont imposés comme des outils standards pour les spécialistes de la logique linéaire et de la sémantique des langages de programmation. Ils contribuent à améliorer notre compréhension et notre capacité à modéliser des systèmes computationnels complexes. « Notre approche a notamment permis de développer des preuves qui n’étaient pas possibles jusqu’alors, mais aussi d’apporter des preuves plus simples de résultats déjà connus », explique Thomas Ehrhard, actuellement directeur de recherche CNRS à l'IRIF au sein de l’équipe-projet commune Picube (CNRS/Inria/Université Paris-Cité). Leurs idées ont aussi inspiré des avancées en théorie des catégories, une branche des mathématiques qui étudie les structures et leurs transformations.