Почему Пролог не может найти сумму, когда я перефразирую ее?

Question

Предположим, я хочу найти сумму списка в SWI-Prolog. Наиболее очевидным решением было бы что-то в форме:

sum([],0).
sum([H|T],S) :- sum(T, SofT), S is SofT + H.

и работает точно так, как ожидалось.

Однако из любопытства я решил перефразировать проблему, сказав, что нам нужно найти сумму, такую, что сумма хвоста равна общей сумме минус голова. Должно быть то же самое математически, хотя, возможно, немного менее естественно. Я написал это как

sum2([],0).
sum2([H|T],S) :- sum2(T, S-H).

Затем я выполняю свои запросы с очень простым тестовым примером и получаю результат:

?- sum([1], S).
S = 1.

?- sum2([1], S).
false.

SWI-Пролог, похоже, не смог найти решение для sum2, и мне интересно, почему это так. У меня действительно было внутреннее чувство, что все может пойти так, но я все еще не уверен, что на самом деле здесь происходит. Я запустил трассировщик, но не нашел вывод ужасно полезным. Я новичок в Прологе, поэтому я подозреваю, что вопрос может быть глупым или намекает на какое-то ужасное заблуждение с моей стороны.

Любые объяснения приветствуются, спасибо!

Answer 1

Согласно этого урока
Даны два условия T1 и T2 и которые должны быть объединены:

• Если T1 и T2 являются константами (то есть атомами или числами), тогда, если они одинаковы, преуспевает. Иначе не получится.
• Если T1 является переменной, то создать экземпляр T1 до T2 .
• В противном случае, если T2 является переменной, создать экземпляр T2 до T1 .
• В противном случае, если T1 и T2 являются сложными терминами с одинаковой арностью (числом аргументов), найдите главный функтор F1 из T1 и главный функтор F2 из T2 . Если они совпадают, то возьмите упорядоченный набор аргументов из T1 и упорядоченный набор аргументов из T2 . Для каждой пары аргументов Am и Bm из одной и той же позиции в термине Am должно объединяться с Bm .
• В противном случае не удастся.

поэтому при запуске

?- sum2([1], S).

он пробежал

sum2([],S-1)

, который объединился с

sum2([],0)

и собирается объединить S-1 в 0, где 0 и 1 являются постоянными, а S является переменной.
но S-1 не является ни постоянным, ни переменным, поэтому он потерпел неудачу.