16 décembre 2013
Yoann Marquer (LACL - UPEC)Gurevich a caractérisé dans “Sequential Abstract State Machines Capture Sequential Algorithms” les algorithmes symboliques séquentiels par ses ASMs. Philippe Andary, Bruno Patrou et Pierre Valarcher ont montré dans “A theorem of representation for primitive recursive algorithms” qu’un langage impératif simplifié (le Loop de Albert Meyer et Dennis Ritchie enrichi d’une instruction exit) permettait d’implémenter fidèlement (c’est à dire presque pas à pas) une classe restreinte d’ASMs : les APRAs (Arithmetical Primitive Recursive Algorithms). Mais :
les seuls symboles dynamiques sont les variables
le seul type de données utilisé est celui des entiers unaires
la complexité de l’algorithme est supposée primitive récursive.
Je m’intéresse à un langage de programmation impératif suffisamment général, de façon à ce que les résultats puissent être pertinents pour des langages réels comme le C ou le Python. Théorème 1 : Un langage impératif peut simuler presque pas à pas tout algorithme symbolique séquentiel. Le pas à pas peut être obtenu en augmentant la puissance du langage. Pour travailler sur la complexité de l’algorithme, c’est à dire la durée d’une exécution en fonction de la taille des entrées, il est nécessaire de pouvoir définir les types de données usuels ainsi que leur taille. Théorème 2 : Les types usuels peuvent être implémentés dans les structures logiques des ASMs. Cela comprend les booléens, les entiers, les mots et les listes. Les tableaux, les matrices, les graphes et les pointeurs feront l’objet d’une discussion. Ainsi, nous étendons bien le résultat sur les APRAs :
nous donnons un sens opérationnel à la notion de fonction dynamique
les types usuels sont décrits et leur taille bien définie
la complexité peut être quelconque en utilisant une instruction while, et de plus si elle est primitive récursive il est possible de n’utiliser que des instructions for à la place.