OCaml (option informatique) · Chapitre 20 · Exercice de TD
Une propriété sémantique indécidable
Calculabilité et décidabilité · niveau 3 (difficile)
Énoncé
Montrer que « le programme p (sur l'entrée 0) finit par afficher 42 » est indécidable.
Corrigé
Réduction depuis l'arrêt. Pour décider si q s'arrête sur y, construisons p qui : exécute q sur y, puis (s'il revient) affiche 42. Alors p affiche 42 si et seulement si q s'arrête sur y. Un décideur de « affiche 42 » donnerait donc un décideur de l'arrêt : impossible. C'est une illustration du théorème de Rice — toute propriété non triviale du comportement est indécidable.