이해 core.logic! =

Question

다음 결과는 두 개의 단점 셀이 서로 다른 두 개의 단점 셀로 구성된 여러 결과를 반환 할 것으로 기대합니다. 그러나 0 개의 결과를 반환합니다. 왜 결과가 나오지 않습니까?

(run* [c1 c2] 
    (fresh [lx ly x1 y1 x2 y2] 
    (== lx [1 2]) 
    (== ly [4 5]) 
    (membero x1 lx) 
    (membero x2 lx) 
    (membero y1 ly) 
    (membero y2 ly) 
    (conso x1 y1 c1) 
    (conso x2 y2 c2) 
    (!= c1 c2))) 

예상 결과의

예 :

• [(1 . 4) (2 . 5)]
• [(1 . 4) (1 . 5)]
• [(2 . 4) (2 . 5)]

나는 각각의 단점의 경우 두 지점 [(1 . 4) (1 . 4)] 같은 결과를 반환하기를 기대하지 않을 것이다

같다.

(!= c1 c2) 부분을 제거하면 두 단점이 같은 부분을 포함하여 16 개의 결과가 나타납니다.

는 내가 함께 (!= c1 c2)를 교체하면 내가 기대하는 결과를 얻을 : 같은 일을해야

(conde 
    ((!= x1 x2)) 
    ((!= y1 y2))) 

하지만, 명시 적으로 두 개의 셀을 확인합니다.

Answer 1

유효한 core.logic 프로그램이 아닙니다. 꼬리가 적절하지 않은 곳에서는 conso을 사용할 수 없습니다. Scheme의 miniKanren을 사용하면이 작업을 수행 할 수 있지만 core.logic의 동작은 정의되지 않습니다. 이를 반영하기 위해 conso의 docstring을 수정했습니다. 실무 프로그램 :

(run* [c1 c2] 
    (fresh [lx ly x1 y1 x2 y2] 
    (== lx [1 2]) 
    (== ly [4 5]) 
    (membero x1 lx) 
    (membero x2 lx) 
    (membero y1 ly) 
    (membero y2 ly) 
    (== [x1 y1] c1) 
    (== [x2 y2] c2) 
    (!= c1 c2))) 

Answer 2

이렇게 conso를 사용할 수 없다는 포스터는 정확합니다. 여기에 참조 문이다 :

리터는이 L
및 D의 제되도록 컬렉션이다 릴레이션 (L)의 나머지 부분이다. 접지면이 적절한 꼬리에 묶여 있어야합니다.

당신은 (== [x1 y1] c1) 및 (== [x2 y2] c2) 또는 (conso x1 [y1] c1) 및 (conso x2 [y2] c2)를 사용하여 적절한 목록을 확인해야합니다.