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

Question

我试图在这里理解SICP中描述的统一算法

特别是,在"尽可能扩展"的过程中,有一个检查(标有星号"*"的第一个地方),它检查右手"表达式"是否是已经绑定到某个东西的变量.当前帧:

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

然后要求"extendIfPossible"绑定从？z到？y.

当出现"*"检查时,当被要求用"？y"扩展"？z"时,我们看到"？y"已经绑定到4,然后递归地尝试将"？z"与"4"统一,这导致我们用"？z = 4"扩展框架.

没有检查,我们最终只用"？z =？y"扩展框架.但在这两种情况下,只要？z还没有被其他东西绑定,我就没有看到问题.

请注意,如果- Z 就已经被绑定到别的东西,然后代码没有达到部分标有"*"(我们早就递归到什么？ž统一已经匹配).

经过深思熟虑之后,我意识到可能存在某种形式的争论,即生成一个"最简单"的MGU(Most General Unifier).例如,您可能希望MGU具有引用其他变量的最少数量的变量...也就是说,我们宁愿生成替换{？x = 4,？y = 4}而不是替换{？x =？y, ？y = 4} ...但我认为这种算法在任何情况下都不会保证这种行为,因为如果你要求它将"(？x 4)"与"(？y？y)"统一起来,那么你会仍以{？x =？y,？y = 4}结束.如果行为无法保证,为什么额外的复杂性呢？

我在这里的推理都是正确的吗？如果没有,那么生成正确的 MGU 需要"*"检查的反例是什么？

Answer 1

这是个好问题!

我认为原因是你不想最终得到诸如的循环绑定{ ?x = ?y, ?y = ?x }.特别是,统一(?x ?y)使用(?y ?x)会给你上面,如果你省略了检查圆形框架.通过检查,您可以获得预期的帧{？x =？y}.

帧中的循环绑定很糟糕,因为它们可能导致使用帧执行替换的函数,例如instantiate,在无限循环中运行.