Avancer la Théorie de l'Algèbre Universelle Quantitative – ATQUA

Les équations de programme, qui expriment l'égalité de comportement entre des programmes syntaxiquement différents, sont omniprésentes en informatique. Elles sont au cœur des définitions sémantiques, des transformations, des optimisations, etc. Le domaine mathématique de l'algèbre universelle (UA) constitue une base théorique pour ces sujets.

Cependant, dans de nombreuses applications, un raisonnement plus fin permettant de décrire que deux programmes, bien que différents sur le plan comportemental, ont des comportements similaires est souhaitable. L'algèbre universelle quantitative (QUA), une généralisation de l'UA récemment proposée par Mardare, Panangaden et Plotkin dans un article influent de la conférence LICS 2016, fournit les fondements mathématiques de ce raisonnement. Dans la QUA la similarité informelle est capturée quantitativement et numériquement par le concept mathématique de distance métrique. Par exemple, on peut prendre un programme et remplacer certaines lignes de code par des lignes différentes, mais suffisamment proches selon une métrique appropriée, et s'attendre à ce que le résultat final soit suffisamment proche du programme original dans la métrique.

Ceci est très prometteur dans le contexte de l'IA ou de l'IdO où il faut garantir des résultats fiables même lorsque les entrées, les paramètres et les données des senseurs peuvent être affectés par de perturbations, par exemple à cause de bruit.

Depuis l'article initial de LICS 2016, QUA a reçu une attention considérable et est maintenant un sujet de recherche actif dans l'informatique théorique. Les deux groupes de recherche impliqués dans ce PRCI ANR ont contribué, séparément, à un certain nombre d'avancées techniques présentées dans des conférences de premier plan.

L'objectif principal de ce projet est de stimuler une synergie entre les deux groupes et faire progresser la théorie et les applications de QUA. Ceci sera aussi rendu possible par des postdocs et un PhD financés par le projet.