Compositional Taylor expansion in additive and non-additive models of linear logic

Expansion de Taylor compositionnelle dans les modèles additifs et non additifs de la logique linéaire Le lambda-calcul différentiel est une théorie quantitative du calcul née de la sémantique catégorique de la logique linéaire. Le but du lambda-calcul différentiel est de compter pendant le calcul le nombre de fois qu'un programme nécessite d'accéder à son entrée. Comme son nom l'indique, le lambda-calcul différentiel est étroitement lié au calcul différentiel. En effet, l'opération qui extrait d'un programme sa composante qui utilise son entrée n fois durant le calcul correspond dans la sémantique à une opération de dérivée n-ieme. En poursuivant cette analogie, il est possible de développer une opération syntaxique d'expansion de Taylor, qui associe à un programme P une somme infinie de programmes Pn, le programme Pn étant la partie de P qui utilise son entrée exactement n fois pendant le calcul. Cependant, l'opération de somme requise pour faire l'expansion de Taylor permet de faire des sommes arbitraires de programmes, à la fois dans la syntaxe et la sémantique. La seule interprétation calculatoire de ce genre de somme est le non-déterminisme. C'est un problème, car à moins que le non-déterminisme ne soit une caractéristique explicite du langage, les calculs sont par essence déterministes. Le but de cette thèse est de développer une théorie d'expansion de Taylor qui prend en compte le déterminisme du calcul. Dans cette thèse, nous allons nous concentrer sur la partie sémantique de cette théorie, en donnant une axiomatisation catégorique de l'expansion de Taylor qui couvre des modèles déterministes ou probabilistes de la logique linéaire. Cette axiomatisation remplace les sommes arbitraires du non déterminisme par une notion appropriée de sommes partielles, et s'assure que l'expansion de Taylor survit à cette restriction des sommes. Il se trouve que cette nouvelle axiomatisation a également mené à des découvertes de propriétés catégoriques de l'expansion de Taylor qui sont intéressantes en elles mêmes, indépendamment de leur usage pour la logique linéaire ou de la restriction des sommes. De fait, nous allons dédier une partie non négligeable de cette thèse à la description de ces propriétés, indépendamment des considérations initiales de cette thèse.