我试图理解这里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)))))
相关评论指出：
“在第一种情况下，如果我们尝试匹配的变量未绑定，但我们尝试匹配的值本身是一个（不同的）变量，则有必要检查该值是否已绑定，并且“
但是，我想不出实际上有必要这样做的情况。
我认为它在谈论的是您当前可能存在以下框架绑定的地方：
{?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 的反例是什么？