Лучшее завершение для 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): - неверно.
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 наградой)

Источник

4 ответа

Решение
nat_nat_sum(0, B, B).
nat_nat_sum(s(A), B, s(C)) :-
        nat_nat_sum(B, A, C).

?

Источник

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

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'es.

Это действительно лучше 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)

Источник

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

sum(0,N,N).
sum(N,0,N).
sum(s(A),B,s(C)):- sum(B,A,C) ; sum(A,B,C).
Источник

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

Определение 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 заканчивается для шаблона add(-,-,+), тогда как определение 2 не заканчивается для шаблона add(-,-,+). Смотреть видеть:

Определение 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.

до свидания

Источник
Другие вопросы по тегам