L'unification : filtrer et lier, en un geste

D'où viennent les valeurs des variables ? De l'unification : le geste par lequel Fix fait coïncider ta question avec un fait (ou une tête de règle), en liant les variables au passage. Filtrer et lier, d'un coup.

Un programme avec des termes structurés :

pt(coord(1, 2)).
pt(coord(3, 4)).

Filtrer dans la structure

?- pt(coord(X, Y)).
X = 1, Y = 2
X = 3, Y = 4

coord(X, Y) ne matche que ce qui a la même forme — un coord à deux arguments — et lie X, Y aux valeurs trouvées. L'unification descend dans le terme : elle ne compare pas des chaînes, elle fait correspondre des structures.

Fixer une partie, chercher le reste

Tu peux figer une position et laisser l'autre libre :

?- pt(coord(1, Y)).
Y = 2

Le 1 doit coïncider (il n'y a qu'un coord(1, …)), et Y se lie à ce qui reste. La même opération sert donc à la fois à contraindre et à découvrir — c'est ce qui rend les requêtes réversibles.

Le mécanisme sous tout le reste

L'unification n'est pas réservée aux requêtes : c'est elle qui fait avancer chaque règle. Quand impacte(S, T) :- depend(S, T) s'applique, c'est l'unification qui fait correspondre depend(S, T) aux faits et propage S, T dans la tête. Le moteur ne fait, à la base, que ça — unifier, encore et encore, jusqu'au point fixe.

Premier ordre, avec occurs-check

L'unification de Fix est du premier ordre : on unifie des données (atomes, nombres, termes composés), pas des prédicats ni des fonctions. Et une variable ne peut pas se lier à un terme qui la contient elle-même (l'occurs-check) — ce qui interdit les termes infinis et garde le tout sain.

Les bords honnêtes

• Premier ordre seulement : pas d'unification d'ordre supérieur (pas de variable en position de prédicat).
• L'occurs-check est actif : X ne s'unifie pas avec f(X).

À côté

• Interroger — l'unification vue depuis les questions et leurs modes.
• :help unification — la fiche, dans le REPL.
• Référence : fiches — commandes, builtins, concepts.