Ответ 1

Если вы хотите подробно изучить свойства завершения, программы, использующие successor-arithmetics - идеальный объект исследования: вы знаете априори, что они должны описывать, поэтому вы можете сосредоточиться на более технических деталях. Вам нужно будет понять несколько понятий.

Универсальное завершение

Самый простой способ объяснить это - рассмотреть Goal, false. Это завершает iff Goal завершается универсально. То есть: смотреть на трассировщики является самым неэффективным способом - они покажут вам только один путь выполнения. Но вам нужно понять их всех сразу! Также никогда не смотрите на ответы, когда вы хотите универсального завершения, они будут только отвлекать вас. Вы видели это выше: у вас есть три аккуратных и правильных ответа, только тогда ваша программа будет проходить. Поэтому лучше "выключить" ответы с помощью false. Это удаляет все отвлечение.

Отказоустойчивость

Следующее понятие, которое вам нужно, это фрагмент отказа. Возьмите чистую монотонную логическую программу и запустите несколько целей false. Если результирующий фрагмент отказа не заканчивается (универсально), то и исходная программа не будет. В вашем примере рассмотрим:

prod(0,M,0) :- false.
prod(s(N), M, P) :-
    prod(N,M,K), false,
    sum(K,M,P).

Эти цели false помогают удалить ненужные украшения в вашей программе: оставшаяся часть ясно показывает, почему prod(X,Y,s(s(s(s(s(s(0))))))). не заканчивается. Он не заканчивается, потому что этот фрагмент вообще не заботится о P! Вы надеетесь, что третий аргумент поможет сделать prod/3 завершенным, но фрагмент показывает вам, что все это напрасно, так как P не встречается ни в одной цели. Нет необходимости в чатах.

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

Что примечательно в отношении фрагмента отказа: если вы хотите улучшить программу, вы должны изменить свою программу в части, видимой в этом фрагменте! Пока вы его не измените, проблема будет сохраняться. Таким образом, срез сбоя является очень важной частью вашей программы.

Завершение вывода

Это последняя вещь, в которой вы нуждаетесь: терминатор (или анализатор терминации), такой как cTI, поможет вам быстро определить условие завершения, Посмотрите на предполагаемые условия завершения prod/3 и улучшенный prod2/3 здесь!

Изменить: И поскольку это был вопрос домашней работы, я не опубликовал окончательное решение. Но для того, чтобы было ясно, вот условия завершения, полученные до сих пор:

    prod(A,B,C)terminates_if b(A),b(B).
    prod2(A,B,C)terminates_if b(A),b(B);b(A),b(C).

Итак, новый prod2/3 строго лучше исходной программы!

Теперь вам решать, как найти финальную программу. Его условие завершения:

   prod3(A,B,C)terminates_if b(A),b(B);b(C).

Для начала попробуйте найти фрагмент отказа для prod2(A,B,s(s(s(s(s(s(0)))))))! Мы ожидаем, что он закончится, но он все еще не работает. Поэтому возьмите программу и добавьте вручную false целей! Оставшаяся часть покажет вам ключ!

В качестве окончательного намека: вам нужно добавить еще одну цель и один факт.

Изменить: по запросу здесь находится срез отказа для prod2(A,B,s(s(s(s(s(s(0))))))):

prod2(0,_,0) :- false.
prod2(s(N), M, P) :-
   sum(M, K, P),
   prod2(N,M,K), false.

sum(0, M, M).
sum(s(N), M, s(K)) :- false,
    sum(N,M,K).

Обратите внимание на значительно упрощенное определение sum/3. Он говорит только: 0 плюс что-нибудь есть. Больше не надо. В результате даже более специализированный prod2(A,0,s(s(s(s(s(s(0))))))) будет зацикливаться, а prod2(0,X,Y) изящно завершает...

Ответ 2

Первый вопрос (ПОЧЕМУ) довольно легко заметить, особенно если вы знаете о левой рекурсии. sum(A,B,C) связывает A и B, когда C , но исходная программа prod (A, B, C) не использует эти привязки и вместо этого перезаписывает A, B unbound.

Если мы поменяем сумму, то мы получим 2 полезных привязки из суммы для рекурсивного вызова:

sum(M, K, P)

Теперь M привязан и будет использоваться для завершения лево-рекурсии. Мы можем заменить N и M, поскольку мы знаем, что произведение является коммутативным.

sum(0, M, M).
sum(s(N), M, s(K)) :-
    sum(N, M, K).

prod3(0, _, 0).
prod3(s(N), M, P) :-
    sum(M, K, P),
    prod3(M, N, K).

Заметим, что если мы поменяем M, K (т.е. sum (K, M, P)), когда prod3 вызывается с P unknown, мы снова имеем неконцевую петлю, но в сумме.

?- prod3(X,Y,s(s(s(s(s(s(0))))))).
X = s(s(s(s(s(s(0)))))),
Y = s(0) ;
X = s(s(s(0))),
Y = s(s(0)) ;
X = s(s(0)),
Y = s(s(s(0))) ;
X = s(0),
Y = s(s(s(s(s(s(0)))))) ;
false.

OT Я озадачен сообщением cTI: prod3 (A, B, C) terminates_if b (A), b (B); b (A), b (C).