将插入事实从 Prolog 转换为 core.logic

Question

我正在玩弄 core.logic 并尝试翻译一些 Prolog 代码并遇到insert 事实的无限递归（取自 R.A.O'Keefe 的“Prolog 工艺”）：

 insert(L, X, [X|L]).
 insert([H|T], X, [H|L]) :-
        insert(T,X,L).

这是我到目前为止提出的（请注意前两个参数被交换以匹配conso参数列表）：

 (defn insert [x l nl]
    (conde
      [(conso x l nl)]
      [(fresh [h t]
         (conso h t l)
         (insert x t l)
         (conso h l nl))]))

我遇到的问题是这些 midje 测试的最后两个事实永远不会返回。 第一个按预期工作得很好，因为这只需要第一个 conso 子句。

   (fact "Inserting works"
         (run* [q] (insert 1 [2] q)) => '((1 2)))
         (run* [q] (insert 1 [2 3] q)) => '((1 2 3)))
   (fact "We can retrieve the inserted data"
         (run* [q] (insert q [2] '(1 2))) => '(1))
   (fact "We can retrieve the list data, too"
         (run* [q] (insert 1 q '(1 2))) => '((2))))

我想我忽略了一些明显的东西，但是什么？

编辑：事实没有正确反映 Prolog 代码的行为。正确的行为是这样的：

   ?- insert([2,3], 1, Q).
   Q = [1, 2, 3] ;
   Q = [2, 1, 3] ;
   Q = [2, 3, 1].

所以，第二个checkable实际上应该是

 (fact "Inserting works"
       (run* [q] (insert 1 [2 3] q)) => '((1 2 3) (2 1 3) (2 3 1)))

Answer 1

解决办法是把递归插入子句放在最后：

(defn insert [x l nl]
    (conde
      [(conso x l nl)]
      [(fresh [h t]
         (conso h t l)
         (conso h l nl)
         (insert x t l))]))

Answer 2

Prolog 代码几乎可以逐字转录，因为 core.logic 也支持匹配。

(defne inserto [L, X, L*] 
    ([L, X, (X . L)]) 
    ([(H . T), X, (H . L)] (inserto T, X, L)))

请注意，我保留了 Prolog 版本的顺序，而不是您版本中前两个逻辑变量的倒序。

user=> (run* [q] (inserto [2] 1 q))
((1 2))
user=> (run* [q] (inserto [2 3] 1 q))
((1 2 3))
user=> (run* [q] (inserto [2] q [1 2]))
(1)
user=> (run* [q] (inserto q 1 [1 2]))
((2))