Planners-5c — Le différentiel d’atteignabilité : ce que l’ajout d’une primitive rend possible

« Les agents modifient leur vocabulaire » est une formule nébuleuse. Ce notebook la rend testable.

Le lake planning_lean — consommé ici, jamais modifié — prouve sans sorry que toute trajectoire réelle reste une trajectoire possible dans la dynamique relaxée sans delete (run π s ⊆ runR π s, Planning/Relaxation.lean:56, lemme clé step ⊆ stepR en Planning/Strips.lean:58), d’où l’admissibilité \(h^+ \le h^*\) (Planning/Admissibility.lean:41). C’est un théorème sur deux mondes issus du même vocabulaire : la relaxation élargit ce que les deletes interdisaient.

La question de ce notebook est d’une autre nature :

quelle nouvelle classe de plans devient atteignable après l’ajout d’une primitive ?

C’est un différentiel d’atteignabilité : \(A_t \hookrightarrow A_{t+1}\), et l’on mesure ce que l’élargissement du vocabulaire rend possible que l’approfondissement de la recherche dans \(A_t\) ne pouvait pas. Le protocole, en quatre pas :

  1. Un problème où aucune politique disponible n’atteint le but — vérifié, pas supposé.
  2. L’agent cherche davantage dans le même \(A_t\) — plus de budget, meilleure heuristique — et échoue toujours. Sans cette mesure de contrôle, on ne sait pas si l’extension a servi.
  3. L’agent est autorisé à inventer une primitive — nommée, et payante.
  4. L’extension rend le but atteignable — le delta est mesuré en buts, en coûts, en taille d’espace.

Ce que le protocole sépare : chercher davantage dans un espace d’actions donné contre élargir cet espace. C’est aussi le banc du différentiel de Laborit — l’écart entre approfondir et élargir (cf. issue #12233, strate 7, See #12207). Le companion formel de la relaxation est Planners-5b ; le présent notebook en est le consommateur expérimental.

Le moteur STRIPS, minimal et déterministe

Tout est en stdlib pur : le sujet est le protocole de mesure, pas un solveur. Un état est un frozenset de propositions, un opérateur STRIPS un triplet (préconditions, ajouts, suppressions). Deux dynamiques cohabitent, exactement comme dans le lake :

  • successeurs — la dynamique réelle (step : adds puis dels) ;
  • successeurs_relaxes — la dynamique sans delete (stepR : adds seulement), la même construction que celle sur laquelle step_subset_stepR (Planning/Strips.lean:58) porte.

L’itération est triée partout : deux exécutions donnent les mêmes nombres (la mesure est déterministe, exigence de la série).

from collections import deque

class Operateur:
    """Operateur STRIPS : nom, preconditions, ajouts, suppressions (cout 1)."""
    def __init__(self, nom, precond, ajouts, dels):
        self.nom, self.precond, self.ajouts, self.dels = nom, frozenset(precond), frozenset(ajouts), frozenset(dels)
    def applicable(self, etat):
        return self.precond <= etat
    def __repr__(self):
        return self.nom

def successeurs(etat, ops):
    """Dynamique reelle (step) : tous les etats successeurs, ordre deterministe."""
    out = []
    for op in sorted(ops, key=lambda o: o.nom):
        if op.applicable(etat):
            out.append((op, (etat | op.ajouts) - op.dels))
    return out

def successeurs_relaxes(etat, ops):
    """Dynamique sans delete (stepR) : l'etat ne fait que croitre."""
    out = []
    for op in sorted(ops, key=lambda o: o.nom):
        if op.applicable(etat) and not op.ajouts <= etat:
            out.append((op, etat | op.ajouts))
    return out

def bfs(initial, ops):
    """Enumere EXACTEMENT l'ensemble atteignable (dynamique reelle).
    Retourne (dist, peres, expansions)."""
    dist = {initial: 0}
    peres = {initial: None}
    expansions = 0
    file = deque([initial])
    while file:
        s = file.popleft()
        expansions += 1
        for op, t in successeurs(s, ops):
            if t not in dist:
                dist[t] = dist[s] + 1
                peres[t] = (s, op)
                file.append(t)
    return dist, peres, expansions

def reconstruire(peres, but):
    plan, s = [], but
    while peres[s] is not None:
        s, op = peres[s]
        plan.append(op.nom)
    return list(reversed(plan))

def distances_relaxees(initial, ops):
    """BFS dans le monde sans delete : distance relaxee de chaque proposition
    (premiere apparition). C'est la base de l'heuristique h_max."""
    dist_atoms = {p: 0 for p in initial}
    vu = {initial}
    file = deque([(initial, 0)])
    while file:
        s, d = file.popleft()
        for op, t in successeurs_relaxes(s, ops):
            if t not in vu:
                vu.add(t)
                for p in t - s:
                    dist_atoms.setdefault(p, d + 1)
                file.append((t, d + 1))
    return dist_atoms

def h_max(etat, but_conjonctif, ops):
    """h_max : max des distances relaxees des atomes du but. Admissible,
    calculable exactement — la version calculable de la chaine h_max <= h+ <= h*
    garantee par le lake (Admissibility.lean:41)."""
    dr = distances_relaxees(etat, ops)
    if any(b not in dr for b in but_conjonctif):
        return float('inf')
    return max(dr[b] for b in but_conjonctif)

print("Moteur STRIPS charge : step (reel) + stepR (relaxe sans delete).")
Moteur STRIPS charge : step (reel) + stepR (relaxe sans delete).

Les deux dynamiques, face à face avec le lake

La correspondance avec le lake est terme à terme : là où Planning/Strips.lean définit un Action F (préconditions, ajouts, suppressions) et deux transitions — step (la réelle : ajouts puis suppressions) et stepR (la relaxée : ajouts seulement) — le moteur ci-dessus définit la même paire. Le lemme step_subset_stepR (Strips.lean:58) dit pourquoi la relaxée ne peut qu’élargir : appliquer un opérateur sans faire les suppressions rend l’état obtenu sur-ensemble de l’état réel — un état réel est toujours un état relaxé possible, jamais l’inverse.

Deux choix de mesure méritent d’être dits :

  • Déterminisme : les opérateurs sont itérés triés par nom, les états sont des frozenset — deux exécutions produisent les mêmes nombres. Une mesure qui dérive d’une exécution à l’autre ne peut pas étalonner un différentiel.
  • Pourquoi h_max et pas h⁺ direct : le coût du plan relaxé optimal (\(h^+\)) est NP-difficile à calculer exactement ; \(h_{max}\) — le maximum des distances relaxées par atome — se calcule exactement par BFS et minore \(h^+\). La chaîne complète mesurable est donc \(h_{max} \le h^+ \le h^*\) : le lake garantit le maillon droit (Admissibility.lean:41), le notebook mesure les deux extrémités calculables.

Le domaine : deux rives, un gouffre, un radeau qui n’existe pas encore

Une grille \(6 \times 3\) où la colonne 3 est un gouffre (aucune case) : rive gauche (colonnes 0-2), rive droite (colonnes 4-5). Le robot démarre en \((0,0)\). Sur la rive gauche : une planchette en \((1,1)\) et une clé en \((2,0)\). Sur la rive droite : un trésor en \((4,1)\).

Le vocabulaire disponible \(A_t\) : se déplacer (4 directions, case cible existante) et ramasser (être sur la case de l’objet). Trois buts :

But Proposition Rive
\(g_1\) atteindre la balise en \((5,2)\) droite
\(g_2\) détenir le trésor droite
\(g_3\) détenir la clé gauche

\(g_3\) est le témoin de santé : s’il échoue, c’est le moteur qui est en cause, pas le gouffre.

COLS_GAUCHE = [0, 1, 2]
COLS_DROITE = [4, 5]
RANGS = [0, 1, 2]
CASES = sorted({(c, r) for c in COLS_GAUCHE + COLS_DROITE for r in RANGS})  # colonne 3 = gouffre

def prop(c, r):
    return f"at-x{c}-y{r}"

INITIAL = frozenset({prop(0, 0), "plank-at-x1-y1", "key-at-x2-y0", "treasure-at-x4-y1"})

def ops_de_base():
    ops = []
    for (c, r) in CASES:
        for (dc, dr, nom_dir) in [(1, 0, "est"), (-1, 0, "ouest"), (0, 1, "nord"), (0, -1, "sud")]:
            cible = (c + dc, r + dr)
            if cible in CASES:
                ops.append(Operateur(f"move-{nom_dir}-x{c}-y{r}", {prop(c, r)}, {prop(*cible)}, {prop(c, r)}))
    for objet, cell in [("plank", (1, 1)), ("key", (2, 0)), ("treasure", (4, 1))]:
        c, r = cell
        ops.append(Operateur(f"pickup-{objet}", {prop(c, r), f"{objet}-at-x{c}-y{r}"},
                             {f"holding-{objet}"}, {f"{objet}-at-x{c}-y{r}"}))
    return ops

A_T = ops_de_base()
BUTS = {"g1: balise (5,2)": frozenset({prop(5, 2)}),
        "g2: detenir le tresor": frozenset({"holding-treasure"}),
        "g3: detenir la cle": frozenset({"holding-key"})}

print(f"Cases existantes : {len(CASES)} (colonne 3 = gouffre)")
print(f"Operateurs A_t   : {len(A_T)} ({sum(1 for o in A_T if o.nom.startswith('move'))} moves + {sum(1 for o in A_T if o.nom.startswith('pickup'))} pickups)")
print(f"Buts             : {list(BUTS)}")
Cases existantes : 15 (colonne 3 = gouffre)
Operateurs A_t   : 41 (38 moves + 3 pickups)
Buts             : ['g1: balise (5,2)', 'g2: detenir le tresor', 'g3: detenir la cle']

Pas 1 — Vérifier l’inatteignabilité, pas la supposer

L’énumération exhaustive de l’ensemble atteignable est un certificat fini : si l’espace est énuméré en entier et que le but n’y figure pas, l’inatteignabilité est exacte — pas un délai dépassé, pas une impression. C’est l’exigence du protocole : le pas 1 ne dit pas « on n’a pas trouvé », il dit « il n’y a pas ».

dist_t, peres_t, exp_t = bfs(INITIAL, A_T)
S_atteint = set(dist_t)

print(f"Ensemble atteignable dans A_t : {len(S_atteint)} etats, {exp_t} expansions (BFS exhaustif)")
print()
for nom, but in sorted(BUTS.items()):
    ok = any(but <= s for s in S_atteint)
    hstar = min((d for s, d in dist_t.items() if but <= s), default=float('inf'))
    print(f"{nom:28s} atteignable={ok}   h*={hstar if hstar != float('inf') else 'infini'}")

but_droite = [p for s in S_atteint for p in s if p.startswith(('at-x4', 'at-x5', 'holding-treasure'))]
print(f"\nPropositions de la rive droite presentes dans l'ensemble atteignable : {sorted(set(but_droite)) or 'AUCUNE'}")
Ensemble atteignable dans A_t : 36 etats, 36 expansions (BFS exhaustif)

g1: balise (5,2)             atteignable=False   h*=infini
g2: detenir le tresor        atteignable=False   h*=infini
g3: detenir la cle           atteignable=True   h*=3

Propositions de la rive droite presentes dans l'ensemble atteignable : AUCUNE

Lecture du pas 1 : le certificat et son architecture

L’ensemble atteignable vaut exactement 36 états — et ce nombre n’est pas arbitraire : 9 cases de la rive gauche × 4 combinaisons d’inventaire (∅, planchette, clé, les deux). La rive droite apporte zéro état : aucune proposition at-x4-*/at-x5-*/holding-treasure n’apparaît jamais. Le BFS a énuméré l’espace en entier (36 expansions pour 36 états : chaque état a été dépilé exactement une fois) — l’inatteignabilité de \(g_1\) et \(g_2\) est donc un certificat fini, à distinguer soigneusement d’un échec de recherche : un solveur qui « n’a pas trouvé en 10 secondes » ne prouve rien ; une énumération complète qui ne contient pas le but prouve l’impossibilité.

Le témoin de santé fait son office : \(g_3\) est atteignable avec \(h^* = 3\) (deux déplacements jusqu’à la clé en \((2,0)\), un pickup). Le moteur marche, le gouffre seul est en cause.

Pas 2 — La mesure de contrôle : chercher davantage dans le même \(A_t\)

C’est le pas que l’on a le plus envie de sauter, et le grain entier s’effondre sans lui. Trois niveaux d’effort, même vocabulaire :

  1. BFS exhaustif — l’exploration complète (déjà faite, budget : 36 états) ;
  2. A* avec l’heuristique admissible \(h_{max}\) — la meilleure heuristique calculable issue de la relaxation du lake (chaîne \(h_{max} \le h^+ \le h^*\)) ;
  3. IDDFS (approfondissement itératif, profondeur 24) — l’effort systématique sans mémoire.

Si le but devient atteignable à un seul de ces niveaux, l’extension du pas 3 n’aurait rien mesuré : c’était un problème de recherche, pas de vocabulaire.

import heapq, itertools

def astar_hmax(initial, but, ops):
    """A* avec h_max (admissible). Retourne (but_atteint, expansions)."""
    compteur = itertools.count()
    frontiere = [(h_max(initial, but, ops), 0, next(compteur), initial)]
    vu = {initial}
    expansions = 0
    while frontiere:
        f, g, _, s = heapq.heappop(frontiere)
        expansions += 1
        if but <= s:
            return True, expansions, g
        for op, t in successeurs(s, ops):
            if t not in vu:
                vu.add(t)
                heapq.heappush(frontiere, (g + 1 + h_max(t, but, ops), g + 1, next(compteur), t))
    return False, expansions, None

def iddfs(initial, but, ops, prof_max):
    """Iterative deepening : exhaustif a profondeur bornee."""
    expansions = 0
    for limite in range(prof_max + 1):
        pile = [(initial, 0)]
        chemin_vu = set()
        while pile:
            s, d = pile.pop()
            expansions += 1
            if but <= s:
                return True, expansions, d
            if d < limite:
                for op, t in successeurs(s, ops):
                    if (t, d + 1) not in chemin_vu:
                        chemin_vu.add((t, d + 1))
                        pile.append((t, d + 1))
    return False, expansions, None

rapport = []
for nom, but in sorted(BUTS.items()):
    ok_bfs = any(but <= s for s in S_atteint)
    ok_astar, exp_astar, g_astar = astar_hmax(INITIAL, but, A_T)
    ok_iddfs, exp_iddfs, d_iddfs = iddfs(INITIAL, but, A_T, 24)
    rapport.append((nom, ok_bfs, exp_t, ok_astar, exp_astar, ok_iddfs, exp_iddfs))

print(f"{'but':28s} {'BFS':>10s} {'A*+h_max':>18s} {'IDDFS(24)':>18s}")
for nom, b, eb, a, ea, i, ei in rapport:
    print(f"{nom:28s} {'OK' if b else 'ECHEC':>7s}({eb:3d}) {'OK' if a else 'ECHEC':>8s}({ea:4d}) {'OK' if i else 'ECHEC':>8s}({ei:5d})")

print("\nVerdict du controle : g1 et g2 echouent aux TROIS niveaux d'effort.")
print("L'espace atteignable est le MEME (36 etats) quel que soit le budget.")
but                                 BFS           A*+h_max          IDDFS(24)
g1: balise (5,2)               ECHEC( 36)    ECHEC(  36)    ECHEC( 4151)
g2: detenir le tresor          ECHEC( 36)    ECHEC(  36)    ECHEC( 4151)
g3: detenir la cle                OK( 36)       OK(   4)       OK(   24)

Verdict du controle : g1 et g2 echouent aux TROIS niveaux d'effort.
L'espace atteignable est le MEME (36 etats) quel que soit le budget.

Lecture du pas 2 : l’asymétrie des budgets est la signature

Le tableau se lit en deux colonnes morales. Sur le but atteignable \(g_3\), l’effort paie de façon spectaculaire : BFS énumère les 36 états, A* avec \(h_{max}\) n’en développe que 4 (l’heuristique admissible le mène droit au but), IDDFS en re-développe 24. C’est le régime ordinaire de la planification : plus d’effort, une meilleure heuristique — le même problème devient tractable.

Sur les buts inatteignables, l’effet disparaît : BFS et A* rendent le même verdict en énumérant le même espace de 36 états — la meilleure heuristique du monde ne peut pas indiquer un chemin qui n’existe pas, elle ne peut qu’épuiser. IDDFS, lui, brûle 4 151 expansions — plus de cent fois la taille de l’espace, parce qu’il ré-explorre sans mémoire à chaque seuil de profondeur — pour conclure la même chose. C’est l’asymétrie qui authentifie le diagnostic :

  • budgets qui s’améliorent sur un but → le problème était de recherche ;
  • budgets qui brûlent sans rien rapporter → le problème est de vocabulaire.

Et le résultat négatif de la relaxation (section suivante) complète le verdict : même le monde relaxé — pourtant plus grand par construction — ne contient pas la rive droite. Le trou n’est pas dans les deletes, il est dans l’alphabet des actions.

Ce que le lake garantit — et pourquoi la relaxation ne peut pas sauver \(g_1\)

Le théorème d’admissibilité (Planning/Admissibility.lean:41) dit : tout plan réel est un plan relaxé, donc \(h^+ \le h^*\). La relaxation sans delete (run ⊆ runR, Planning/Relaxation.lean:56) est un élargissement de monde : elle rend atteignable tout ce que les suppressions d’effets interdisaient. Mesurons-la ici :

  • sur la rive gauche, la relaxation minorer honnêtement : \(h_{max} \le h^*\), parfois strictement — le but conjonctif « planchette et clé et revenir au départ » coûte 8 en réel mais paraît plus court au monde relaxé (les positions s’accumulent, les détours disparaissent) ;
  • sur \(g_1\)/\(g_2\), la distance relaxée est infinie elle aussi : aucun opérateur de \(A_t\), même relaxé, ne produit une proposition de la rive droite. La relaxation élargit les mondes par les deletes ; une primitive manquante est un trou que même le monde relaxé ne comble pas.
# (a) La relaxation minore, parfois strictement, sur la rive gauche
but_conjonctif = frozenset({"holding-plank", "holding-key", prop(0, 0)})
hstar_conj = min((d for s, d in dist_t.items() if but_conjonctif <= s), default=float('inf'))
hmax_conj = h_max(INITIAL, but_conjonctif, A_T)
print(f"But conjonctif (planchette ET cle ET revenir au depart)")
print(f"  h* (reel, BFS uniforme)  = {hstar_conj}")
print(f"  h_max (relaxe, exact)    = {hmax_conj}")
print(f"  chaine verifiee          : h_max ({hmax_conj}) <= h* ({hstar_conj})  -> {'STRICT' if hmax_conj < hstar_conj else 'egalite'}")
print(f"  (le lake garantit h+ <= h* en Admissibility.lean:41 ; h_max <= h+ complete la chaine)")

# (b) Sur g1/g2 : meme le monde relaxe est infini
for nom in ["g1: balise (5,2)", "g2: detenir le tresor"]:
    hm = h_max(INITIAL, BUTS[nom], A_T)
    print(f"\n{nom}: h_max dans A_t = {hm if hm != float('inf') else 'INFINI (relaxement inatteignable)'}")
But conjonctif (planchette ET cle ET revenir au depart)
  h* (reel, BFS uniforme)  = 8
  h_max (relaxe, exact)    = 3
  chaine verifiee          : h_max (3) <= h* (8)  -> STRICT
  (le lake garantit h+ <= h* en Admissibility.lean:41 ; h_max <= h+ complete la chaine)

g1: balise (5,2): h_max dans A_t = INFINI (relaxement inatteignable)

g2: detenir le tresor: h_max dans A_t = INFINI (relaxement inatteignable)

Pas 3 — La primitive nommée, et ce qu’elle coûte

Une extension gratuite ne mesure rien : si la nouvelle action ne coûte rien, le delta d’atteignabilité n’a pas de contrefactuel. La primitive inventée ici est le radeau :

raft-across-y{r} — préconditions : être en \((2,r)\) et détenir la planchette. Effets : atterrir en \((4,r)\) ; la planchette est consommée (suppression holding-plank).

Son coût est double et visible dans les plans du pas 4 : (1) la planchette est dépensée — un seul trajet, pas d’aller-retour gratuit ; (2) l’aller chercher en \((1,1)\) est un détour imposé avant la traversée. Le vocabulaire s’élargit : \(A_t \hookrightarrow A_{t+1}\).

def ops_avec_radeau():
    ops = ops_de_base()
    for r in RANGS:
        ops.append(Operateur(
            f"raft-across-y{r}",
            {prop(2, r), "holding-plank"},
            {prop(4, r)},
            {prop(2, r), "holding-plank"}))
    return ops

A_T1 = ops_avec_radeau()
nouveaux = [o for o in A_T1 if o.nom.startswith("raft-")]
print(f"A_t   : {len(A_T)} operateurs")
print(f"A_t+1 : {len(A_T1)} operateurs (primitive ajoutee : {sorted(o.nom for o in nouveaux)})")
for op in nouveaux:
    print(f"  {op.nom}: precond={sorted(op.precond)} ajouts={sorted(op.ajouts)} supprime={sorted(op.dels)}")
A_t   : 41 operateurs
A_t+1 : 44 operateurs (primitive ajoutee : ['raft-across-y0', 'raft-across-y1', 'raft-across-y2'])
  raft-across-y0: precond=['at-x2-y0', 'holding-plank'] ajouts=['at-x4-y0'] supprime=['at-x2-y0', 'holding-plank']
  raft-across-y1: precond=['at-x2-y1', 'holding-plank'] ajouts=['at-x4-y1'] supprime=['at-x2-y1', 'holding-plank']
  raft-across-y2: precond=['at-x2-y2', 'holding-plank'] ajouts=['at-x4-y2'] supprime=['at-x2-y2', 'holding-plank']

Pas 4 — Le delta, mesuré

Trois mesures, pas une impression :

  1. En buts : quels éléments de \(G\) deviennent atteignables — le différentiel \(\Delta = \text{atteignable}(A_{t+1}) \setminus \text{atteignable}(A_t)\), but par but ;
  2. En plans : le plan pour \(g_1\) et celui pour \(g_2\), exhibés action par action avec leur coût \(h^*\) ;
  3. En espace : la taille de l’ensemble atteignable — le monde lui-même a grandi, ce n’est pas la recherche qui a approfondi.
dist_t1, peres_t1, exp_t1 = bfs(INITIAL, A_T1)
S_atteint_1 = set(dist_t1)

print(f"Ensemble atteignable : |A_t| = {len(S_atteint)} etats  ->  |A_t+1| = {len(S_atteint_1)} etats "
      f"(+{len(S_atteint_1) - len(S_atteint)})")
print()
print(f"{'but':28s} {'A_t':>8s} {'A_t+1':>8s} {'h*(A_t+1)':>10s}  delta")
for nom, but in sorted(BUTS.items()):
    avant = any(but <= s for s in S_atteint)
    apres = any(but <= s for s in S_atteint_1)
    h1 = min((d for s, d in dist_t1.items() if but <= s), default=float('inf'))
    print(f"{nom:28s} {'OK' if avant else 'ECHEC':>8s} {'OK' if apres else 'ECHEC':>8s} {h1:>10}  {'NOUVELLEMENT ATTEIGNABLE' if (apres and not avant) else ''}")

etat_g1 = min((s for s in dist_t1 if BUTS['g1: balise (5,2)'] <= s), key=lambda s: dist_t1[s])
etat_g2 = min((s for s in dist_t1 if BUTS['g2: detenir le tresor'] <= s), key=lambda s: dist_t1[s])
print(f"\nPlan g1 (balise, h* = {dist_t1[etat_g1]}) :")
for i, a in enumerate(reconstruire(peres_t1, etat_g1), 1):
    print(f"  {i:2d}. {a}")
print(f"\nPlan g2 (tresor, h* = {dist_t1[etat_g2]}) :")
for i, a in enumerate(reconstruire(peres_t1, etat_g2), 1):
    print(f"  {i:2d}. {a}")
Ensemble atteignable : |A_t| = 36 etats  ->  |A_t+1| = 60 etats (+24)

but                               A_t    A_t+1  h*(A_t+1)  delta
g1: balise (5,2)                ECHEC       OK          7  NOUVELLEMENT ATTEIGNABLE
g2: detenir le tresor           ECHEC       OK          6  NOUVELLEMENT ATTEIGNABLE
g3: detenir la cle                 OK       OK          3  

Plan g1 (balise, h* = 7) :
   1. move-est-x0-y0
   2. move-nord-x1-y0
   3. pickup-plank
   4. move-est-x1-y1
   5. move-nord-x2-y1
   6. raft-across-y2
   7. move-est-x4-y2

Plan g2 (tresor, h* = 6) :
   1. move-est-x0-y0
   2. move-nord-x1-y0
   3. pickup-plank
   4. move-est-x1-y1
   5. raft-across-y1
   6. pickup-treasure

Lecture du delta : ce que les trois mesures disent ensemble

  • \(\Delta = \{g_1, g_2\}\) — les deux buts de la rive droite deviennent atteignables ; \(g_3\), le témoin de santé, était déjà atteignable et le reste : l’extension n’a rien cassé.
  • Les plans racontent le coût de la primitive : le plan de \(g_1\) commence par le détour \((0,0) \to (1,0) \to (1,1)\) pour la planchette, et la traversée consomme la planchette — si le but exigeait un retour, il faudrait réinventer. Le plan de \(g_2\) suit le même squelette et s’arrête une case plus tôt : la traversée en rangée 1 atterrit pile sur le trésor \((4,1)\) — un pickup de plus, deux déplacements de moins, d’où \(h^*(g_2) = 6 < h^*(g_1) = 7\).
  • L’espace a grandi, pas la recherche : l’ensemble atteignable passe de 36 à 60 états (+24) — des états de la rive droite existent maintenant, alors que les trois niveaux d’effort du pas 2 énuméraient inlassablement les mêmes 36. C’est la différence entre approfondir \(A_t\) et élargir en \(A_{t+1}\) : le différentiel de Laborit, mesuré.

Et la relaxation ? Dans \(A_{t+1}\), \(h_{max}(g_1)\) devient fini — le monde relaxé suit le vocabulaire, jamais l’inverse.

for nom in ["g1: balise (5,2)", "g2: detenir le tresor"]:
    hm_avant = h_max(INITIAL, BUTS[nom], A_T)
    hm_apres = h_max(INITIAL, BUTS[nom], A_T1)
    hstar1 = min((d for s, d in dist_t1.items() if BUTS[nom] <= s), default=float('inf'))
    print(f"{nom:28s} h_max: A_t={hm_avant if hm_avant != float('inf') else 'inf'} -> A_t+1={hm_apres}"
          f"   h*(A_t+1)={hstar1}   chaine h_max<=h*: {'OK' if hm_apres <= hstar1 else 'VIOLEE'}")
g1: balise (5,2)             h_max: A_t=inf -> A_t+1=7   h*(A_t+1)=7   chaine h_max<=h*: OK
g2: detenir le tresor        h_max: A_t=inf -> A_t+1=6   h*(A_t+1)=6   chaine h_max<=h*: OK

Résumé — le test opérationnel de la strate 7

Pas Mesure Résultat
1. Inatteignabilité vérifiée énumération exhaustive 36 états, \(g_1, g_2\) absents — certificat exact
2. Contrôle d’effort BFS / A*+\(h_{max}\) / IDDFS(24) les trois échouent, même espace : c’est un problème de vocabulaire
3. Primitive nommée raft-across-y{r} coût : planchette consommée + détour \((1,1)\)
4. Delta buts, plans, espace \(\Delta = \{g_1, g_2\}\), plans exhibés (\(h^*\) 7 et 6), l’espace atteignable 36 → 60

Ce que le certificat couvre et ne couvre pas. Le lake garantit les énoncés structurels : \(step \subseteq stepR\) (Strips.lean:58), \(run \subseteq runR\) (Relaxation.lean:56), \(h^+ \le h^*\) (Admissibility.lean:41). Il ne dit rien du choix d’une primitive, ni de l’optimisation du chercheur : ce qui est certifié est la garantie de l’heuristique, ce qui est mesuré ici est l’instance. Les autres sémantiques (préférences, temporalité, incertitude) restent hors de ce certificat comme de cette mesure.

Le protocole, réutilisable. Toute revendication du type « l’agent a appris une nouvelle capacité » passe le même banc : (1) but inatteignable prouvé, (2) l’effort accru échoue, (3) la primitive est nommée et payante, (4) le delta est un ensemble ou un chiffre. Sans le pas 2, chercher davantage et élargir sont indiscernables ; sans le pas 3, le delta ne mesure rien.

Limites et suites

Ce que ce banc ne fait pas, pour être lu honnêtement :

  • Ce n’est pas une étude de solveur. Fast Downward et OR-Tools CP-SAT (Planners-4, Planners-7) traitent des espaces que ce mini-moteur ne peut pas énumérer ; ici, l’énumération exhaustive est précisément l’instrument de mesure — c’est elle qui transforme « on n’a pas trouvé » en certificat. Sur un espace exponentiel, le pas 1 devrait remplacer l’énumération par une preuve d’inatteignabilité (invariants, abstraction) — le protocole reste, l’instrument change.
  • \(h^+\) exact n’est pas calculé — NP-difficile en général ; la chaîne mesurée s’arrête à ses bornes calculables (\(h_{max}\), \(h^*\)). Le companion formel Planners-5b exécute le lemme d’admissibilité dans le kernel Lean lui-même.
  • La synthèse reste hors Lean : ce qui est certifié est la garantie structurelle de la relaxation, pas le choix de la primitive. Un raft-across mal fichu (qui traverserait sans planchette) passerait le même banc — l’exercice 2 montre le versant symétrique : une extension stérile y échoue.

Suite naturelle : le différentiel se généralise en remove-differential (quelle classe de plans disparaît quand on retire une primitive) et en coût-differential (même vocabulaire, coût des actions changé) — le même protocole à quatre pas s’applique, seul le pas 3 change de geste.

Exercices

Exercice 1 — Une primitive gratuite : le deltaplane

Ajoutez l’opérateur deltaplane-y{r} : précondition être en \((0,r)\) (bord gauche), effet atterrir en \((4,r)\), sans planchette. Recalculez \(\Delta\) et \(h^*(g_1)\) avec ce vocabulaire \(A_{t+1}'\). Le delta change-t-il ? Le coût, oui ou non, et pourquoi le pas 3 du protocole exige-t-il de le dire ?

# Exercice 1 a completer : construire A_t1_prime avec deltaplane-y{r}, recalculer
# le delta de buts et h*(g1), puis comparer au radeau.
# A_t1_prime = ...
# result_exo1 = None  # TODO etudiant : (delta, hstar_g1)
result_exo1 = None  # TODO etudiant
print("Exercice 1 a completer : delta et h*(g1) avec le deltaplane.")
Exercice 1 a completer : delta et h*(g1) avec le deltaplane.

Exercice 2 — Une extension stérile : jeter la planchette

Ajoutez l’opérateur discard-plank : précondition holding-plank, effet suppression de holding-plank (rien d’ajouté). Le vocabulaire s’élargit pourtant — mesurez \(\Delta\) et la taille de l’ensemble atteignable. Que démontre ce contre-exemple sur le protocole ?

# Exercice 2 a completer : construire A_t1_sterile = A_t + discard-plank,
# verifier que Delta = ensemble vide et que l'espace atteignable ne change pas.
# result_exo2 = None  # TODO etudiant : (delta, taille_atteignable)
result_exo2 = None  # TODO etudiant
print("Exercice 2 a completer : delta et taille de l'espace avec discard-plank.")
Exercice 2 a completer : delta et taille de l'espace avec discard-plank.

Exercice 3 — La chaîne \(h_{max} \le h^+ \le h^*\) sur \(g_3\)

Sur le but \(g_3\) (détenir la clé), calculez \(h_{max}\) et \(h^*\) dans \(A_t\). Sont-ils égaux ? Trouvez l’argument (en une phrase) qui explique pourquoi la relaxation ne gagne rien sur ce but, alors qu’elle gagnait 5 unités sur le but conjonctif de la rive gauche (\(h_{max} = 3\) contre \(h^* = 8\)).

# Exercice 3 a completer : h_max(g3) et h*(g3) dans A_t, verdict egalite/strict,
# et la phrase d'explication dans explication_exo3.
# result_exo3 = None   # TODO etudiant : (hmax_g3, hstar_g3)
# explication_exo3 = ""  # TODO etudiant
result_exo3 = None  # TODO etudiant
explication_exo3 = ""  # TODO etudiant
print("Exercice 3 a completer : h_max(g3), h*(g3), explication.")
Exercice 3 a completer : h_max(g3), h*(g3), explication.
Retour au sommet