Clojure의 core.logic에서 목표를 주문하는 경우

Question

The following Clojure code은 core.logic을 사용하여 두 가지 주문에서 동일한 목표를 가진 동일한 로직 문제를 해결합니다. 이 정렬 순서로 인해 하나는 빨리 끝내고 다른 하나는 걸리게됩니다.

(use `clojure.core.logic) 

;; Runs quickly. Prints (1 2 3). 
(clojure.pprint/pprint (run* [q] (fresh [x] (== x [1,2,3]) 
              (membero q x)))) 

;; Hangs 
(clojure.pprint/pprint (run* [q] (fresh [x] (membero q x) 
              (== x [1,2,3])))) 

이 문제를 방지하려면 일반적인 해결책이나 일반적인 방법이 있습니까? core.logic와

, 당신은 가능한 한 빨리 검색 공간을 줄이고 자 :

Answer 1

membero을 사용하려는 경우이 문제에 대한 일반적인 해결책은 없습니다. 신선한 vars로 membero을 호출하면 q이 구성원 인 모든 (읽기, 무제한) 가능한 목록이 생성됩니다. 물론 3보다 큰 목록은 적용되지 않습니다. 그러나 run*을 사용했기 때문에 각 목록이 실패하더라도 맹목적으로 3 번보다 큰 목록을 계속 시도합니다.

제약 인프라를 사용하여 새로운 버전의 core.logic에 membero의 더 나은 버전을 작성할 수는 있지만,이를 수행하는 방법에 대한 자세한 내용은 향후 몇 개월 동안 변경 될 수 있습니다. 제약 조건을 정의 할 수있는 견고한 공개 API가있을 때까지 Prolog에 문제가되는 미묘한 주문 및 비 종료 문제와 관련이 있습니다.

Answer 2

여기 나의 이해이다. 처음에 membero 제약 조건을 입력하면 membero 공간을 검색하고 == 제약 조건에 의해 생성 된 오류를 추적하여 실행이 시작됩니다. 그러나 membero 공간은 매우 크다. 왜냐하면 q도 아니고 x도 통일되어 있지 않기 때문이다.

그러나 먼저 == 제약 조건을 넣을 경우, 직접 [1 2 3]와 x를 통합하고, membero에 대한 검색 공간은 이제 명확 x의 요소에 묶여있다.