Lionel Vaux
I2M, Aix-Marseille Université
/user/lionel.vaux/
Date(s) : 31/03/2016 iCal
11 h 00 min - 12 h 30 min
Ehrhard et Regnier ont montré au milieu des années 2000 que le développement de Taylor d’un λ-terme pur est toujours normalisable, et que sa forme normale correspond exactement à l’arbre de Böhm du λ-terme. Leurs techniques reposent fortement sur une propriété d’uniformité des λ-termes et sont de ce fait assez fragiles : on ne peut pas les transposer à des extensions non déterministes par exemple. Et d’ailleurs, en présence de sommes, le développement de Taylor d’un terme n’est pas toujours normalisable.
Dans des travaux récents avec Michele Pagani et Christine Tasson, en partie publiés dans FoSSaCS 2016, nous avons donné une caractérisation de la normalisabilité (forte, faible, de tête) d’un λ-terme M comme une propriété de finitude de son développement de Taylor T(M). Une conséquence (et la motivation principale) de ces travaux est que le développement de Taylor des λ-termes normalisables est lui-même normalisable, et ce y compris dans des variantes non déterministes du λ-calcul.
Il reste à établir que, dans ce cas, normalisation et développement de Taylor commutent : NF(T(M)) = T(NF(M)). Je propose pour cela de définir une notion de réduction sur les combinaisons linéaires de termes avec ressources, contenant la traduction de la β-réduction via le développement de Taylor, tout en étant compatible avec la normalisation des termes avec ressources. Je détaillerai cette solution en expliquant les problèmes qui se posent et les choix techniques qui permettent de les résoudre. J’expliquerai également en quoi cette approche permet d’introduire une alternative robuste aux arbres de Böhm comme notion de forme normale généralisée, dans un cadre non uniforme.
Catégories