왜 이런 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