18/10/2001: Jean Goubault (ENS Cachan)
Un theoreme simple de terminaison.

Résumé
Les ordres recursifs sur les chemins sont un outil pratique pour montrer la terminaison de systemes de reecriture, introduits par Dershowitz voici une vingtaine d'annees. La demonstration classique de leur noetherianite passe par le theoreme de Kruskal et l'axiome du choix.
Je vais donner une version abstraite de ces ordres et une preuve elementaire de leur noetherianite. De plus,
1. La preuve est intuitionniste, ce qui pave le chemin a une analyse des longueurs maximales de reduction (travail futur...)
2. La preuve est elementaire (une demi-page de Coq). En ceci, d'autres preuves non basees sur Kruskal ont deja ete donnees (Ferreira et Zantema 1995, Jouannaud et Rubio 1999), mais sont plus longues.
3. Alors que le theoreme de Kruskal est tres lie a la structure de terme, je montrerai que les ordres recursifs sur les chemins sont pratiquement independants de la notion de terme. Il s'ensuit des applications aux reecritures de graphes, de termes infinis, et d'automates notamment.
Dans une deuxieme partie, je montrerai pourquoi ce theoreme ne s'applique pas tel quel au lambda-calcul, et quelle extension naturelle on peut en faire pour qu'il s'applique. On trouve alors une construction tres proche du horpo de Jouannaud et Rubio (1999), dont la preuve de noetherianite est essentiellement la meme que pour le cas plus simple decrit ci-dessus.
Je conclurai en donnant quelques applications, concluantes ou conjecturees.