Calculabilité et décidabilité
Cours · OCaml (option informatique), chapitre 20 · prépas MPSI et MP, option informatique · le début du chapitre, la suite sur Adloun
20.1 Introduction et motivation
Tout au long de ce livre, on a écrit des programmes et prouvé qu'ils s'arrêtent (variant, chapitre 4) et calculent juste (invariant). Une question vertigineuse se pose alors : pourrait-on écrire un programme qui décide automatiquement, pour n'importe quel programme, s'il s'arrête ? Plus généralement, tout problème bien posé est-il résoluble par un algorithme ?
La réponse, l'un des plus beaux résultats de l'informatique, est non : il existe des problèmes parfaitement définis qu'aucun programme ne pourra jamais résoudre. Le plus célèbre est le problème de l'arrêt. Ce chapitre final, théorique, en donne la démonstration (par auto-référence, à la Turing) et ses conséquences — notamment pourquoi la terminaison se prouve « à la main », au cas par cas, faute de pouvoir l'automatiser en général.
20.2 Décidable, semi-décidable
Un problème de décision associe à chaque entrée une réponse oui ou non. Il est décidable s'il existe un algorithme qui, sur toute entrée, s'arrête et donne la bonne réponse. Il est semi-décidable s'il existe un algorithme qui s'arrête en répondant oui sur les instances positives, mais peut ne pas s'arrêter sur les négatives.
« Cette liste est-elle triée ? » est décidable : la fonction du chapitre 9 s'arrête toujours.
let rec est_trie l =
match l with
| [] | [_] -> true
| x :: (y :: _ as reste) -> x <= y && est_trie resteDe même « n est-il premier ? », « cet automate accepte-t-il ce mot ? » (chapitre 18), « ce graphe est-il connexe ? » (chapitre 15) : tous décidables, car résolus par des algorithmes qui terminent sur toute entrée.
Exercices du chapitre
- Semi-décider l'arrêt corrigé
- Syracuse, problème ouvert mais pas indécidable corrigé
- Comprendre une réduction corrigé
- La diagonale corrigé
- Une propriété sémantique indécidable corrigé
- Le castor affairé (busy beaver) corrigé