Guillaume Bonfante (LORIA, université de Nancy)

Les ordres sont utilises (entre autre) en reecriture pour montrer la terminaison des systemes. Mais en fait, la donnee d’une preuve de terminaison renferme beaucoup plus d’informations, en particulier, on peut determiner la complexite des fonctions calculees eu egard a sa preuve de terminaison (pour les ordres usuels). Nous nous interessons essentiellement a preciser ces resultats en etudiant la « forme » des preuves de terminaison (pour les ordres par interpretation polynomiales et pour l’ordre de Knuth-Bendix). D’autre part, on peut penser utiliser les termes ordinaux pour montrer la terminaison (cf les travaux de Touzet et Cichon). Nous nous interessons a la construction d’un systeme analogue au systeme T de Godel, mais pour ces termes ordinaux.