sicp - 附加到表单如何工作？ (SICP 的逻辑编程部分)

Question

我目前正在研究 SICP 关于逻辑编程的部分，但我被困在有关逻辑推导的示例中，尤其是附加到表单规则。它们是如何工作的？我不太明白的是第二条规则是如何取消第一个列表的。例如，给定:

(规则(附加到表单()？y？y))

(规则(追加形式(？u。？v)？y(？u。？z)) (追加形式 ?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

通过拿一张纸写下每一步来玩翻译。对于每一步，您都记下触发/可以触发的规则以及将哪个变量绑定(bind)到哪个值。

例如:

(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 列表一样。

这些绑定(bind)应用于规则的主体 (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)) 绑定(bind) ?z_3 到 (c d)。然后递归开始，?z_2 被定义为 (b . ?z_3)，?z 被定义为 (a . ?z2)

原始查询 (append-to-form (a b) (c d) ?z) 被应用于其中 ?z = (a . (b . (c d))) 和返回 (append-to-form (a b) (c d) (a b c d))

剩下的练习留给读者;)

这里的关键概念是模式匹配和统一，可以在 section 4.2.2 找到。 .整个查询求值器确实是 SICP 中最难的部分，所以不要气馁。这是非常值得的努力。尝试运行代码(在 R5RS 方案中)并修改它，例如添加跟踪。