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

Question

我正在尝试理解 SICP here 中描述的统一算法

特别是，在“extend-if-possible”过程中，有一个检查（第一个用星号“*”标记的地方）检查右手“表达式”是否是一个已经绑定的变量到当前帧中的某物：

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

然后被要求“扩展IfPossible”从 ?z 到 ?y 的绑定。

有了“*”检查，当被要求用“?y”扩展“?z”时，我们看到“?y”已经绑定到4，然后递归地尝试将“?z”与“ 4"，这导致我们用 "?z = 4" 扩展框架。

如果没有检查，我们最终会用“?z = ?y”来扩展框架。但在这两种情况下，只要 ?z 还没有绑定到其他东西，我就看不到问题所在。

注意，如果 ?z 已经绑定到其他东西，那么代码不会到达标记为“*”的部分（我们已经递归到与 ?z 已经是匹配）。

经过深思熟虑，我意识到生成“最简单”的 MGU（最通用统一器）可能存在某种争论。例如您可能想要一个具有最少数量的变量引用其他变量的 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）在无限循环中运行。

Answer 2

没有它，您将无法获得最通用的统一器。还有很多工作要做：统一 x 和 y。