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

Question

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

13

我正试图理解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}

然后被要求“如果可能”的扩展从?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？

- Paul Hollingsworth

2个回答

0

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

- Thomas Danecker

定义“最一般”是什么意思？如何理解 { ?x = ?y, ?y = 4 } 比 { ?x = 4, ?y = 4 } 更一般？对于第一个式子，不存在绑定 x 和 y 的情况满足它而不满足第二个式子。 - Paul Hollingsworth

是的，你说得对，这与“最一般”的统一无关。我在这里混淆了变量和值的定义：http://www.cs.ualberta.ca/~you/courses/325/Mynotes/Log/unif.html实际上，我还没有看到过不尝试尽可能多地统一的实现... - Thomas Danecker

如果你在中途停止，它还能被称为统一吗？我记得我的逻辑编程教授会扣分，如果你没有尽可能地统一所有内容。 - Thomas Danecker

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- namin · Accepted Answer

这是一个很好的问题！

我认为原因在于你不想得到循环绑定，比如 { ?x = ?y, ?y = ?x }。特别地，如果省略检查，将 (?x ?y) 与 (?y ?x) 统一会给你上面的循环框架。有了检查，你会得到预期的框架 { ?x = ?y }。

帧中的循环绑定是不好的，因为它们可能导致使用该帧进行替换的函数（例如 instantiate）运行在无限循环中。