Towards a resource based approximation theory of programs

Il y a un peu moins de 20 ans, Ehrhard et Regnier, inspirés par la sémantique de la logique linéaire, ont découvert la possibilité d'effectuer un développement de Taylor d'un programme dans le cadre du lambda-calcul. Même en oubliant les coefficients rationnels, les termes qui apparaissent dans le développement de Taylor d'un programme contiennent de l'information quantitative sur le programme lui-même. Si l'on considère ces termes sensibles aux ressources, on obtient une théorie de l'approximation qui est plus simple que l'originelle et qui est encore intéressante. Or, en mathématiques, une notion d'approximation est d'habitude vue comme un outil pour prouver des propriétés des objets que l'on approxime : ce sera également notre approche dans ce manuscrit. Dans la première partie de la thèse, on définit cette théorie de l'approximation par ressources et on l'applique à des résultats, qui sont déjà connus mais fondamentaux, du lambda-calcul. On montre notamment que, dans une certaine mesure, cela subsume la théorie classique de l'approximation qui est basée sur les arbres de Böhm et sur la continuité, et on le fait en fournissant des nouvelles preuves de ces résultats importants. Nos techniques de preuves utilisent toutes les propriété cruciales de telle notion d'approximation, notamment la linéarité, la normalisation forte et la confluence. On obtient ainsi une nouvelle formulation d'une partie importante du lambda-calcul, qui en plus apporte deux avantages : premièrement, même si nos preuves ne sont pas du tout triviales, elles sont tout de même plus "basiques" que celles traditionnelles, dans le sens où elles sont basées sur l'induction (à la base de la définition du développement de Taylor) au lieu de la coinduction (à la base de la définition d'arbre de Böhm); deuxièmement, on peut voir de cette façon que tous ces résultats, qui sont d'habitude prouvés avec des techniques ad-hoc et dépendants les uns des autres, sont en réalité indépendants et proviennent tous d'une seule technique : l'approximation par ressources (et la commutation d'Ehrhard et Regnier entre la normalisation et le développement). Cette notion d'approximation, et en général la formule du développement de Taylor, a un troisième avantage : elle est facilement transportable à d'autres langages de programmation, et cette direction de recherche a été souvent empruntée dans les années récentes. Dans une deuxième partie de la thèse, on se tourne justement vers cette optique, et on adapte l'approximation par ressources au lambda-mu-calcul, l'un des habituels langages de programmation fonctionnels (impurs) qui sont en correspondance de Curry-Howard avec la logique classique. Même si plusieurs définitions et propriétés sont simples à adapter dans ce nouveau cadre, les preuves de normalisation forte et de confluence du calcul avec ressources associé ne sont pas immédiates. Enfin, on s'attaque à la question des applications de ces outils ; on montre comment reproduire, dans le lambda-mu-calcul, les preuves données avant pour le lambda-calcul pour établir la propriété de Stabilité et celle des Lignes Perpendiculaires. Ce sont deux nouveaux résultats sur la structure mathématique du lambda-calcul-calcul. On remarquera aussi que la preuve de la propriété de Stabilité peut être également adaptée dans le cadre du lambda-calcul avec appel par valeur. On conclut le manuscrit avec des réflexions qui ont pour but de lier des méthodes d'homotopie avec la sémantique dénotationnelle de la logique linéaire, mais aussi avec des réflexions méthodologiques et philosophiques sur le statut de notre discipline de rechercheAlmost 20 years ago Ehrhard and Regnier, inspired by the semantics of linear logic, discoveredthe possibility of performing the Taylor expansion of a program in the realm of lambda-calculus. Evenforgetting the rational coefficients, the terms populating the Taylor expansion of a programcontain quantitative information about the program itself. Simply collecting such resourcesensitive approximants allows to define an approximation theory simpler than the original one,but still meaningful. Now, in mathematics, a notion of approximation is usually conceived as atool for inferring properties of the approximated objects: it is precisely the approach we adoptin this manuscript.In the first part of the thesis, we define this resource approximation theory and apply itto the investigation of some already known, but fundamental, properties of lambda-calculus. More specifically, we show that in some sense it subsumes the classic theory of approximation, based on Böhm trees and continuity, by providing new proofs of these important results. Our proof techniques employ all the crucial aspects of this notion of approximation, i.e., linearity, strong normalisation and confluence. We obtain in this way a new formulation of an important part of lambda-calculus, presenting two advantages: firstly, even though they are not trivial, our new proofs are more ?basic? than the old ones, in the sense that they are based on induction (at the base of Taylor expansion) rather than coinduction (at the base of Böhm trees); secondly, we are able to see that in fact all these results, usually based on ad-hoc, interrelated techniques are actually independent from each another, and only originate from a unique technique: resource approximation (exploiting Ehrhard and Regnier's commutation between normalisation and expansion). This notion of approximation and, more generally, the Taylor expansion formula, has a third advantage: it scales to other programming languages, and this direction has been often explored in the recent years. In the second part of the thesis, we add another brick to these works by adapting the resource approximation to the lambda-mu-calculus, one of the most typical (impure) functional programming language in Curry-Howard correspondence with classical logic. Althoughmost definitions and properties are straightforward to obtain in the new setting, the proof of strong normalisation and confluence of the corresponding resource calculus are not immediate. Finally, we consider the question of the application of the developed tools; we show how one can easily reproduce, in the lambda-mu-calculus, the proofs given for lambda-calculus of two results, namely the Stability Property and the Perpendicular Lines Property. Those constitute two original results on the mathematical foundations of lambda-mu-calculus. We also remark that the Stability Property can be easily adapted to the case of call-by-value lambda-calculus. We conclude the thesis by presenting some work in progress, aiming at relating homotopy with denotational semantics of linear logic, as well as some methodological and philosophical considerations about our discipline of researc