Caractérisation de H* par le développement de Taylor extensionnel
Date(s) : 25/05/2023 iCal
11h00 - 12h30
Le développement de Taylor extensionnel déjà présenté au séminaire
le 9 février dernier valide les règles β et η : deux termes
βη-convertibles ont des développements de Taylor équivalents (pour la
réduction du calcul à ressources extensionnel).
Mieux : comme les sémantiques des jeux dont il est inspiré, ce
développement de Taylor extensionnel est un modèle de la théorie H*,
la plus grande λ-théorie cohérente et sensée. Celle-ci peut être
caractérisée par l’égalité des arbres de Nakajima, qui sont des sortes
d’arbres de Böhm infiniment η-longs (c’est un exercice du Barendregt),
mais ces derniers sont difficiles à définir et à manipuler. On peut
voir le calcul à ressources extensionnel comme un langage
d’approximations finies des arbres de Nakajima, à la syntaxe et à la
dynamique très simples, au même titre que le calcul à ressources
usuel définit un calcul d’approximations finies des arbres de Böhm.
Dans cet exposé, je rappellerai rapidement la syntaxe du calcul à
ressources extensionnel et les propriétés basiques du développement de
Taylor associé. Je démontrerai ensuite que deux λ-termes ont des
développements de Taylor extensionnels équivalents ssi ils sont
équivalents pour H*. J’expliquerai enfin comment ce résultat permet
d’établir simplement qu’un certain modèle relationnel du λ-calcul
admet H* comme théorie (un résultat de Manzonetto, dont la
démonstration se ramène maintenant au seul fait que ce modèle est
compatible avec le développement de Taylor extensionnel).
Comme le précédent, cet exposé est basé sur des travaux en cours
avec Lison Blondeau-Patissier (qui en abordera d’autres aspects le 22
juin) et Pierre Clairambault. Les prépublications sont là :
https://arxiv.org/abs/2302.04685 et https://arxiv.org/abs/2305.08489.
Emplacement
I2M Luminy - Ancienne BU, Salle Séminaire2 (RdC)
Catégories
