Sur la syntaxe de la sémantique quantitative (HDR Lionel Vaux Auclair)

Composition du jury

• Robin Cockett (Calgary, rapporteur),
• Ugo Dal Lago (Bologna),
• Delia Kesner (Paris, rapporteuse),
• Guy McCusker (Bath, rapporteur),
• Paul-André Melliès (Paris),
• Myriam Quatrini (Aix-Marseille),
• Laurent Regnier (Aix-Marseille).

Résumé

Le développement de Taylor des λ-termes et des preuves de la logique linéaire est le fruit d’une relecture syntaxique par Ehrhard et Regnier de la sémantique quantitative de Girard : il associe à chaque terme ou preuve une combinaison linéaire infinie d’approximations multilinéaires et finies de l’objet de départ. Il matérialise une correspondance étroite entre le comportement calculatoire des termes, défini par la β-réduction, et leur interprétation dans certains modèles dénotationnels : le développement de Taylor d’un terme est toujours normalisable, et sa forme normale correspond exactement à l’arbre de Böhm du terme. Cette correspondance se retrouve dans le fait que, pour de nombreux modèles de la logique linéaire, la promotion d’un morphisme s’obtient comme une superposition d’opérations multilinéaires, faisant du développement de Taylor des preuves une structure sous-jacente de ces modèles.

Ce mémoire présente quelques avancées récentes visant à raffiner l’analyse de la normalisation (qui est un processus potentiellement infini) offerte par le développement de Taylor pour la ramener au niveau de la β-réduction ou de l’élimination des coupures (qui correspond à un calcul fini).

On démontre que cette approche permet d’étendre l’analyse à un cadre non-uniforme, susceptible de prendre en compte par exemple une forme de non-déterminisme calculatoire — alors que la normalisation peut échouer dans ce cadre. On démontre également que la même approche peut être appliquée aux réseaux de démonstration de la logique linéaire. Enfin les techniques développées précédemment permettent de revisiter et simplifier le résultat originel d’Ehrhard et Regnier pour la normalisation dans le cas uniforme, tout en l’adaptant à une forme restreinte de non-déterminisme.

Visio : https://greenlight.virtualdata.cloud.math.cnrs.fr/b/lio-22f-qvd

La soutenance sera précédée d’une séance du séminaire logique et interactions, à 14h et toujours à la FRUMAM, avec deux exposés donnés l’un par Ugo Dal Lago et l’autre par Paul-André Melliès.