似乎不必要的情况下，在统一的算法在sic颗粒

Question

我试着去理解的统一描述的算法在sic颗粒 在这里，

特别是，在手术过程"延伸如果可能的"，有一个检查(第一位标有星号"*")，这是检查看看右手"表达"是一个可变的，是已经绑来的东西在目前的框架：

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

与"*"检查本，当被要求延长"?z"与"?y"，我们看到，"?y"已经开4，然后递归尝试统一"?z"与"4"，其结果我们延伸的框架与"?z=4".

不检查，我们将最终延伸框架只有"?z=?y"。但在这两种情况下，这么久？z是不是已经开到别的东西，我没有看到这个问题。

注意，如果？z 已 已经开到别的东西，然后代码没有达到该部分的标记"*"(我们已经recursed到统一的什么？z已经匹配)。

后经想过了，我已经意识到，可能有某种参数，用于产生一个"简单的"闭塞(最一般的统一).例如你可能会想要一个闭塞，以最少数量的变量参照其他变量...也就是说，我们宁愿产生的替代{?x=4,?y=4}比的替代{?x=?y?y=4}...但我不认为这种算法将保证这种行为在任何情况下，因为如果你问到统一"(?x4)"与"(?y?y)"然后你仍然会结束了{?x=?y?y=4}.如果该行为不能得到保证，为什么附加的复杂性？

是我推理在这里所有正确的吗？如果不是，什么是反的例子"*"检查是必要的，以产生一个 正确的 闭塞?

Answer 1

这是一个好问题！

我想原因是你不想与圆形绑定，例如{ ?x = ?y, ?y = ?x }结束了。特别是，(?x ?y)统一(?y ?x)会给你上面，如果你省略了检查圆形框架。与被检查，则得到预期的帧{X =？Y}。

在帧

圆形绑定是坏的，因为它们可能导致功能使用帧，如instantiate，以无限循环运行时执行置换。

Answer 2

如果没有它，你不会得到的最常规合一。有好多仍然是一个要完成的工作：统一x和y