Semi-décider l'arrêt

(* execute_n_etapes p x k : exécute p sur x pendant au plus k étapes,
   renvoie true si p s'est arrêté dans ce délai (fonction idéalisée). *)
let semi_arrete p x =
  let k = ref 0 in
  while not (execute_n_etapes p x !k) do k := !k + 1 done;
  true

On simule p de plus en plus longtemps. Si p s'arrête (en k0 étapes), on le détecte dès k = k0 et l'on renvoie true. Mais si p boucle, la recherche sur k ne s'arrête jamais : aucune réponse non. Semi-décideur, pas décideur.