なぜこのsortoの実装は終了しないのですか？

Question

私はロジックプログラミングの初心者です。

私はこのようなソート関係を実装しようとしています：

(sorto [3 2 1][1 2 3]) -> #s

のClojureとcore.logic使用I'am：これは中に終了することができない理由を私は理解していない

をほとんどの場合。

ご意見ありがとうございます。

(require '[clojure.core.logic :refer :all] 
     '[clojure.core.logic.fd :as fd]) 

まず、私はいくつかの小さなヘルパーを定義します。

簡単なカウント関係：(counto [a b] 2) -> #s

(defne counto [list n] 
     ([() 0]) 
     ([[fl . rl] _] 
     (fresh [nnxt] 
       (fd/- n 1 nnxt) 
       (counto rl nnxt)))) 

を削減し、すべての？リレーショナル当：

(defne reduceo [rel acc x y] 
     ([_ _() _] (== acc y)) 
     ([_ _ [fx . rx] _] 
     (fresh [nacc] 
       (rel acc fx nacc) 
       (reduceo rel nacc rx y)))) 

(defne everyo [g list] 
     ([_()]) 
     ([_ [fl . rl]] 
     (g fl) 
     (everyo g rl))) 

分関係：(mino* [1 2 3 0] 0) -> #s

(defne mino* [xs y] 
     ([[fxs . rxs] _] 
     (reduceo mino fxs rxs y))) 

メイン関係：(sorto [2 3 1 4] [1 2 3 4]) -> #s

(defne sorto [x y] 
     ([()()]) 
     ([[fx . rx] [fy . ry]] 
     (fresh [x* c] 
       (counto rx c) 
       (counto ry c) 
       (mino* x fy) 
       (rembero fy x x*) 
       (sorto x* ry)))) 

リストとその最小要素間 (mino 1 2 1) -> #s

(defn mino [x y z] 
    (conde 
    [(fd/<= x y) (== x z)] 
    [(fd/> x y) (== y z)])) 

関係

以下の実行は終了しません。理由を理解したいと思います。

(run* [q] 
     (sorto q [1 2])) 
; does not terminate 

(run* [q] 
     (sorto [2 1] q)) 
; does not terminate 

(run* [a b] 
     (everyo #(fd/in % (fd/interval 10)) a) 
     (everyo #(fd/in % (fd/interval 10)) b) 
     (sorto a b)) 
;neither 

Answer 1

高いレベルの答えは、順番に組み合わせて試してみることです。それらを並べ替えるとプログラムを終了させることがありますが、一般的な場合は「良い」順序が存在しないかもしれません。

が正直なところhttps://scholarworks.iu.edu/dspace/bitstream/handle/2022/8777/Byrd_indiana_0093A_10344.pdf