SICP统一算法中看似不必要的情形

我试图理解SICP中描述的统一算法 here

特别是,在“如果可能的话扩展”过程中,有一个检查(第一个用asterix“*”标记的位置)正在检查右侧的“表达式”是否是一个已绑定到当前帧中某个内容的变量:

(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)))))

相关评论指出:

“在第一种情况下,如果我们尝试匹配的变量没有绑定,但我们尝试匹配的值本身是一个(不同的)变量,则需要检查该值是否绑定,如果绑定,则需要检查该值是否匹配其值。如果比赛双方都未绑定,我们可以将其中一方绑定到另一方。”

但是,我想不出有必要这样做的情况。

它在说什么,我 认为 ,是当前可能存在以下帧绑定的位置:

{?y = 4}

然后被要求“扩展”一个绑定?Z到?是的。

当被要求延期时,是否有“*”支票?Z“与”?是的,“我们看到了”?Y“已经绑定到4,然后递归地尝试统一”?Z“with”4“,which results with us extending the frame with”?z=4”。

如果没有检查,我们最终会用“?Z=?是的。但在这两种情况下,只要?Z还没有绑定到其他东西上,我看不出问题所在。

注意,如果?Z 有 已经绑定到其他东西上,那么代码就不会到达标记为“*”的部分(我们应该已经递归到与什么相统一了?z已经匹配了)。

在仔细考虑之后,我意识到可能会有一些关于生成“最简单”的mgu(最通用的unifier)的论点。例如,您可能需要一个具有引用其他变量的最小变量数的MGU…也就是说,我们更愿意生成替换?X=4,?Y=4比替代物?X=?是的,?Y=4…但是我不认为这个算法在任何情况下都能保证这种行为,因为如果你要求它统一“(?x 4)“带”(?是吗?y)“那么你最终还是会得到?X=?是的,?Y=4。如果行为不能得到保证,为什么还要增加复杂性呢?

我的推理是正确的吗?如果没有,则需要“*”检查来生成 对的 MGU?