scheme - 如何解释 The Reasoned Schemer 中的 run 5 (x) g0 g1

Question

我不明白 run n (x) g0 g1 ... 如何运行 listo

列表是这样定义的

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

The Reasoned Schemer 第 29 页第 14 段说了代码

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

产生结果

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

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

Answer 1

查询是

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

我添加了准引号 ` 和取消引号 ,，本书为此使用了粗体和非粗体文本:

(<b>run<sup>5</sup></b> (<i>x</i>)
  (<i>list<sup>o</sup></i> <b>(a b c .</b> <i>x</i><b>)</b>))

无论如何 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)。两个查询将产生相同的结果。