Le cul-de-sac de $J_2$

La définition. L'étage $A_1$ contient $\{p^{\prime }\in S_2:\forall p^{\prime }\to q^{\prime },q^{\prime }\in A_0\}$. Pour $q$, qui n'a aucun successeur, cette condition porte sur un ensemble vide de coups : elle est vraie par vacuité. Donc $q\in A_1$, puis $p\in A_2$ puisque $J_1$ peut y aller.

Le code. Il initialise restant au degré sortant et ne décrémente que lorsqu'un successeur est retiré de la file. Une position de $J_2$ de degré $0$ n'a aucun successeur, donc n'est jamais atteinte par la boucle, donc n'est jamais marquée. Exécution :

Les deux ne disent pas la même chose. La correction tient en trois lignes : avant la boucle, on met dans la file toute position de $J_2$ dont le compteur vaut déjà $0$.

(* À ajouter APRÈS l'initialisation par la cible et AVANT la boucle :
   une position de J2 sans aucun coup satisfait le « pour tout » par vacuité. *)
Array.iteri (fun p r ->
    if ctrl.(p) = 2 && r = 0 && not dans.(p) then begin
      dans.(p) <- true; Queue.push p f
    end) restant;

Ce que ce cas signifie dans le jeu, et c'est là qu'il faut choisir. Un joueur qui ne peut plus jouer a perdu : c'est la convention normale, et elle rend la définition juste. Si l'on adopte au contraire la convention « la partie s'arrête et personne ne gagne », alors ce sont les positions terminales qu'il faut classer explicitement dans $C_1$, $C_2$ ou « nul » — les trois types d'états finals du programme — et le code redevient juste, mais la définition doit être restreinte aux positions non terminales.

La règle générale, et elle vaut au-delà de ce chapitre : un quantificateur universel sur un ensemble vide est vrai, et c'est le cas que les implémentations oublient. On l'a déjà rencontré au chapitre chap:logique ; on le retrouvera partout où une boucle « pour tout successeur » se traduit par un compteur.