Cas apparemment inutile dans l'algorithme d'unification dans SICP
-
22-07-2019 - |
Question
J'essaie de comprendre l'algorithme d'unification décrit dans SICP ici
En particulier, dans la procédure "extend-if-possible", il y a un contrôle (le premier endroit marqué d'un astérisque "*") qui vérifie si l'expression "expression" de droite est est une variable déjà liée à quelque chose dans le cadre actuel:
(define (extend-if-possible var val frame)
(let ((binding (binding-in-frame var frame)))
(cond (binding
(unify-match
(binding-value binding) val frame))
((var? val) ; *** why do we need this?
(let ((binding (binding-in-frame val frame)))
(if binding
(unify-match
var (binding-value binding) frame)
(extend var val frame))))
((depends-on? val var frame)
'failed)
(else (extend var val frame)))))
Le commentaire associé indique:
" Dans le premier cas, si la variable que nous essayons de faire correspondre n'est pas liée, mais que la valeur à laquelle nous essayons de faire correspondre est elle-même une variable (différente), il est nécessaire de vérifier si la valeur est lié, et si oui, à correspondre à sa valeur. Si les deux parties ne sont pas liées, nous pouvons nous associer l’une à l’autre. "
Cependant, je ne peux pas penser à un cas où cela est réellement nécessaire.
Ce dont il est question, je pense que , est l'endroit où vous pourriez avoir les liaisons de trame suivantes:
{?y = 4}
Et on vous demande ensuite de "prolonger si possible". une liaison de? z à? y.
Avec cela " * " chèque présent, lorsqu’il est demandé de prolonger "?? z " avec "? y", nous voyons que "? y" est déjà lié à 4, puis essayez de manière récursive d’unifier "& z;"? z " avec "4", ce qui nous oblige à prolonger le cadre avec "? z = 4".
Sans cette vérification, nous étendrions le cadre avec juste "? z =? y". Mais dans les deux cas, tant que? Z n'est pas déjà lié à autre chose, je ne vois pas le problème.
Remarque: si? z avait déjà été lié à autre chose, le code n'atteint pas la partie marquée "" *". (nous aurions déjà eu recours à l’unification avec quoi? z avait déjà été apparié).
Après réflexion, je me suis rendu compte qu'il pourrait y avoir une sorte d'argument pour générer un "plus simple" MGU (Unifier le plus général). par exemple. vous voudrez peut-être une MGU avec un nombre minimal de variables faisant référence à d'autres variables ... c'est-à-dire que nous préférons générer la substitution {? x = 4,? y = 4} plutôt que la substitution {? x =? y,? y = 4} ... mais je ne pense pas que cet algorithme garantirait ce comportement de toute façon, car si vous lui demandiez d'unifier "(? x 4)" avec " (? y? y) " alors vous vous retrouveriez toujours avec {? x =? y,? y = 4}. Et si le comportement ne peut pas être garanti, pourquoi cette complexité supplémentaire?
Est-ce que mon raisonnement est correct? Si ce n’est pas le cas, c’est quoi un contre exemple où le " * " vérification est nécessaire pour générer un correct MGU?
La solution
C'est une bonne question!
Je pense que la raison en est que vous ne voulez pas vous retrouver avec des liaisons circulaires telles que {? x =? y,? y =? x}
. En particulier, unifier (? X? Y)
avec (? Y? X)
vous donnerait le cadre circulaire ci-dessus si vous avez omis la vérification. Avec le chèque, vous obtenez le cadre {? X =? Y} comme prévu.
Les liaisons circulaires dans un cadre sont incorrectes, car elles peuvent entraîner l'exécution de substitutions à l'aide du cadre, telles que instancier
, pour s'exécuter dans une boucle infinie.
Autres conseils
Sans cela, vous n'obtiendrez pas l'unificateur le plus général . Il y aurait encore du travail à faire: unifier x et y.