Clojure.logic 与 The Reasoned Schemer 的区别

Posted 2023-05-08

【中文标题】Clojure.logic 与 The Reasoned Schemer 的区别

【英文标题】：Clojure.logic difference with The Reasoned Schemer

【发布时间】：2013-07-07 01:47:56

【问题描述】：

我一直在使用 Clojure.logic 处理 The Reasoned Schemer (TRS) 并关注 differences documented here。我到达了第 3 章的第 24 帧，TRS 报告了这一点

(run 5 [x]
  (lolo '((a b) (c d) . x)))

应该产生

'(()
  (())
  (() ())
  (() () ())
  (() () () ())

现在，我实现了 `lolo as

(defn lolo
  "Succeeds if l is a list-of-lists."
  [l]
  (conde
   ((emptyo l) s#)
   ((fresh [a]
           (firsto l a)
           (listo a)) (fresh [d]
                             (resto l d)
                             (lolo d)))
   (s# u#)))

这会产生以下奇怪的结果：

'(()
  (())
  ((_0))
  (() ())
  ((_0 _1)))

这基本上意味着我的 lolo 正在生成泄漏出新变量的解决方案。如果我继续前进，试图看到一个模式，我会得到

'(()
  (())
  ((_0))
  (() ())
  ((_0 _1))
  (() (_0)
  ((_0) ())
  (() () ())
  ((_0 _1 _2)))

但我在迷雾中看不清楚，希望能对此有所了解。这是我lolo的一个错误吗？它是 clojure.logic 中的错误吗？ TRS 中的求解器和 clojure.logic 中的求解器之间存在合理的区别吗？我如何解释或使用结果？如何在心理上预测 clojure.logic 的结果？

【参考方案1】：

正如您链接到的 core.logic wiki 页面上所述，core.logic 的 conde 是 TRS 的 condi。不同之处在于 TRS 的 conde 按顺序尝试子句，而 condi 交错结果流。所以 core.logic 版本会产生 TRS 中显示的所有结果，但在它们之间，它会返回 miniKanren 永远无法处理的其他结果。

您较长的答案中的一个相关模式是，如果您从(()) 开始每隔一个结果取一个结果，那么结果序列的子序列看起来就像在每个单独结果前面加上() 的整个结果序列。这是由于交错 - 在这个子序列上，() 被选为结果的第一个元素，然后 lolo 递归生成其余部分。