Retour à l'index du GREYC

Séminaire Algorithmique

Site du CNRS

Séminaire Algorithmique

Le séminaire a lieu le mardi à 11 h 45 (sauf modification exceptionnelle), au campus Côte de Nacre, bâtiment Sciences 3, salle S3 351, 3ème étage.

Résumé du séminaire du Mardi 17 Avril 2001

Utilisation d'ordres en reecriture : problemes de complexite, et de constructions

par 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.

GREYC
Campus Côte de Nacre, boulevard du Maréchal Juin
BP 5186
14032 Caen Cedex
FAX : +33 (0)2 31 56 73 30
http://www.greyc.fr