Taylor approximation and infinitary lambda-calculi

Approximation de Taylor et λ-calcul infinitaire 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 com- mutation (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 normalisant 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). Nous nous penchons également 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). Enfin, nous étendons notre travail au cadre paresseux, c’est-à-dire celui du λ-calcul 101-infinitaire, et nous démontrons un théorème de commutation pour les arbres de Lévy-Longo (chapitre 6)