Lipsum.dev

Blague, énigme et raisonnement automatisé

19 septembre 2025 — Énigme, Logique épistémique

Dans un article du journal Le Monde, le vulgarisateur Mickaël Launay présente la blague suivante :

C’est l’histoire de trois logiciennes qui entrent dans un bar.
« Tout le monde prend une bière ? », demande le barman.
La première logicienne répond : « Je ne sais pas ».
La deuxième répond : « Je ne sais pas ».
La troisième répond : « Oui ! ».

Je reviendrai un peu plus loin sur cette blague — vous pouvez, si besoin, déjà prendre connaissance de l’explication fournie dans le lien qui précède.

Mon but ici est, à travers cet exemple et un autre qui va suivre, d’illustrer comment certains types de raisonnements peuvent être automatisés.

Une énigme

Je vous propose maintenant de nous intéresser à une autre énigme, qui est une variante de l’énigme des « blue-eyed islanders » décrite sur le blog de Terence Tao :

Cinq personnes vivent sur une île au milieu du Pacifique, où règne un étrange tabou : il est interdit de connaître la couleur de ses propres yeux.
Chacun voit bien la couleur des yeux de chaque autre habitant, mais il est interdit d’en discuter et si par malheur un des cinq habitants venait à apprendre la couleur de ses propres yeux, il devrait alors se donner la mort le lendemain sur la place du village, à midi lorsque tous y sont réunis.
Un lundi, un étranger aux yeux bleus accoste sur l’île. Le soir, il dîne avec tous les habitants et s’exclame devant eux : « Je suis surpris, ce n’est pas courant de voir quelqu’un aux yeux bleus dans cette région du monde ! »; il repart ensuite.
Le mardi, les cinq habitants se réunissent à midi comme à leur habitude et déjeunent.
Le mercredi, les cinq habitants se réunissent à midi comme à leur habitude et déjeunent.
Le jeudi, les cinq habitants se réunissent à midi comme à leur habitude et là, trois d’entre eux se donnent la mort.
Comment expliquer ces évènements ?

Avant de donner la réponse, j’aimerais discuter un peu de ce qu’ont en commun ces différentes histoires.

Un langage formel

Revenons à la blague d’introduction concernant les trois logiciennes : Alice, Bianca et Clara.

La question du barman est « Tout le monde prend une bière ? », qui peut se transcrire formellement en $p_1 \land p_2 \land p_3$ où l’on introduit les variables booléennes associées aux choix des logiciennes :

$p_1: \text{Alice veut une bière}$
$p_2: \text{Bianca veut une bière}$
$p_3: \text{Clara veut une bière}$

Par ailleurs, nous utiliserons les notations suivantes pour exprimer des propositions sur l’état de connaissance d’un agent $x$ (e.g. Alice, Bianca ou Clara) :

$K_x^{?}(p)$ représente la proposition « $x$ connaît la valeur de vérité de la proposition $p$ »
$K_x(p)$ représente la proposition « $x$ sait que la proposition $p$ est vraie » (ce qui est plus fort)
Enfin, pour toute proposition $p$ (y compris des propositions à propos de la connaissance des agents), nous noterons $[! p ]$ pour signifier que $p$ est annoncée vraie devant tous les agents.

Le déroulé de la scène est donc le suivant :

Alice répond « Je ne sais pas », ce que l’on peut écrire de façon formelle ${\lnot K_a^{?}(p_1 \land p_2 \land p_3)}$ . Par ailleurs, cette information sur la connaissance d’Alice est annoncée publiquement, on note donc : ${[! \lnot K_a^{?}(p_1 \land p_2 \land p_3)]}$
Ensuite, Bianca annonce qu’elle ne sait pas non plus, ce que l’on écrira de même : ${[! \lnot K_b^{?}(p_1 \land p_2 \land p_3)]}$
Enfin, Clara répond « Oui ! », ce que l’on écrira ${K_c(p_1 \land p_2 \land p_3)}$ . Il s’agit aussi d’une annonce, mais ici nous ne l’indiquons pas car nous voulons juste valider que cette proposition se déduit des annonces qui précèdent.

Tout cela mis ensemble, la scène peut se transcrire formellement par la formule ${[! \lnot K_a^{?}(p_1 \land p_2 \land p_3)][! \lnot K_b^{?}(p_1 \land p_2 \land p_3)]K_c(p_1 \land p_2 \land p_3)}$ qui signifie précisément qu’après les deux annonces successives d’Alice et Bianca, Clara sait qu’elles veulent toutes les trois prendre une bière.

Un logiciel de raisonnement automatisée

Le logiciel SMCDEL, codé en Haskell — je reviendrai un peu plus loin sur son fonctionnement — permet de décrire un scénario comme celui de la blague des logiciennes et de vérifier sa validité, c’est-à-dire dans notre cas de vérifier que les annonces d’Alice et Bianca permettent effectivement à Clara d’avoir connaissance de la réponse.

Voici comment on y peut encoder ce scénario :

-- Déclaration de trois variables booléennes (correspondant à p1, p2, p3)
VARS 1,2,3
-- Cette instruction signifie qu'il n'y a pas de contraintes particulières
-- sur les valeurs possibles des variables
LAW  Top
-- Ici, on décrit quelles variables sont observables initialement par quel agent
-- (en l'occurrence, chacun ne connaît que sa propre volonté)
OBS  a: 1
     b: 2
     c: 3
-- Validation du scénario précédemment présenté
VALID?
  [ ! ~ a knows whether (1 & 2 & 3) ]
  [ ! ~ b knows whether (1 & 2 & 3) ]
  c knows whether (1 & 2 & 3)

Vous pouvez copier / coller ce code dans https://w4eg.de/malvin/illc/smcdelweb/index.html et cliquer sur RUN SMCDEL!, puis vérifier dans la fenêtre de droite que la formula est bien validée.

Si vous supprimez la ligne [ ! ~ b knows whether (1 & 2 & 3) ] correspondant à l’annonce de Bianca, vous verrez au contraire que la validation échoue.

(Cet exemple est par ailleurs implémenté de façon un peu plus détaillée dans le logiciel, section Load Examples: DrinkingLogicians.)

Retour sur notre énigme (spoiler : solution)

Le logiciel présenté précédemment dispose aussi d’une instruction WHERE? qui permet d’identifier automatiquement les configurations d’un système qui valident un scénario.

Dans le cas de l’énigme, on peut utiliser des variables $p_i$ ( $i = 1, 2, 3, 4, 5$ ) pour encoder les propositions « L’habitant $i$ a les yeux bleus ? » et regarder ce que cela nous donne. C’est ce que j’ai fait ci-dessous :

-- Variables booléennes encodant pour chaque agent « Il ou elle a les yeux bleus ? »
VARS 1,2,3,4,5
LAW Top
-- Chaque agent peut voir les yeux de chaque autre agent, mais pas les siens
OBS a: 2, 3, 4, 5
    b: 1, 3, 4, 5
    c: 1, 2, 4, 5
    d: 1, 2, 3, 5
    e: 1, 2, 3, 4
WHERE?
   -- Lundi : Le visiteur annonce qu'il voit une personne aux yeux bleux
   < ! (1 | 2 | 3 | 4 | 5) >
   -- Mardi : Les habitants se réunissent et déjeunent.
   < ! (
         ~(a knows that 1)
         & ~(b knows that 2)
         & ~(c knows that 3)
         & ~(d knows that 4)
         & ~(e knows that 5)
      ) >
    -- Mercredi : Les habitants se réunissent et déjeunent.
    < ! (
         ~(a knows that 1)
         & ~(b knows that 2)
         & ~(c knows that 3)
         & ~(d knows that 4)
         & ~(e knows that 5)
      ) >
   -- Jeudi : Les habitants se réunissent,
   -- a, b et c ont appris la couleur de leurs yeux et se suicident.
   (
      a knows that 1
      & b knows that 2
      & c knows that 3
      & ~(d knows that 4)
      & ~(e knows that 5)
   )

En exécutant ce code dans SMCDEL, on apprend que le seul état qui valide ce scénario est $\{1, 2, 3\}$ : c’est-à-dire que les trois habitants qui se sont suicidés (et seulement eux) avaient les yeux bleus.

Il peut sembler paradoxal que l’annonce de l’étranger ait un quelconque effet puisque chacun des habitants savait déjà qu’il existait au moins un habitant aux yeux bleus : de fait, chacun pouvait voir au moins deux habitants aux yeux bleus. SMCDEL nous le confirme d’ailleurs :

-- La commande TRUE? nous permet de valider que sous l'hypothèse que les trois
-- premiers habitants (et seulement eux) ont les yeux bleus, ils sont bien
-- déjà au courant qu'au moins un habitant a les yeux bleus
TRUE?
    {1, 2, 3}
    a knows that (1 | 2 | 3 | 4 | 5)
    & b knows that (1 | 2 | 3 | 4 | 5)
    & c knows that (1 | 2 | 3 | 4 | 5)
    & d knows that (1 | 2 | 3 | 4 | 5)
    & e knows that (1 | 2 | 3 | 4 | 5)

De même, tous les habitants savaient que tous les habitants savaient qu’il existait au moins un habitant aux yeux bleus (comme ils en voyaient au moins deux, ils savaient que chacun en voyait au moins un) :

-- a (aux yeux bleus) sait que tous les habitants savent qu'au moins un habitant
-- a les yeux bleus
TRUE?
    {1, 2, 3}
    a knows that a knows that (1 | 2 | 3 | 4 | 5)
    & a knows that b knows that (1 | 2 | 3 | 4 | 5)
    & a knows that c knows that (1 | 2 | 3 | 4 | 5)
    & a knows that d knows that (1 | 2 | 3 | 4 | 5)
    & a knows that e knows that (1 | 2 | 3 | 4 | 5)

Mais, tous les habitants ne savaient pas que tous les habitants savaient que tous les habitants savaient qu’il existait un habitant aux yeux bleus.

Par exemple, l’un des trois habitants aux yeux bleus pouvait penser qu’il n’y avait que deux habitants aux yeux bleus (ceux qu’il voyait) et pouvait donc penser que l’un de ces deux pensait qu’il n’y avait qu’un seul habitant aux yeux bleus qui lui-même aurait donc pu être ignorant du fait qu’il existait un habitant aux yeux bleus (oui, cette phrase est compliquée…).

Ce raisonnement nous est confirmé par le code ci-dessous :

-- a (aux yeux bleus) ne sait pas que b (aux yeux bleus) sait que c (aux yeux bleus)
-- sait que tous les habitants savent qu'au moins un habitant a les yeux bleus
TRUE?
    {1, 2, 3}
   ~(a knows that b knows that c knows that (1 | 2 | 3 | 4 | 5))

En terme de théorie des jeux on dirait que, avant l’annonce du visiteur, la connaissance de la proposition était mutuelle mais pas commune, ce qu’elle est devenue ensuite.

Cette notion peut également directement se vérifier dans le logiciel :

TRUE?
   {1, 2, 3}
   ~((a, b, c, d, e) comknow that (1 | 2 | 3 | 4 | 5))

Muni de ces explications, vous avez maintenant les éléments pour avancer dans la compréhension de cette (difficile) énigme. Vous pouvez si besoin consulter ce fil Reddit qui discute d’un scénario similaire.

Le code complet de cet exemple est disponible ici.

Quelques mots sur le fonctionnement de SMCDEL

Les formules logiques utilisées pour modéliser les deux problèmes font partie de ce qu’on appelle la logique épistémique dynamique.

Il n’est pas du tout évident de vérifier efficacement de telles formules, en particulier lorsque le nombre d’agents ou de configurations possibles est élevé.

Une approche fondée sur les modèles de Kripke consiste à maintenir en mémoire une liste des mondes possibles et des relations de compatibilité entre eux, du point de vue de chacun des agents.

SMCDEL est un outil codé dans le langage Haskell, qui a été développé dans le cadre d’une thèse. Il s’inspire de l’approche des modèles de Kripke et introduit des structures de données permettant de résoudre plus efficacement des problèmes complexes de logique épistémique dynamique.

Une partie du travail exposé dans la thèse a notamment consisté à prouver différents théorèmes permettant de valider l’approche retenue. Je vous invite à lire le rapport de thèse si vous voulez en apprendre davantage.

Maths et applications, avec les mains et avec du code 💻
Suivre sur Twitter

← Sur un résultat d'impossibilité en informatique