Пролог пытается найти другие решения, но я не знаю почему (есть только одно)

Question

Я читаю веб-сайт Learn Prolog Now и пытаюсь выполнить следующее упражнение:

6.5. Создать предикат swapfl (List1, List2), который проверяет, идентичен ли List1 List2, за исключением того, что первыйи последние элементы обмениваются. Вот где append / 3 может снова пригодиться, но также возможно написать рекурсивное определение без обращения к append / 3 (или любым другим) предикатам.

Я написал это, и оно работает правильно, но пытается найти более одного решения.

swapfl([HL1|TL1],[HL2|TL2]):-
   swpfl(TL1,TL2,HL2,HL1).

swpfl([HL1|TL1],[HL2|TL2],AccEL1,AccEL2):-
   swpfl(TL1,TL2,AccEL1,AccEL2),
   HL1=HL2.
swpfl([H1],[H2],H1,H2).

Я смотрю на код и след

[trace] [5]  ?- swapfl([1,2,3],[3,2,1]).
   Call: (51) swapfl([1, 2, 3], [3, 2, 1]) ? creep
   Call: (52) swpfl([2, 3], [2, 1], 3, 1) ? creep
   Call: (53) swpfl([3], [1], 3, 1) ? creep
   Exit: (53) swpfl([3], [1], 3, 1) ? creep
   Call: (53) 2=2 ? creep
   Exit: (53) 2=2 ? creep
   Exit: (52) swpfl([2, 3], [2, 1], 3, 1) ? creep
   Exit: (51) swapfl([1, 2, 3], [3, 2, 1]) ? creep
true ;
   Redo: (52) swpfl([2, 3], [2, 1], 3, 1) ? creep
   Fail: (52) swpfl([2, 3], [2, 1], 3, 1) ? creep
   Fail: (51) swapfl([1, 2, 3], [3, 2, 1]) ? creep
false.

и я не могу понять, почему пролог считает, что может быть стоит начать повторную часть.

Может кто-нибудь объяснить, почему существует неисследованная ветвь дерева решений?

Answer 1

Пролог всегда изучит все варианты, прежде чем принять окончательное решение.

Попробуйте взглянуть на следующий вопрос о переполнении стека: Пролог: условие остановки?

Ложный ответ может показаться несовместимым с начинающими программистами Prolog и «ощущаться» как ошибка или предупреждение, но на самом деле это совершенно нормальный ответ Prolog. Пролог достаточно последовательн в своем поведении, пытаясь найти решения, и, когда больше нет выбора, он вернет false. Если Prolog исчерпал все остальные варианты, прежде чем нашел окончательное решение, он отображает решение и не возвращает false.