이 Prolog Predicate가 효과가있는 이유는 무엇입니까?

Question

다음 코드가 있습니다.이 코드는 목록에서 작동하지만이 목록은 세트를 나타내므로 [1,1,2,2,3,3] 및 [1,2,3]은 동등해야합니다.

%contains(L1, L2), returns true if L1 contains L2
contains(_, []).
contains(L1, [Head|Tail]) :- member(Head, L1), contains(L1, Tail).
%equals(L1, L2), returns true if L1 is equal to L2
equals([X|L1],[X|L2]) :- equals(L1, L2).
equals(L1, L2) :- contains(L1, L2), contains(L2, L1).

아이디어는 평등 ([1,2,3], [1,2,1,3])가 True를 반환해야한다는 것입니다. 그러나 위의 정의를 바탕으로 내가 기대할 것으로 예상되는 일은 다음과 같습니다.

1. 동등한 ([1,2,3], [1,2,1,3])는 첫 번째 규칙과 일치하고 동등한 ([2,3], [2,1,3]])를 호출합니다.
2. Equals ([2,3], [2,1,3]])는 두 번째 규칙과 일치하고 ([2,3], [2,1,3])를 포함하고 ([2,1,3], [2,3]).
3. ([2,3], [2,1,3])가 실패하고 반환 번호와 동일합니다.

그러나 여전히 작동합니다. 그리고 다른 시도도 혼동하려고합니다. 누군가 나에게 설명해 주시겠습니까?

(프롤로그 구현 : SWI-PROLOG 버전 2.7.12)

Answer 1

Prolog는 "Backtracking"이라는 기술을 사용합니다.

첫 번째 단계 인 1 단계를 살펴보십시오.

Prolog에는 여기서 사용할 수있는 두 가지 규칙이 있습니다. 설명에서 선택한 규칙을 사용하면 항상 실패합니다. 그러나 일단 실패하면 Prolog는 역 추적하고 대안 규칙을 시도합니다.

Equals ([1,2,3], [1,2,1,3]) :- ([1,2,3], [1,2,1,3]), 포함 ([1,2, 1,3], [1,2,3])

잘못된 답변을 찾은 후 반복적으로 역 추적함으로써, Prolog는 사실 인 해결책을 찾아서 그 대답이 사실이라는 것을 알고 있습니다.

규칙을 적용 할 수있는 모든 방법을 시도한 경우, 진정한 답변을 찾지 않고 대답은 거짓이어야합니다.

이것은 Prolog의 매우 근본적인 부분입니다. 나는 당신이 그것을 이해하지 않고 이것을 멀리 있다는 것에 놀랐습니다.

Answer 2

귀하의 코드는 매우 이상하지만 테스트 목적으로 Trace 술어를 사용하는 것이 좋습니다. 예는 다음과 같습니다.

4 ?- trace([equals,contains]).
%         equals/2: [call, redo, exit, fail]
%         contains/2: [call, redo, exit, fail]
true.

[debug] 5 ?- equals([1,2,3],[1,2,1,3]).
 T Call: (7) equals([1, 2, 3], [1, 2, 1, 3])
 T Call: (8) equals([2, 3], [2, 1, 3])
 T Call: (9) equals([3], [1, 3])
 T Call: (10) contains([3], [1, 3])
 T Fail: (10) contains([3], [1, 3])
 T Fail: (9) equals([3], [1, 3])
 T Redo: (8) equals([2, 3], [2, 1, 3])
 T Call: (9) contains([2, 3], [2, 1, 3])
 T Call: (10) contains([2, 3], [1, 3])
 T Fail: (10) contains([2, 3], [1, 3])
 T Fail: (9) contains([2, 3], [2, 1, 3])
 T Fail: (8) equals([2, 3], [2, 1, 3])
 T Redo: (7) equals([1, 2, 3], [1, 2, 1, 3])
 T Call: (8) contains([1, 2, 3], [1, 2, 1, 3])
 T Call: (9) contains([1, 2, 3], [2, 1, 3])
 T Call: (10) contains([1, 2, 3], [1, 3])
 T Call: (11) contains([1, 2, 3], [3])
 T Call: (12) contains([1, 2, 3], [])
 T Exit: (12) contains([1, 2, 3], [])
 T Exit: (11) contains([1, 2, 3], [3])
 T Exit: (10) contains([1, 2, 3], [1, 3])
 T Exit: (9) contains([1, 2, 3], [2, 1, 3])
 T Exit: (8) contains([1, 2, 3], [1, 2, 1, 3])
 T Call: (8) contains([1, 2, 1, 3], [1, 2, 3])
 T Call: (9) contains([1, 2, 1, 3], [2, 3])
 T Call: (10) contains([1, 2, 1, 3], [3])
 T Call: (11) contains([1, 2, 1, 3], [])
 T Exit: (11) contains([1, 2, 1, 3], [])
 T Exit: (10) contains([1, 2, 1, 3], [3])
 T Exit: (9) contains([1, 2, 1, 3], [2, 3])
 T Exit: (8) contains([1, 2, 1, 3], [1, 2, 3])
 T Exit: (7) equals([1, 2, 3], [1, 2, 1, 3])
true