Soutenance de thèse de Rémy CERDA

Depuis son introduction par Church, le λ-calcul a joué un rôle majeur dans un siècle de développement de l'informatique théorique et de la logique mathématique, mais aussi dans la naissance de nombreux langages de programmation. Une propriété cruciale de ce calcul est qu'il n'est pas normalisant en général, de sorte qu'un intérêt croissant a porté sur la recherche d'approximations de sa dynamique. Les outils « classiques » d'approximation, nés dans les années 1970 dans le sillage des sémantiques de Scott, sont essentiellement sémantiques. Les outils basés sur le développement de Taylor, introduits dans les années 2000 par Ehrhard et Regnier, proposent à l'inverse une approximation dynamique de la β-réduction. Puisant ses inspirations dans le développement de la logique linéaire, le développement de Taylor traduit le λ-calcul vers un calcul « à ressources » multilinéaire, muni d'une dynamique finitaire. Un théorème de commutation (entre approximation et normalisation) fait notamment l'efficacité de cette approche, et en justifie le succès. La notion d'arbre de Böhm est centrale dans cette ligne de recherche. Née de l'idée que les termes normalisants ne sont pas les seuls à avoir un sens calculatoire, elle généralise la notion de forme normale en constituant une « forme normale à l'infini ». La compréhension de la nature coinductive de cet objet a mené dans les années 1990 à l'introduction de λ-calculs infinitaires. Dans ces calculs, les termes et les réductions peuvent être infinis et, dans le cas du calcul 001-infinitaire, l'arbre de Böhm est la notion de forme normale à l'infini (sans guillemets). L'idée qui guide cette thèse est que le λ-calcul 001-infinitaire se prête à une généralisation de l'approximation de Taylor où, en particulier, les arbres de Böhm seraient des « citoyens ordinaires ». L'approximation du λ-calcul fini, et notamment de ses propriétés de normalisation, devient alors un cas particulier de l'approximation du calcul infinitaire. Cela est permis par le principal résultat de la thèse, qui établit que la dynamique du calcul à ressources est à même de simuler la β-réduction infinitaire via le développement de Taylor. Pour arriver à ce résultat, nous faisons d'abord un détour par une présentation abstraite d'une syntaxe « mixte » (inductive et coinductive) d'ordre supérieur, à l'aide d'un formalisme nominal généralisant des travaux récents introduisant des types coalgébriques avec lieurs. Cela nous permet de définir formellement des coalgèbres de classes d'α-équivalence de λ-termes infinitaires (chapitre 1). Dans un second temps, nous définissons les λ-calculs infinitaires à l'aide d'une présentation coinductive, puis nous rappelons leurs principales propriétés ainsi que leur lien avec les théories classiques de l'approximation de la β-réduction (chapitre 2). Ensuite, nous présentons le λ-calcul à ressources comme un cas particulier d'une réécriture avec sommes, et distinguons ses versions qualitative et quantitative (chapitre 3). Dans une seconde partie consacrée à l'approximation de Taylor proprement dite, nous commençons par introduire le développement de Taylor des λ-termes infinitaires et prouvons le théorème de simulation annoncé, dans sa forme qualitative puis quantitative. Nous démontrons l'efficacité de ce théorème en le mettant à l'œuvre, proposant notamment une nouvelle preuve de confluence pour le λ-calcul 001-infinitaire (chapitre 4). Enfin, nous nous penchons sur la conservativité de la propriété de simulation, et démontrons l'existence surprenante d'un contre-exemple à cette propriété réciproque (chapitre 5).

Since its introduction by Church, the λ-calculus has played a major role in a century of development in theoretical computer science and mathematical logic, as well as in the birth of numerous programming languages. A crucial property of this calculus is that it is not normalising in general, leading to growing interest in finding approximations to its dynamics. The 'classic' approximation tools, which emerged in the 1970s in the wake of Scott's semantics, are essentially semantic. The tools based on Taylor expansion, introduced in the 2000s by Ehrhard and Regnier, conversely propose a dynamic approximation of the β-reduction. Drawing its inspiration from the development of linear logic, Taylor expansion translates the λ-calculus into a multilinear 'resource' calculus, equipped with finitary dynamics. A commutation theorem (between approximation and normalisation) makes this approach particularly effective, and justifies its success. The notion of Böhm tree is central to this line of research. Assoiated with the idea that normalising terms are not the only computationally meaningful ones, it generalises the notion of normal form by constituting an 'infinite normal form'. Understanding the coinductive nature of this object led in the 1990s to the introduction of infinitary λ-calculi. In these calculi, terms and reductions can be infinite and, in the case of the 001-infinitary calculus, the Böhm tree is the notion of infinite normal form (without quotes). The idea guiding this thesis is that the 001-infinitary λ-calculus lends itself to a generalisation of the Taylor approximation where, in particular, Böhm trees would be 'ordinary citizens'. The approximation of the finite λ-calculus, and in particular its normalisation properties, then becomes a special case of the approximation of the infinitary calculus. This is enabled by the main result of the thesis, which establishes that the dynamics of the resource calculus is able to simulate the infinitary β-reduction via Taylor expansion. To arrive at this result, we first make a diversion via an abstract presentation of a 'mixed' (inductive and coinductive) higher-order syntax, using a nominal formalism generalising recent work on coalgebraic types with binders. This allows us to formally define coalgebras of α-equivalence classes of infinite λ-terms (Chapter 1). In a second step, we define infinitary λ-calculi using a coinductive presentation, then recall their main properties as well as their connection with classical theories of approximation of the β-reduction (Chapter 2). Then, we present the resource λ-calculus as a special case of a rewriting with sums, and distinguish its qualitative and quantitative flavours (Chapter 3). In a second part devoted to the Taylor approximation itself, we begin by introducing the Taylor expansion of infinitary λ-terms and prove the announced simulation theorem, in its qualitative and quantitative forms. We demonstrate the effectiveness of this theorem by putting it at work, proposing in particular a new confluence proof for the 001-infinitary λ-calculus (Chapter 4). Finally, we consider the conservativity of the simulation property, and demonstrate the surprising existence of a counterexample to this converse property (Chapter 5).