Frontières de la reconnaissabilité – FREC

Traiter, par des moyens finis, des données prises dans un ensemble infini est l’un des défis auxquels l’informatique est confrontée. Le concept central qu’elle a fait émerger pour y répondre est la notion algébrique de reconnaissabilité, qui jouit en effet de propriétés algorithmiques et de clôture remarquables, alliées avec une puissance d’expression fort utile. Sa combinaison avec la logique et la théorie des automates s’est révélée incroyablement fructueuse.

L’objectif du projet est d’être à la pointe de l’extension de l’approche algébrique rendue possible par de récents progrès. Une nouvelle frontière est en train de s’ouvrir à l’étude de la reconnaissabilité. Nous nous concentrerons sur quatre fronts. L'un d’eux (T2) concerne les langages d'arbres : les arbres sont devenus un modèle essentiel en informatique, du fait de l'émergence de XML, devenu un format standard d'échange de données sur le web et de structuration des bases de données, et du fait de leur rôle en vérification. Le second front (T3) concerne les langages de lambda-termes. Ces derniers jouent un rôle essentiel en linguistique informatique et en sémantique, mais ils ne sont d'habitude pas étudiés du point de vue de la reconnaissabilité. Le troisième front (T4) est l'étude des automates à compteurs limités pour les mots et les arbres. Il existe des connections surprenantes entre ces modèles et des questions classiques. Le dernier front (T5), qui sert de fondement, développera des outils algébriques et topologiques pour les autres tâches, sur la base de l'émergence de concepts et de résultats entièrement nouveaux, qui ont révolutionné la théorie algébrique des langages reconnaissables de mots finis.

Le projet bénéficiera des développements récents importants sur ces quatre fronts. Pour celui qui a la plus longue histoire (T5), il s’agit de la découverte du rôle de la dualité de Stone et de la puissance des équations profinies. La recherche dans le domaine des langages d’arbres (T2) a aussi une histoire relativement longue, mais des approches algébriques récemment introduites lui ont donné un nouvel élan. Les tâches T3 et T4 ouvrent des domaines très novateurs encore largement inexploités. Les tout premiers résultats dans ces deux champs justifient à nos yeux la place importante qu’ils ont dans ce projet. L’interaction entre des tâches parvenues à des degrés différents de maturité nous paraît pouvoir être extrêmement profitable.

Dans le domaine des arbres, nous espérons mieux comprendre la puissance expressive des formalismes d’arbres. Par exemple, un des principaux problèmes ouverts du domaine est la décidabilité du premier ordre pour les arbres. Un autre objectif est de comprendre les effets de l’existence d’un ordre ad-hoc dans les arbres, un ordre qui découle naturellement de la façon dont les arbres sont mis en mémoire ou acquis.

Pour les lambda-termes, nous étudierons la notion récente de reconnaissabilité. Les outils algébriques et topologiques que nous développerons permettront de faire le lien avec la sémantique des langages de programmation et la linguistique. Cette approche a déjà fait émerger de nouvelles intuitions et des résultats (par exemple une preuve simple de la décidabilité du matching du 4ème ordre). Enfin, nous voulons entamer l’étude des lambda-termes infinis, et envisager la théorie des schémas de programme récursifs depuis une nouvelle perspective.

Nous fournirons enfin les bases algorithmiques de l’étude des fonctions de coût et nous développerons une approche logique de leur théorie, que nous essaierons ensuite d’étendre aux arbres. De récents résultats ont montré que sur les mots, la théorie des fonctions de coût permet d’obtenir des preuves simples de résultats classiques comme la décidabilité de la hiérarchie de hauteur d’étoile.L’extension de ce type de théorie aux arbres infinis résoudrait un problème ouvert ancien de la théorie des automates, celui de la hiérarchie de Mostowski.