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

Question

我试图理解 SICP 此处

特别是，在“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)))))

相关注释指出：

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

但是，我想不出实际上有必要这样做的情况。

我认为正在谈论的是，当前可能存在以下帧绑定：

{?y = 4}

然后被要求将绑定从 ?z “extendIfPossible” 到 ?y。

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

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

注意，如果 ?z had 已经绑定到其他东西，那么代码不会到达标记为“*”的部分（我们已经递归到与 ?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 } 。

框架中的循环绑定是不好的，因为它们可能会导致使用框架执行替换的函数（例如实例化）在无限循环中运行。

Answer 2

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