Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur Graph Search.
Concept
Terminaison d'un algorithme
Résumé
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.
É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.
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, 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.
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.
Dans le cas des processus non déterministes, la sûreté est un concept dual de la terminaison.
Source officielle
À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.
Cours associés (2)
CS-550: Formal verification
We introduce formal verification as an approach for developing highly reliable systems. Formal verification finds proofs that computer systems work under all relevant scenarios. We will learn how to u
CH-310: Dynamics and kinetics
The course covers the principles of chemical kinetics, including differential rate laws, derivation of exact and approximate integral rate laws for common elementary and composite reactions, fundament
Séances de cours associées (7)
Programmes de vérification avec l'inox: Partie 2
Se concentre sur l'utilisation d'Inox pour la vérification des programmes, en démontrant le processus de vérification des programmes et en assurant l'exactitude.
Polymérisation en chaîne: mécanisme et cinétique
Explore le mécanisme et la cinétique de la polymérisation en chaîne, en se concentrant sur les inhibiteurs et l'inhibition compétitive dans les réactions enzymatiques.
Propositions en tant que types: Logique et correspondance de programmation
Explore la relation entre les preuves logiques et les preuves de programmation à travers la correspondance de Curry-Howard.
Publications associées (11)
Personnes associées (3)
Concepts associés (6)
Correction d'un algorithme
Un algorithme est correct s'il fait ce qu'on attend de lui. Plus précisément, rappelons qu'un algorithme est décrit par une spécification des données sur lesquelles l'algorithme va démarrer son calcul et une spécification du résultat produit par l'algorithme. Démontrer la correction de l'algorithme consiste à démontrer que l'algorithme retourne, quand il calcule en partant des données, un objet qui est un des résultats escomptés et qui satisfait la spécification du résultat comme énoncé dans la description de l'algorithme.
Idris (programming language)
Idris is a purely-functional programming language with dependent types, optional lazy evaluation, and features such as a totality checker. Idris may be used as a proof assistant, but is designed to be a general-purpose programming language similar to Haskell. The Idris type system is similar to Agda's, and proofs are similar to Coq's, including tactics (theorem proving functions/procedures) via elaborator reflection. Compared to Agda and Coq, Idris prioritizes management of side effects and support for embedded domain-specific languages.
Haskell
Haskell est un langage de programmation fonctionnel fondé sur le lambda-calcul et la logique combinatoire. Son nom vient du mathématicien et logicien Haskell Curry. Il a été créé en 1990 par un comité de chercheurs en théorie des langages intéressés par les langages fonctionnels et l'évaluation paresseuse. Le dernier standard est Haskell 2010 : c'est une version minimale et portable du langage conçue à des fins pédagogiques et pratiques, dans un souci d'interopérabilité entre les implémentations du langage et comme base de futures extensions.