将插入事实从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].

因此，第二个可检查项实际上应该是

(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))