Запись преемника Пролог дает неполный результат и бесконечный цикл

Я начал изучать Пролог и впервые узнал о записи преемника.

И здесь я узнаю о написании аксиом Пеано в Прологе.

Смотрите страницу 12PDF:

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

prod(0,M,0).
prod(s(N), M, P) :-
    prod(N,M,K),
    sum(K,M,P).
</code>

Я положил правила умножения в Пролог. Затем я делаю запрос:

<code>?- prod(X,Y,s(s(s(s(s(s(0))))))).
</code>

Что означает найти фактор 6 в принципе.

Вот результаты.

<code>X = s(0),
Y = s(s(s(s(s(s(0)))))) ? ;
X = s(s(0)),
Y = s(s(s(0))) ? ;
X = s(s(s(0))),
Y = s(s(0)) ? ;
infinite loop
</code>

Этот результат имеет две проблемы:

Not all results are shown, note that the result X=6,Y=1 is missing. It does not stop unless I Ctrl+C then choose abort.

Итак ... мои вопросы:

WHY is that? I tried switching "prod" and "sum" around. The resulting code gives me all results. And again, WHY is that? It still dead-loops though. HOW to resolve that?

Я прочитал другой ответ на бесконечный цикл. Но я бы хотел, чтобы кто-то ответил на основании этого сценария. Это очень помогает мне.

 mat21 мар. 2016 г., 21:39
После сравнения тега вики,non-termination кажется гораздо лучше подходит. На самом деле, судя по тегу вики, практически во всех случаях, когда мы сейчас используемinfinite-loop вместе сprolog должен быть помечен вместо или в дополнение сnon-termination, Как лучше всего обсуждать такие лучшие методы маркировки? Лично я предпочитаюnon-termination, по крайней мереin addition вinfinite-loop.

Ответы на вопрос(2)

Решение Вопроса

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

Universal termination

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

Failure slice

Следующее, что вам нужно, это понятиесрез неудачи, Возьмите программу с чисто монотонной логикой и добавьте несколько целей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 не встречается ни в одной цели. Нет необходимости в болтливых трассировщиках.

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

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

Termination inference

Это последнее, что вам нужно: вывод (или анализатор) завершения типа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) элегантно заканчивается ...

 14 апр. 2012 г., 14:18
@ Чак: Да. Пожалуйста, ознакомьтесь с условиями расторжения, установленными cTI - см. Последнюю ссылку.
 13 апр. 2012 г., 17:55
но prod2 (X, Y, s (0)) (или любое другое значение) также не завершается. Это улучшение?
 14 апр. 2012 г., 14:15
@Felastine: Вы добавляете дополнительные целиfalse/0 где-то. Таким образом, вы не отрицаете условие. Отрицание, это было бы, например,dif(X,a) на местеX = a.
 Felastine13 апр. 2012 г., 16:05
По сбою ломтик, это все равно что отрицать все условия в правилах? И тогда мы делаем запрос, как обычно? то есть prod (X, Y, s (s (s (s (s (s (s))))))))?
 15 апр. 2012 г., 18:18
Действительно отличный ответ. А такжеLocalizing and explaining reasons for non-terminating logic programs with failure-slices это то, что я абсолютноneed понять.

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

Если мы поменяем сумму на сумму, то получим 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) завершается, если b (A), b (B); b (A), b (C).

 18 апр. 2012 г., 20:26
+1: я впечатлен - этоnot решение, которое я ожидал!
 18 апр. 2012 г., 20:30
относительно cTI: система говорит вам, что есть2 unresolved: [prod3(f,b,b),prod3(f,f,b)], Это означает, что cTI не смог вывести эти случаи, а NTI не смог доказать факт невыполнения. Так что это неизвестно cTI. Увидетьthe manual

Ваш ответ на вопрос