Développement de Taylor extensionnel des λ-termes purs

Lionel Vaux Auclair
I2M, Aix Marseille université
/user/lionel.vaux/

Date(s) : 09/02/2023   iCal
11 h 00 min - 12 h 30 min

Né au début des années 2000 avec les travaux d’Ehrhard et Regnier sur le λ-calcul différentiel, le développement de Taylor des programmes et des preuves est devenu un outil polyvalent et un concept structurant pour l’étude du λ-calcul et de la logique linéaire.

Il consiste à associer à chaque λ-terme un ensemble, voire une combinaison linéaire infinie de termes à ressources, qui sont des approximations multilinéaires de λ-termes. Les termes à ressources sont eux-mêmes munis d’une dynamique, qui est strictement finitaire (tous les termes sont fortement normalisables) et qu’on peut à son tour voir comme une approximation de la β-réduction : chaque pas de β-réduction est simulé par la réduction itérée des termes à ressources dans l’image du développement de Taylor.

Dans cet exposé, je présenterai une version extensionnelle du développement de Taylor : c’est-à-dire qu’elle valide la règle η du λ-calcul, qui assure que tout terme est équivalent à une abstraction.
La prise en compte de la règle η est une question naturelle (on sait très bien la gérer sur les arbres de Böhm par exemple), mais elle est étonnamment difficile. En effet, contrairement à la β-réduction, elle ne peut pas se réduire à une transformation locale sur les termes à ressources du calcul introduit par Ehrhard et Regnier.

La solution, issue de travaux en collaboration avec Lison Blondeau-Patissier et Pierre Clairambault, consiste à considérer des termes à ressources qu’on peut qualifier d’η-longs. Dans un cadre typé, cette contrainte assure que tout terme de type fonctionnel est équivalent à une abstraction. En l’absence de typage, on doit modifier la syntaxe pour considérer des termes infiniment η-longs, c’est-à-dire que chaque valeur commence par une infinité d’abstractions. Je réserve les détails scabreux de l’implémentation pour l’exposé mais les spécialistes de sémantique des jeux y trouveront des similitudes non fortuites.

L’exposé sera également retransmis ici : https://greenlight.lal.cloud.math.cnrs.fr/b/lio-hdc-jef


Séminaire Logique et Interactions

 

Emplacement
Site Sud, Luminy, Ancienne BU, Salle Séminaire2 (RdC)

Catégories



Retour en haut 

Secured By miniOrange