Terminaison d'un algorithme
La terminaison est une propriété fondamentale des algorithmes. Elle stipule que les calculs décrits par l'algorithme s'arrêteront. En général cet arrêt doit avoir lieu quelles que soient les données initiales que l'on fournit à l'algorithme. Si l'on veut insister sur ce point on parle alors souvent de terminaison uniforme, mais le plus généralement « terminaison » couvre aussi bien l'arrêt sur une donnée que l'arrêt sur toutes les données et c'est le contexte qui décide. La terminaison forme avec la correction partielle un des aspects de la correction des algorithmes, la correction partielle et la terminaison forment ce que l'on appelle la correction totale.
Dans le cas spécifique des machines de Turing, la terminaison s'appelle l'arrêt (halting en anglais dans le vocabulaire de Turing). Un cas particulier d'étude de la terminaison est la terminaison d'un système de réécriture.
Notion de terminaison
Étant donné un algorithme et des valeurs, la question de sa terminaison est de savoir s'il va s'arrêter s'il prend en entrée ces valeurs. Par exemple l'algorithme de pseudo-code :
- tant que i est supérieur à 0 remplacer i par i+1,
ne s’arrêtera sur aucune entrée positive.
Preuve de terminaison
L'une des méthodes classiques pour prouver la terminaison d'un algorithme est de définir une fonction, parfois appelée fonction de terminaison[1], qui satisfait les conditions suivantes. Elle a pour variables, les variables du programme, elle décroît pendant l'exécution et elle est à valeur dans un ensemble muni d'un ordre bien fondé, typiquement l'ensemble des entiers ou l'ensemble des couples d'entiers ou l'ensemble des multiensembles sur un ensemble déjà muni d'un ordre bien fondé. Par exemple, on choisira une fonction qui, pour un algorithme itératif décroît à chaque boucle, et pour un programme récursif décroît à chaque appel[2].
Problème de l'arrêt
Le problème de l'arrêt consiste, étant donné un algorithme, à décider s'il termine ou pas. Ce problème est indécidable, au sens algorithmique du terme.
Un concept dual: la sûreté
Dans le cas des processus non déterministes, la sûreté est un concept dual de la terminaison. En effet, au lieu de garantir que tous les calculs s'arrêteront, la sûreté garantit qu'aucun des calculs ne s'arrêtera, si on admet que l'arrêt est un état que l'on cherche à éviter. En revanche si l'arrêt est un état que l'on recherche comme bon, la vivacité est apparentée à la terminaison.
Notes et références
Voir aussi
- Complexité en temps, une autre caractéristique importante pour les programmes qui terminent : le temps de calcul en fonction de la taille de l'entrée
Portail de l'informatique théorique
Portail de l’informatique
Portail de la logique