Lê Thành Dũng Nguyễn
IRISA, Rennes
https://nguyentito.eu/
Date(s) : 03/03/2022 iCal
11 h 00 min - 12 h 30 min
La correspondance preuves-programmes fait intervenir des langages de programmation totaux, qui ne sont donc pas Turing-complets. Quels prédicats ou quelles fonctions peut-on définir par des termes d’un type idoine (pensez à « string -> bool ») dans de tels langages ? Le domaine de la complexité implicite (*) a montré que des classes de complexité intéressantes pouvaient être caractérisées ainsi. De tels résultats s’appuient sur des systèmes de types délibérément conçus dans cette optique, et souvent inspirés de la logique linéaire.
(*) Voir https://tel.archives-ouvertes.fr/tel-02978986
Dans le travail présenté ici, nous portons notre attention sur des λ-calculs typés (certains étant linéaires ou affines) introduits pour des raisons initiales sans rapport avec la complexité implicite. Nous prétendons que des liens avec divers modèles de calcul à états finis (autrement dit, des automates) émergent alors plus naturellement dans ce contexte qu’avec la théorie de la complexité algorithmique.
En particulier, cet exposé se concentrera sur les transducteurs, c’est-à-dire les automates pouvant produire un mot en sortie, qui sont un objet d’étude central des informaticien⋅ne⋅s d’à côté (équipe MoVe du LIS). Si le temps permet, je pourrai mentionner également :
- une caractérisation des langages sans étoile au moyen du λ-calcul non commutatif (planaire) ;
- quelques pistes pour éclaircir de vieilles questions sur le λ-calcul simplement typé ;
- les outils sémantiques mis en œuvre pour obtenir ces résultats, et leur lien avec la théorie catégorique des automates.
Ce travail est une collaboration avec Pierre Pradic (Lecturer à Swansea University), et on pourra trouver un résumé un peu plus technique de nos recherches à l’adresse suivante : https://cs-web.swan.ac.uk/~pierrepradic/smp-abstract.pdf
Catégories