Stratégies pour la réduction forte
Vendredi 15 décembre 2023 14h
Université Paris-Saclay, bâtiment 660 (amphithéâtre) et visioconférence
Résumé: La sémantique d’un langage de programmation, et d’un langage fonctionnel en particulier, laisse généralement une certaine liberté quant à l’ordre dans lequel sont effectuées les différentes opérations. Les différentes stratégies qui peuvent être adoptées, comme l'appel par valeur ou l'évaluation paresseuse, bénéficient déjà à la fois d'un large corpus théorique et de nombreuses implémentations efficaces. Ce corpus cependant est majoritairement tourné vers un objectif d'évaluation des programmes, c'est-à-dire de production d'une valeur. Le cadre associé est celui de l'évaluation faible, dans lequel aucune évaluation n'est effectuée à l'intérieur d'une fonction qui ne serait pas totalement appliquée. En effet, dans un langage fonctionnel la fermeture représentant une telle fonction est déjà en elle-même considérée comme une valeur.
Cependant plusieurs situations justifient d'aller au-delà de ce cadre vers un objectif de normalisation, où la réduction est poussée jusqu'au bout, y compris à l'intérieur de ce qui est usuellement considéré comme une valeur. On parle alors de réduction forte. L'évaluation forte peut notamment intervenir comme un outil d'optimisation à la compilation, pour évaluer partiellement le corps d'une fonction en fonction de valeurs qui seraient déjà connues pour certains de ses arguments. Dans un autre contexte, cela concerne également l'implémentation des assistants à la preuve, avec par exemple dans Coq les différentes machines de conversion, en stratégie paresseuse, et de réduction, en appel par valeur.
Malgré l'importance des applications, le corpus théorique fondant l'extension des stratégies usuelles de l'évaluation faible au cadre de la réduction forte reste très en-deçà du corpus traditionnel de l'évaluation faible, tant du point de vue du volume que de la maturité. Il se concentre sur quelques extensions particulières ou sur des cadres intermédiaires comme l'évaluation ouverte. Ces travaux, pour l'essentiel très récents, n'apportent cependant pas encore de réponses satisfaisantes à tous les nouveaux comportements observés en réduction forte, par exemple relatifs à l'explosion de la taille de certains termes. Par conséquent, les implémentations déjà réalisées utilisent souvent des stratégies ad hoc pour limiter l'impact de ces problèmes.
Cette thèse définit un calcul en appel par nécessité avec réduction forte, c'est-à-dire des stratégies de normalisation qui étendent les stratégies usuelles d'évaluation en appel par nécessité. Le calcul utilise des substitutions explicites afin de supprimer certains effets d'explosion de la taille des termes. Par ailleurs, les stratégies détectent de manière précoce certains radicaux nécessaires, réduisant ainsi le nombre de calculs dupliqués.
De plus, notre calcul bénéficie de propriétés de correction (les résultats obtenus correspondent bien à des formes normales du lambda-calcul) et de complétude (pour tout terme normalisable, nos stratégies atteignent bien la forme normale). Nous avons formalisé ce calcul et prouvé sa correction avec l'assistant de preuve Abella.
Parmi les stratégies autorisées par notre calcul, nous en avons isolé une qui produit systématiquement les séquences de réduction les plus courtes, et défini et implémenté une machine abstraite qui réalise cette stratégie. L'implémentation a permis de réaliser un grand nombre de tests qui confirment les gains attendus par rapport aux stratégies d'évaluation usuelles.
Membres du jury:
- Mme. Johanne COHEN, Directrice de recherche, CNRS, Université Paris Saclay - Examinatrice
- Mme. Delia KESNER, Professeure des universités, Université Paris Cité - Examinatrice
- M. Antonio BUCCIARELLI, Maître de conférences (HDR), Université Paris Cité - Rapporteur & Examinateur
- M. Giulio MANZONETTO, Professeur des universités, Université Paris Cité - Rapporteur & Examinateur
Encadrants:
- M. Guillaume MELQUIOND, Directeur de recherche, INRIA, Université Paris-Saclay - Directeur de thèse
- M. Thibaut BALABONSKI, Maître de conférences, Université Paris-Saclay - Co-encadrant de thèse