Unification dans Prolog

Question

Ceci est une question d'un examen passé sur l'unification dans Prolog. nous étions supposés dire s'ils étaient unifiés et ensuite les instanciations.

f(a,g(b,a)) and f(X,g(Y,X)) 

Cette unifie tout à fait a = X, g (b, a) = g (Y, X) et est tout à fait en avant

f(g(Y),h(c,d)) and f(X,h(W,d)) 

Je ne pense pas directement celui-ci unifie en raison de g (Y) =/X, bien que h (c, d) s'unifie avec h (W, d). Est-il possible que X = g (Y) puisque les majuscules X regardent jusqu'à trouver une solution?

Answer 1

Oui, il unifie, et il le fait parce que g(Y) est un terme à évaluer, ainsi que a - dans le premier exemple que vous avez pointé.

Vous pouvez vérifier l'évaluation dans un interpréteur Prolog:

?- f(g(Y),h(c,d)) = f(X,h(W,d)). 
X = g(Y), 
W = c. 

Le processus d'unification travaille dans une profondeur d'abord la mode, les membres d'unifier et de retourner chacun la réponse disponible, jusqu'à ce qu'aucune autre combinaison est possible.

Cela signifie que la méthode d'unification est appelé à f(g(Y),h(c,d)) = f(X,h(W,d)), qui trouve les appariements disponibles: g(Y) = X, h(c, d) = h(W, d).

Ensuite, l'unification est effectuée sur g(Y) = X, cela, puisqu'il n'y a pas d'autre réduction possible, renvoie X = g(Y).

Ensuite, la même méthode est appelée h(c, d) = h(W, d) correspondant, ce qui vous donne c = W, et aucune autre correspondance, résultant, ainsi, W = c. Les réponses, après l'unification, sont renvoyées, et false est généralement renvoyé pour indiquer qu'aucune correspondance/correspondance supplémentaire n'est possible. Comme l'indique CapelliC, la variable Y, après le processus d'unification, n'est toujours pas liée. L'unification est effectuée sur des variables non liées, ce qui signifie:

• l'unification des h(c, d) = h(W, d) retours h(_) = h(_), et cela permet l'unification de continuer, puisque h est un terme, et non un var non lié; L'unification de d = d est une correspondance de termes, et ne forme pas une attribution - ou une liaison;

• l'unification des c = W formes d'attribution et la W variable est liée à l'expression c, car il n'a pas été tenu avant - une comparaison sera effectuée autrement;

• l'unification de X = g(Y) lie simplement la variable X non liée au terme g(Y) et g(Y) est un terme avec une variable non liée, car il n'y a pas d'unification disponible pour g(Y).

Cordialement!