Réductions et approximations linéaires

Non communiquéDe nombreux outils syntaxiques et sémantiques ont été développés pour l'étude de la dynamique des preuves et des programmes au cours des cinquante dernières années. Nous montrons ici que parmi ces outils – en particulier les types intersections et certaines sémantiques bien connues – de nombreux peuvent être définis au travers d'approximations linéaires de la manière suivante : pour un langage donné, on définit d'abord une notion d'approximation qui associe à un terme du langage un ensemble (généralement infini) d'approximants ayant un comportement dynamique dérivé de celui du terme ; puis on définit les outils usuels sur les approximants, ce qui est grandement simplifié par la linéarité, et enfin, on ramène cette construction au terme de départ. Définir une notion d'approximation cohérente avec la dynamique nécessite de présenter les langages étudiés dans un cadre 2- catégorique. Ce cadre permet d'exprimer comment les constructions sur les approximants donnent la construction générale (par une variation sur la construction de Grothendieck dans le cas des types intersections, et par des extensions de Kan dans le cas des sémantiques) et est suffisamment général pour englober les systèmes de types intersections caractérisant des propriétés de normalisation pour différentes variantes du λ-calcul (par nom, par valeur et le λμ- calcul) ainsi que la plupart des sémantiques issues de la logique linéaire.Enfin, on s'intéresse aux limites des approximants en étudiant dans quelles situations un terme est ou non caractérisé par certaines de ses approximations