Лучшее завершение для s(X)-суммы

(Позвольте мне добавить это в волну промежуточных вопросов.)

Обычное определение суммы двух натуральных чисел — nat_nat_sum/3:

nat_nat_sum(0, N, N).
nat_nat_sum(s(M), N, s(O)) :-
   nat_nat_sum(M, N, O).

Строго говоря, это определение слишком общее, так как мы имеем теперь успех и для

?- nat_nat_sum(A, B, unnatural_number).

Аналогично получаем следующую подстановку ответов:

?- nat_nat_sum(0, A, B).
   A = B.

Мы интерпретируем эту подстановку ответов как включающую все натуральные числа и не заботимся о других терминах.

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

nat_nat_sum(0, N, N) :- false.
nat_nat_sum(s(M), N, s(O)) :-
   nat_nat_sum(M, N, O), false.

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

Чтобы быть уверенным, срез сбоя не только идентичен своему общему условию завершения (используйте cTI), который читается

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

Он также заканчивается точно так же для тех случаев, которые не подпадают под это условие, например

?- nat_nat_sum(f(X),Y,Z).

Теперь мой вопрос:

Есть ли альтернативное определение nat_nat_sum/3, которое имеет условие завершения:

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

(Если да, покажите это. Если нет, объясните, почему)

Другими словами, новое определение nat_nat_sum2/3 должно заканчиваться, если уже один из его аргументов является конечным и обоснованным.

Мелкий шрифт. Рассматривайте только чистые, монотонные программы на Прологе. То есть никаких встроенных модулей, кроме (=)/2 и dif/2

(Я назначу награду в размере 200 за это)


prolog termination successor-arithmetics failure-slice
person false    schedule 29.11.2014    source источник

Ответы (4)


arrow_upward
2
arrow_downward

Ладно, кажется, все кончено. Решение, о котором я думал, было:

nat_nat_sum2(0, N,N).
nat_nat_sum2(s(N), 0, s(N)).
nat_nat_sum2(s(N), s(M), s(s(O))) :-
   nat_nat_sum2(N, M, O).

Но насколько я понимаю, это то же самое, что и у @mat, которое почти такое же, как у @WillNess.

Это действительно лучше nat_nat_sum/3? Время выполнения оригинала не зависит от B (если мы проигнорируем один (1), произойдет проверка на данный момент).

Есть еще один недостаток моего решения по сравнению с решением @mat, которое, естественно, распространяется на nat_nat_nat_sum/3.

nat_nat_nat_sum(0, B, C, D) :-
   nat_nat_sum(B, C, D).
nat_nat_nat_sum(s(A), B, C, s(D)) :-
   nat_nat_nat_sum2(B, C, A, D).

Который дает

nat_nat_nat_sum(A,B,C,D)terminates_if b(A),b(B);b(A),b(C);b(B),b(C);b(D).

(доказуемо в развернутой версии с cTI)

person false    schedule 29.11.2014
comment
Я бы сказал, что мой вариант ближе к вашему минимальному переписыванию, чем вариант Мэта. Его я рассматривал в первую очередь, но затем попытался настроить его дальше. Ваша настройка перемещает мой 2-й пункт, так сказать, на один уровень вниз. Но мы оба не решили ее. Вы действительно должны принять свой собственный (этот) ответ. - person Will Ness; 30.11.2014
comment
теперь, когда я вижу этот вариант, он имеет гораздо больше смысла, чем что-либо еще. :) - person Will Ness; 30.11.2014
comment
@WillNess: Это, безусловно, легче понять, поскольку каждый аргумент независимо уменьшается в рекурсивном правиле, что также является причиной проблем с cTI. А теперь представьте nat_nat_nat_sum/4! Версия @mat работает здесь так же гладко, гарантируя завершение для: nat_nat_nat_sum(A,B,C,D)terminates_if b(A),b(B);b(A),b(C);b(B),b(C);b(D). - person false; 30.11.2014
comment
(увидеть какой-то код поможет...), но это другой вопрос, о сумме/4. вот твой ответ. - person Will Ness; 30.11.2014

arrow_upward
1
arrow_downward

Очевидный трюк состоит в том, чтобы перевернуть аргументы:

sum(0,N,N).
sum(N,0,N).
sum(s(A),B,s(C)):- sum(B,A,C) ; sum(A,B,C).
person Will Ness    schedule 29.11.2014
comment
Но sum(s(0),B,C), false не прекращается, верно? - person false; 29.11.2014
comment
Хм да. Должен ли? Я не понял условий прекращения: что означает b(A)? - person Will Ness; 29.11.2014
comment
b(A): конечное и основное. вульго: ограниченный или ограниченный - я никогда не знаю, какой именно :-) - person false; 29.11.2014
comment
Спасибо. Это тяжело. :) - person Will Ness; 29.11.2014
comment
Доказательства. Просто используйте другой ответ для другой попытки! - person false; 29.11.2014
comment
Это означает, что nTI cTI (вывод без завершения) не смог вывести/найти/доказать пример с этим режимом. См. complang.tuwien.ac.at/cti/help#NTI. - person false; 29.11.2014
comment
а что значит ф? - person Will Ness; 29.11.2014
comment
@false вау, спасибо! Я признателен за это. Спасибо за интересную задачу, хотелось бы решить ее полностью. :) Реальное решение, как показывает ваш ответ, состоит в том, чтобы не вводить дублирование ни в один из пунктов, при этом охватывая, так сказать, все углы. Хороший. - person Will Ness; 02.12.2014

arrow_upward
1
arrow_downward

Возьмем следующие два определения:

Определение 1:

add(n,X,X).
add(s(X),Y,s(Z)) :- add(X,Y,Z).

Определение 2:

add(n,X,X).
add(s(X),Y,Z) :- add(X,s(Y),Z).

Определение 1 завершается для добавления шаблона (-,-,+), тогда как определение 2 не завершается для добавления шаблона (-,-,+). Смотреть видеть:

Определение 1:

?- add(X,Y,s(s(s(n)))).
X = n,
Y = s(s(s(n))) ;
X = s(n),
Y = s(s(n)) ;
X = s(s(n)),
Y = s(n) ;
X = s(s(s(n))),
Y = n
?-

Определение 2:

?- add(X,Y,s(s(s(n)))).
X = n,
Y = s(s(s(n))) ;
X = s(n),
Y = s(s(n)) ;
X = s(s(n)),
Y = s(n) ;
X = s(s(s(n))),
Y = n ;
Error: Execution aborted since memory threshold exceeded.
    add/3
    add/3
?-

Так что я думаю, что определение 1 лучше, чем определение 2.

до свидания

person Mostowski Collapse    schedule 05.12.2014
comment
Определение 2 нейтрально по завершению для Arg2 и Arg3. - person false; 06.12.2014
comment
Понятие завершения хорошо известно в контексте логического программирования и Пролога. Если быть точным, речь идет об универсальном прекращении. Если у вас есть контрпример двух запросов с некоторыми терминами A, B, C1, C2 такими, что add(A,B,C1), false и add(A,B,C2), false (с определением 2) заканчиваются по-разному, сообщите мне их. Я утверждаю: такого контрпримера не существует. - person false; 07.12.2014

arrow_upward

arrow_downward

person    schedule
comment
Можем ли мы увидеть контрпример из этого вывода? - person mat; 30.11.2014
comment
Минимальное изменение дает nat_nat_sum(A,B,C)terminates_if b(A);b(B);b(C). - person false; 30.11.2014
comment
Ключевая идея моего решения заключается в циклическом повороте слагаемых, чтобы периодически каждое из них оказывалось в позиции первого аргумента, что может повлиять на завершение. Эта стратегия допустима в данном случае, поскольку сложение коммутативно. Это работает для любого количества слагаемых. Я начал с минимальной перезаписи. Затем я сократил его до версии выше. - person mat; 03.12.2014
comment
Не могли бы вы включить это в свой ответ? - person false; 07.04.2016