mini-Kanren，core.logic，clojure：推理方案练习60答案

【问题标题】：mini-Kanren, core.logic, clojure: Reasoned Scheme Exercise 60mini-Kanren，core.logic，clojure：推理方案练习60
【发布时间】：2012-06-05 08:46:29
【问题描述】：

这不是家庭作业——解决方案已经在文本中。我只是无法理解解决方案。

问题

(run* (q)
  (let [a (== true q)
        b (== false q)]
    b))

正确的解决方案

(false)

我相信的解决方案

()

我的困惑

显然“a (== true q)”行没有被执行，因为只有 b 是目标。这让我很困惑。到目前为止，我的逻辑编程心智模型是：

考虑所有可能的分配给 q
输出设法通过整个程序的那些

因此，“a (== true q)”强制 q = true，从而无法满足“b (== false q)”这一行。

但是，显然只执行“计算目标所需的事情”。这是怎么回事？ core.logic / mini-kanren 的正确心理执行模型是什么？

谢谢

（顺便说一句，我显然错了，因为 mini-karen + core.logic 彼此一致——我只是想了解我做错了什么。）

【问题讨论】：

当你的目标是达到目标时，最好留下一些与你的目标无关的东西来达到目标
@Ankur：你可能是对的。但是，我不明白。您能否提供一些关于“让”如何适合迷你 kanren / core.logic 的执行模型的见解？很明显，我不明白“让”是什么意思——很明显，“让”在纯方案/clojure 中的含义是别的。

标签： clojure logic minikanren clojure-core.logic

【解决方案1】：

== 产生一个目标。但是你没有通过a 目标来运行。所以run对此一无所知。类似的情况是这样的：

(defn call [f] (f))

(call
  (let [a #(println "a")
        b #(println "b")]
    b))

a 函数已创建但未传递给 call。所以它永远不会被执行。

【讨论】：

现在这很有意义，尽管在 repl 上胡闹，但我没有意识到 == 返回的函数。 [我认为这只是使 core.logic 工作的一些奇怪的类型/宏技巧。]