附加到表单如何工作？ （SICP 的逻辑编程部分）

Question

我目前正在学习 SICP 的逻辑编程部分，但我陷入了有关逻辑推论的示例中，尤其是附加到表单规则。它们如何工作？我不太明白的是第二条规则 cdr-downs 第一个列表是如何的。例如，给定：

(rule (append-to-form () ?y ?y))

(rule (append-to-form (?u . ?v) ?y (?u . ?z)) (append-to-form ?v ?y ?z))

a) 我们如何到达：

;;; Query input:
(append-to-form (a b) (c d) ?z)

to

;;; Query results:
(append-to-form (a b) (c d) (a b c d))

b) 这个怎么样：

;;; Query input:
(append-to-form (a b) ?y (a b c d))

to

;;; Query results:
(append-to-form (a b) (c d) (a b c d))

c) 最后：

;;; Query input:
(append-to-form ?x ?y (a b c d))

to

;;; Query results:
(append-to-form () (a b c d) (a b c d))
(append-to-form (a) (b c d) (a b c d))
(append-to-form (a b) (c d) (a b c d))
(append-to-form (a b c) (d) (a b c d))
(append-to-form (a b c d) () (a b c d))

我对执行该规则所需的具体心理步骤感兴趣匹配。

先感谢您。

Answer 1

拿一张纸并写下每一个步骤来扮演口译员的角色。对于每一步，您都写下哪个规则被触发/可以被触发以及哪个变量绑定到什么值。

例如：

(append-to-form (a b) (c d) ?z)

触发规则

(rule (append-to-form (?u . ?v) ?y (?u . ?z)) 
  (append-to-form ?v ?y ?z))

注意

?u = a, ?v = (b), ?y = (c d), ?z = (a . ?z_2)

：原始查询中的?z 应该是与规则主体中的?z 不同的变量，因此将规则的?z 重命名为?z_2。列表 (1 2 3) 与 (?a . ?b) 匹配时会生成 ?a = 1, ?b = (2 3)，就像 car/cdr'ing 列表时一样。

这些绑定应用于规则的主体 (append-to-form ?v ?y ?z) 因此，我们

(append-to-form (b) (c d) ?z_2)

再次

(append-to-form () (c d) ?z_3)

得到并触发不同的规则： (rule (append- to-form () ?y ?y)) 将 ?z_3 绑定到 (cd)。
然后递归开始，?z_2 被定义为 (b . ?z_3)，?z 被定义为 (a . ?z2)

原始查询 (append-to-form (ab) (cd) ?z)< /code> 应用于 ?z = (a . (b . (cd))) 的绑定并返回 (append-to-form (ab) (cd) (abcd))

其余的练习留给读者；）

这里的关键概念是模式匹配和统一，可以在 第 4.2.2 节。整个查询评估器确实是 SICP 中最困难的部分，所以不要灰心。这是非常值得的。尝试运行代码（在 R5RS 方案中）并修改它，例如添加跟踪。