Géométrie de l’Interaction Différentielle et Développement de Taylor.
Le lambda calcul est un formalisme introduit par Church pour capturer la notion de fonction calculable. C’est le paradigme de référence pour la programmation fonctionnelle et un outil incontournable pour l’étude de l’informatique théorique. Il nous permet en effet de formuler la notion de programme dans un contexte purement mathématique. Ce projet se focalise sur le lambda calcul différentiel, une extension du lambda calcul intégrant un opérateur de dérivation formelle. L’introduction de cet opérateur nous amène également à définir une notion de développement de Taylor des programmes, dont les éléments peuvent être considérés comme une approximation du programme original. Cet objet nous permet ainsi d’analyser les propriétés d’un programme en se basant sur ses approximations. Enfin, la Géométrie de l’Interaction se révèle être un outil extrêmement puissant pour visualiser et comprendre comment les programmes interagissent et évoluent. Elle est particulièrement intéressante pour étudier des méthodes d’évaluation optimale des programmes. L’objectif de ce projet est d’étudier une forme de Géométrie de l’Interaction adaptée au lambda calcul différentiel, et également de comprendre le lien entre la Géométrie de l’Interaction d’un programme et celle de ses approximations, c’est-à-dire son développement de Taylor.
Differential Geometry of Interaction and the Taylor Expansion.
Lambda calculus, introduced by Church, is a formalism designed to capture the concept of a computable function. It stands as the foundational paradigm for functional programming and plays a crucial role in the study of theoretical computer science. It allows us to formulate the notion of program in a purely mathematical context. This project focuses on the differential lambda calculus, an extension of the lambda calculus incorporating a formal derivation operator. The introduction of this operator also leads us to define the notion of Taylor development of programs, whose elements can be considered an approximation of the original program. This object allows us to analyze the properties of a program based on its approximations. At last, the Geometry of Interaction proves to be an exceptionally powerful tool for visualizing and comprehending how programs interact and evolve. It is particularly interesting for studying optimal program evaluation methods. The aim of this project is to study a form of Geometry of Interaction adapted to differential lambda calculus and also to understand the link between the Geometry of Interaction of a program and that of its approximations, i.e. its Taylor expansion.