logic-programming - 不理解 The Reasoned Schemer 第 5 章第 62 帧

Question

我目前正在通过学​​习 The Reasoned Schemer 来学习 miniKanren。

而我卡在第5章第62帧的练习中:(run* (x) (flatten_o (a) x))，为什么输出的是三个列表？

Answer 1

好问题!这些额外的列表从何而来？？？

问题出在 flatteno 定义的 else 子句中。 else 子句处理 s 是符号的情况(这里是符号 a)。但是，该子句还允许 s 为空列表或一对!这就是为什么我们看到三个列表而不是一个列表的原因——额外的两个列表是由递归调用生成的，这些调用由于 else 子句接受 s 的非符号值而成功.

在后来的 miniKanren 版本中，我们添加了特殊的约束，例如 symbolo 和 =/= 来防止这种行为。例如，下面是用 faster-miniKanren ( https://github.com/webyrd/faster-miniKanren ) 编写的相同查询和 flatteno:

(define flatteno
  (lambda (s out)
    (conde
      ((== '() s) (== '() out))
      ((fresh (a d res-a res-d)
         (== (cons a d) s)
         (flatteno a res-a)
         (flatteno d res-d)
         (appendo res-a res-d out)))
      ((symbolo s) (== (cons s '()) out)))))

(run* (x)
  (flatteno '(a) x))
=>
((a))

注意在 flatteno 中使用 symbolo 约束来确保 s 是一个符号。

您可以在本文中找到这些约束的非“小书”解释:

http://webyrd.net/quines/quines.pdf

我们正试图弄清楚如何将这些约束的描述包含在小书本格式中。约束的实现有点复杂，很难写进小书里!

希望这对您有所帮助!

干杯，

--将