La terminaison : une garantie, et son prix

« Le calcul s'arrête toujours » est la première promesse de Fix. Ce n'est pas un vœu : c'est une propriété vérifiée à la compilation. Cette page explique ce que le vérificateur regarde, pourquoi il refuse parfois un programme qui aurait pourtant terminé, et comment réécrire quand ça arrive.

D'où vient la garantie

Fix sature : il applique tes règles jusqu'au point fixe. Ça termine si l'univers des faits dérivables est fini. Pour la logique pure, c'est acquis — une règle recombine des valeurs qui existent déjà. Le seul danger vient du calcul : une règle qui fabrique des valeurs nouvelles à chaque tour peut grossir sans fin.

compteur(0).
compteur(M) :- compteur(N), N < 5, add(N, 1, M).   % ✗ refusé

add(N, 1, M) produit un M qui n'existait pas. Le vérificateur suit ce flux dans un graphe de positions : chaque argument de chaque prédicat est un nœud, chaque règle trace des arêtes, et une arête est marquée croissante quand la valeur qui la traverse grandit. Une arête croissante qui boucle sur elle-même → refus :

fix: terminaison non prouvable : règle croissante compteur (position 0)
    → :help termination

Le refus est conservateur — et c'est voulu

Tu l'as remarqué : le compteur ci-dessus termine (la garde N < 5 le borne). Le vérificateur le refuse quand même, parce qu'il ignore les gardes : prouver qu'une garde arithmétique borne une croissance est indécidable en général, et Fix préfère un critère simple et sûr à une analyse savante et faillible.

La règle du jeu est donc asymétrique, et honnête :

• ce que Fix accepte termine — c'est le contrat ;
• ce que Fix refuse n'est pas forcément divergent — il y a des faux positifs, et le compteur borné en est l'exemple canonique.

Une nuance connue côté « accepte » : l'accumulation récursive à travers une jointure (cout(X, Z, C) :- cout(X, Y, C1), arc(Y, Z, C2), add(C1, C2, C).) passe la garde alors que sa terminaison dépend des données (une infinité de chemins si arc a un cycle). Le moteur la rattrape à l'exécution : budget de travail borné + certificat Bellman-Ford ⟹ erreur explicite en temps borné (« évaluation incomplète »), jamais un calcul sans fin (BUG-044, volets runtime fermés). La forme recommandée reste la relaxation (voir Recettes) : elle termine, cycles compris (poids ≥ 0).

Il n'y a pas de drapeau pour passer outre : la réponse à un refus est une réécriture, pas un contournement.

La réécriture : descendre au lieu de monter

La forme décroissante est toujours acceptée : pars de la borne et descends. La descente s'arrête d'elle-même à 0 — plus besoin que le vérificateur fasse confiance à une garde.

compteur(5).
compteur(M) :- compteur(N), N > 0, sub(N, 1, M).   % ✓ accepté

?- compteur(X).
X = 0
X = 1
...
X = 5

Même relation, mêmes six faits — la borne (5) est simplement devenue le point de départ au lieu d'un plafond à surveiller. C'est le réflexe à acquérir : quand une règle croissante est refusée, cherche la borne qu'elle visait, et fais-en l'origine d'une descente.

Le même besoin se couvre aussi, souvent, par un générateur de domaine — un prédicat de faits qui énumère les valeurs licites, testé ensuite par la garde (voir Bonnes pratiques).

Ce qui ne risque rien — et le piège du terme construit

Les règles qui recombinent des valeurs existantes passent sans y penser : chemins, fermetures transitives, jointures — aucune valeur neuve n'y naît.

impacte(S, T) :- depend(S, T).
impacte(S, T) :- impacte(S, U), impacte(U, T).   % ✓ recombine, ne fabrique pas

Le piège, c'est qu'une règle peut fabriquer autre chose que des nombres : un terme. Une tête récursive qui construit un terme plus gros que ce que le corps fournit est croissante au même titre :

has_type(cons(H, T), list(int)) :- has_type(H, int), has_type(T, list(int)).
% ✗ refusé : règle croissante has_type (position 0)

La sortie est la même que pour le compteur : donner un nom aux objets et relier leurs types, au lieu de construire le terme en tête. C'est le geste des types dépendants (matmul(A, B, matrix(T, R, C)) :- …) — le terme dérivé vit dans son propre prédicat, les objets sont nommés par des faits. Voir Les types dépendants et, pour les données, un ADT déclaré (type list(T) = nil | cons(T, list(T)).) dont les faits ground sont vérifiés sans qu'aucune règle croissante soit nécessaire.

Les bords honnêtes

• Le critère est conservateur : il rejette des programmes qui terminent (compteur borné). C'est le prix d'une garantie sans exception.
• Les gardes (N < 5) ne sont pas prises en compte par le vérificateur — elles filtrent à l'exécution, elles ne prouvent rien à la compilation.
• Un domaine véritablement non borné (« pour tout entier ») est hors de portée par nature : aucune saturation ne peut énumérer un ensemble infini.

À côté

• Bonnes pratiques — le générateur de domaine, l'autre moitié du réflexe.
• Comprendre — la terminaison dans le tableau d'ensemble du point fixe.