Rémy Cerda
I2M, Aix-Marseille
https://www.i2m.univ-amu.fr/perso/remy.cerda/
Date(s) : 25/11/2021 iCal
11 h 00 min - 12 h 30 min
Formalisme appuyé sur la logique linéaire de Girard, le développement de Taylor de λ-termes développé par Ehrhard et Regnier a été largement utilisé comme outil d’approximation de diverses variantes du λ-calcul. De nombreux résultats découlent d’un théorème de commutation reliant la forme normale du développement de Taylor d’un terme à l’arbre de Böhm de ce terme. Ces arbres de Böhm, quant à eux, sont une notion de « forme normale infinie » de la β-réduction, et se trouvent également être les formes normales d’une version du λ-calcul infinitaire de Kennaway et al.
Cela suggère d’étendre le développement de Taylor au calcul infinitaire en question — Λ001 de son petit nom —, dont on donnera une présentation coinductive fondée sur les travaux d’Endrullis et Polonsky. Le principal résultat auquel on aboutit est la simulation de la β-réduction infinitaire par la réduction avec ressources (finitaire) du développement de Taylor. On en discutera les conséquences, lequel chantier est toujours en cours.
Emplacement
Site Sud, Luminy, Ancienne BU, Salle Séminaire2 (RdC)
Catégories