Un schéma récursif d'ordre supérieur est un ensemble d'équations définissant un ensemble de fonctions d'ordre supérieur. Un tel schéma est récursif car les fonctions définies peuvent apparaitre des deux côté des équations, et est d'ordre supérieur car les fonctions peuvent prendre pour arguments des fonctions. L'interprétation d'un tel schéma - ou plutôt d'un symbole initial - est un terme infini construit à partir des constantes.
Un question fondamentale, ouverte depuis les années 80, est de trouver une classe d'automates qui caractérise l'expressivité des schémas récursifs d'ordre supérieur. Les travaux de Damm et Goerdt puis de Knapik et al. peuvent être vu comme des tentatives de réponses à cette question. Cependant il ne s'agit que de réponses partielles car ils ont dû imposer des contraintes syntaxique (types dérivés, sûreté) sur les schémas pour établir leurs résultats. Dans cet exposé je donnerai une correspondance exacte pour le cas général. Pour cela, j'introduirais une nouvelle classe d'automates à pile d'ordre supérieurs, les automates à piles effondrant.
Je m'attacherais principalement à décrire le modèle des automates effondrant et à présenter plusieurs conséquences de notre résultat d'équi-expressivité. Entre autres, j'expliquerai comment il permet d'obtenir une preuve nouvelle de la décidabilité de MSO sur les schémas récursifs (Ong, LICS'06) et pourquoi il permet de reformuler la conjecture safe vs unsafe pour les schémas.
Je terminerai enfin par une série de problèmes ouverts.
Tous ces travaux ont été réalisés en collaboration avec M. Hagues, A. Murawski et L. Ong (Univ. Oxford)