Une stratégie S est dite gagnante si toutes ses parties maximales sont gagnées par B, et si, de plus, elle n'a pas de partie infinie : une partie infinie de S est un chemin infini dans G dont tous les préfixes (finis) pairs sont dans S.

Questions de finitude: la question des parties infinies est toujours embarrassante. On préfère les jeux où il n' y pas de parties infinies. Et on aime encore plus les jeux "fortement finis" où, pour chaque position initiale p, on peut majorer la longueur des parties commençant en p. Mais on ne s'en tirera pas à si bon compte. A défaut de trouver des règles qui proscrivent les parties infinies, il faudra trouver des règles qui permettent de repérer le tricheur qui rend la partie infinie pour empécher son adversaire de gagner. Par exemple on pourra autoriser un nombre fini de coupures, et disqualifier le joueur qui fait, dans une même partie, une infinité de coupures.

Exemple: le jeu MALL

On va expliquer le jeu MALL (Multiplicative Additive Linear Logic). On commence par dire les positions.

Une position est encore un graphe, encore bipartite (B/N) avec

  • sur chaque arc, une formule positive (voir les formules plus loin)
  • un sommet distingué (le "jeton", c'est à lui de jouer).
  • En plus ce graphe doit être un arbre.

    Il faut penser les sommets comme des joueurs formant deux équipes (B/N), chaque joueur cherchant à prouver son séquent, qu'on peut former en y mettant à gauche les formules entrantes et à droite les formules sortantes. Et chaque équipe cherchant à se débarrasser définitivement du jeton. Pour la commodité, on considérera aussi des graphes avec des formules négatives, pour représenter la position obtenue en changeant, là où il faut le signe des arcs et des formules.

    Pour les formules, il y a quatre constantes , 0 et 1 qui sont positives, et \top et \bot qui sont négatives. Et puis quatre opérations : \oplus et \otimes qui donnent un résultat positif et \avec et \par qui donnent un résultat négatif.

    La négation (linéaire) F \mapsto nonF est une involution définie comme suit: elle échange 1 et \bot, ainsi que 0 et \top. Ensuite elle échange A \oplus B et nonA \avec nonB, ainsi que A \otimes B et nonA \par nonB.

    Maintenant on explique les coups de ce jeu.

    Il y a d'abord les coups passifs, qui sont très simples. Il s'agit tout simplement, pour le joueur qui a le jeton, de le faire passer, le long d'un arc entrant, au joueur voisin. Il faut penser qu'il demande à son voisin d'activer, ou de déstructurer la formule concernée.

    Et maintenant il y a les coups actifs, en gros un par formule positive.

  • S'il a une formule A \oplus B sortante, le joueur qui a le jeton peut choisir entre A et B (disons B). Le jeton passe de l'autre côté de la formule qui devient B. Si B est négative, il faudrait changer les signes, mais notre convention permet de l'éviter.
  • S'il a une formule A \times B sortante vers un joueur K, le joueur J qui a le jeton peut le passe à K, se dédoubler en deux joueurs J1 et J2, tandis que A \otimes B se casse en A, qui va de J1 à K et B qui va de J2 à K. Les autres arcs/formules qui entraient/sortaient en J se répartissent, "au gré de J", entre J1 et J2. De nouveau, notre convention nous simplifie la vie pour expliquer ça.
  • S'il a une formule 1 sortante vers le joueur K, le joueur qui a le jeton peut, à condition qu'il n'ait pas d'autre formule ni entrante ni sortante, passer le jeton à K et disparaître de la position avec son 1.
  • La dermière formule positive, c'est 0, mais il n'y a pas de coup correspondant. C'est une sorte de Faux qu'on ne peut pas prouver. Ce qui fait que le coup passif le long de \top est gagnant, en ce sens que l'adversaire ne peut pas y répondre.

    Maintenant, à la demande générale, on va donner des exemples. Pour que ces exemples ressemblent à ce dont on a l'habitude, on utilisera l' implication linéaire -o , qui est définie par A -o B := nonA \par B.