Caractérisation impérative des algorithmes séquentiels en temps quelconque, primitif récursif ou polynomial

Les résultats de Colson ou de Moschovakis remettent en question que le modèle récursif primitif puisse calculer une valeur par tous les moyens possibles : il y a toutes les fonctions voulues mais il manque des algorithmes. La thèse de Church exprime donc plutôt ce qui peut être calculé que comment le calcul est fait. Nous utilisons la thèse de Gurevich formalisant l'idée intuitive d'algorithme séquentiel par les Abstract States Machines (ASMs).Nous représentons les programmes impératifs par le langage While de Jones, et une variante LoopC du langage de Meyer et Ritchie permettant de sortir d'une boucle lorsqu'une condition est remplie. Nous dirons qu'un langage caractérise une classe algorithmique si les modèles de calcul associés peuvent se simuler mutuellement, en utilisant une dilatation temporelle et un nombre borné de variables temporaires. Nous prouvons que les ASMs peuvent simuler While et LoopC, que si l'espace est primitif récursif alors LoopC est en temps récursif primitif, et que sa restriction LoopC_stat où les bornes des boucles ne peuvent être mises à jour est en temps polynomial. Réciproquement, une étape d'ASM peut être traduite par un programme sans boucle, qu'on peut répéter suffisamment en l'insérant dans un programme qui est dans While si la complexité est quelconque, dans LoopC si elle est récursif primitif, et dans LoopC_stat si elle est polynomiale.Ainsi While caractérise les algorithmes séquentiels en temps quelconque, LoopC ceux en temps et espace récursifs primitifs, et LoopC_stat ceux en temps polynomial