2

我不明白 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))

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

4

1 回答 1

2

查询是

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

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

(run5 (x)
  (listo (a b c . x)))

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

(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). 两个查询将产生相同的结果。

于 2019-04-24T20:08:31.937 回答