Il est bien connu que la fonction d'Ackermann-Péter A n'est pas primitive récursive (et pour cause : pour toute fonction primitive récursive f, il existe y tel que f(x)<A(x,y)).

Par ailleurs, sa preuve de terminaison est généralement donnée par la décroissance lexicographique de ses paramètres.

Il est évident qu'on ne peut prouver la terminaison de cette fonction en faisant remarquer qu'une fonction primitive récursive (par exemple, une fonction arithmétique élémentaire) de ses paramètres décroît strictement, car cela permettrait de borner son temps d'exécution par une fonction primitive récursive et donc de l'exprimer sous une forme primitive récursive. Ceci justifie donc l'usage de l'ordre lexicographique...

D'où ma question : quel est le rapport entre les preuves de terminaison et les classes de fonctions ? Je sens bien qu'il y a des histoires de calcul sur les ordinaux, mais rien de plus précis.