왜 core.logic의 출력이 같은 값을 반복합니까?

Question

나는 [1 4] [1 5]

로 결과를 기대 core.logic

 
(require [clojure.core.logic :as l]) 

(l/run* [q] 
    (l/fresh [a b c] 
    (l/membero a [1]) 
    (l/membero b [4 5]) 
    (l/membero c [1 2]) 
    (l/== q [a b]))) 

이 시도하지만

[1 4] [1 4] [1 5] [1 5] 다음 나는 그것으로 연주하기 시작했고이 발견

 
(require [clojure.core.logic :as l]) 

(l/run* [q] 
    (l/fresh [a b c] 
    (l/membero a [1]) 
    (l/membero b [4 5]) 
    (l/membero c [1 1 1 1 1 1 1 1]) 
    (l/== q [a b]))) 

을

;; => ([1 4] [1 4] [1 4] [1 5] [1 4] [1 4] [1 5] [1 4] [1 5] [1 4] [1 5] [1 5] [1 5] [1 5]) 

[1 5]이 산재되어 있습니다. [1 4]

무슨 일이 일어나고 있습니까? 이 반복 기능이 기능 또는 버그라고 생각합니까?

Answer 1

이것은 논리 변수 c의 사용이 q으로 통일되지 않으므로 필요하지 않기 때문입니다. c을 제거하면 원하는 결과를 얻을 수 있습니다. 기본적으로 당신은 c 때문에 이러한 중복 결과를 얻는 이유를 이해하기 위해 core.logic에서 대체가 어떻게 작동하는지 이해해야합니다.

상위 수준에서 프로세스는 솔루션을 찾기 위해 트리를 검색하는 것과 같습니다.이 경우 벡터의 각 요소는 membero이고 c 인 노드는 검색 트리의 노드로 연결되며 이로 인해 중복 된 결과가 발생합니다. c 가능성있는 값은 c이 통합에서 사용되지 않기 때문에 올바른 결과로 연결됩니다. (l/== q [a b])