如何在 The Reasoned Schemer 中解释 run 5 (x) g0 g1

【问题标题】：How to explain run 5 (x) g0 g1 in The Reasoned Schemer如何在 The Reasoned Schemer 中解释 run 5 (x) g0 g1
【发布时间】：2019-04-05 12:50:24
【问题描述】：

我不明白 run n (x) g0 g1 ... 是如何通过listo来运行的

listo 是这样定义的

(define listo
  (lambda (l)
    (conde
      [(nullo l) #s)]
      [(pairo l)
       (fresh (d)
         (cdro l d)
         (listo d))]
      [else #u])))

第 29 页第 14 节的理性计划者说代码

(run 5 (x)
  (listo (a b c . x)))

产生结果

(()
 (_.0)
 (_.0 _.1)
 (_.0 _.1 _.2)
 (_.0 _.1 _.2 _.3))

你能解释一下这是怎么发生的吗？提前谢谢你。

【问题讨论】：

在前面的 28 页中有很多详细的解释。你审查过那些吗？（这本书看起来很简单，但你不能急于阅读。我经常问“什么？”，需要备份一下。）

标签： scheme reasoned-schemer

【解决方案1】：

查询是

(run 5 (x)
  (listo `(a b c . ,x)))

我添加了 quasiquote ` 和 unquote ,，这本书使用粗体和非粗体文本：

(run⁵ (x)
  (list^o (a b c . x)))

无论如何listo 的工作方式是它尝试检查(nullo `(a b c . ,x)) 并且失败，因此它尝试检查(pairo `(a b c . ,x)) 并且成功。所以它遵循conde 的那个分支并运行

(fresh (d)
     (cdro `(a b c . ,x) d)
     (listo              d))

cdro 产生 d = `(b c . ,x) 所以我们有

(fresh (d)
     ; (cdro `(a b c . ,x) `(b c . ,x))  ;; disappears, has been solved
     (listo                `(b c . ,x)))

所以现在整个过程重复(listo `(b c . ,x)) 然后(listo `(c . ,x)) 然后(listo x)

这也是唯一可以采用的分支，所以(listo `(a b c . ,x))在逻辑上等价于(listo x)。两个查询将产生相同的结果。

【讨论】：