3

我正在尝试使用 clojure.core.logic 解决 Smullyan 的 To Mock a Mockingbird 中的第一个难题，不是因为它特别难，而是作为一种练习。谜题说有一个花园，有三种颜色的花：红色、黄色和蓝色。每种颜色至少出现一次，无论您采摘哪三朵花，其中都会有一朵红色和一朵黄色。问题：第三个一定是蓝色的吗？
逻辑代码的基本骨架非常简单：

(run 5 [flowers]
   (counto flowers 3)
   (containso flowers [:red :yellow])
   (fresh [garden]
          (containso garden [:red :yellow :blue])
          (containso garden flowers)
          (forall [flower-selection] (...))))

counto并containso手动实现并做显而易见的事情。我是新手，所以我可能缺少现有的库支持。重要的一行是以 . 开头的那一行forall。forall基本上是我希望存在的，但似乎找不到。我知道的唯一可以放在这个地方的构造是fresh。但fresh本质上执行存在量化∃。我在这里想要的是全称量化∀。
我对可以选择包含红色和黄色的三朵花的花园不感兴趣。我对一个必然导致这种选择的花园感兴趣。

4

1 回答 1

2

即使有一个forall，这种方法也行不通，因为花园可以任意大，并且测试无限花园中三朵花的所有组合将花费无限的时间。

即使你这样做了，你仍然不会完成，因为你只证明了存在一个满足这个属性的花园：你还没有证明所有满足初始条件的花园也满足这个属性。

core.logic“只是”一种建模搜索问题的方法，可以轻松修剪搜索空间中无趣的子树。如果您试图证明关于无限搜索空间的通用陈述，则需要以某种方式进行修剪以限制搜索空间的最大大小。对于这个问题，我在 core.logic 中看不到任何明显的方法，没有更多地考虑原始问题，这当然会直接导致解决方案，根本不需要 core.logic。

于 2017-06-13T17:23:13.660 回答