Пролог условия завершения

Мой учитель предоставил нам несколько слайдов о Прологе, и я обнаружил кое-что немного странное.

reverse([],[]).
reverse([X|Xs],Zs) :- reverse(Xs,Ys), append(Ys, [X], Zs).

По его словам, программа завершается, когда 1-й аргумент reverse([],..) представляет собой полный список. Кроме того, если вы переключите цели в предикате на reverse([X|Xs],Zs) :- append(Ys, [X], Zs), reverse(Xs,Ys)., программа должна завершиться, когда 2-й аргумент будет полным списком reverse(..,[]).

Это немного противоречит тому, что я узнал до сих пор. Я думал, что оба аргумента повлияли на условие завершения программы, и, судя по примеру моего учителя, это не так. Может ли кто-нибудь дать мне некоторую информацию об этом?


prolog termination failure-slice
person GRoutar    schedule 14.01.2015    source источник

Ответы (1)


arrow_upward
4
arrow_downward

Свойство завершения программ Пролога немного сложно понять из-за относительно сложного потока управления Пролога. Есть способы уменьшить сложность. Во-первых, рассмотреть только части вашей программы, добавив в нее дополнительные цели false. Вы можете разместить их в любом месте. И независимо от того, где вы их поместите, выполняется следующее: если эта новая программа, называемая failure-slice, не завершается , то и ваша исходная программа не завершится. Обратите внимание на «если». Вот ваша программа:

reverse([],[]) :- false.
reverse([X|Xs],Zs) :-
   reverse(Xs,Ys), false,
   append(Ys, [X], Zs).

Этот фрагмент отказа совершенно бесполезен для понимания того, что описывает ваше отношение. Это никогда не удастся. Тем не менее, это помогает нам лучше понять, как завершать работу.

Обратите внимание, что этот факт полностью исключается. На самом деле, независимо от того, как выглядит факт, он не может улучшить прекращение этого фрагмента отказа reverse/2. (Однако это может ухудшить прекращение).

Также обратите внимание на второй аргумент, Zs: больше нет упоминания об этом Zs. Таким образом: второй аргумент reverse/2 может быть каким угодно. Это опять же не улучшит прекращение.

Чтобы заставить reverse/2 завершиться, первый аргумент должен быть создан так, чтобы этот фрагмент завершился. Таким образом, [], [X|[]] прекратятся, даже [X|nonlist] прекратятся. Но частичные списки, такие как Xs, [a|Xs] и т. д., не завершатся.

Если вы хотите улучшить завершение, скажем, для reverse(Xs,[]), вам нужно что-то изменить в видимой, оставшейся части. Один из способов — обмен голами. Теперь Zs может способствовать расторжению. Но, увы, первый аргумент уже не имеет прежнего влияния. Рассмотрим reverse([a], Zs) и:

reverse([],[]) :- false.
reverse([X|Xs],Zs) :-
   append(Ys, [X], Zs), false,
   reverse(Xs,Ys).

append([], Zs, Zs) :- false.
append([X|Xs], Ys, [X|Zs]) :-
   append(Xs, Ys, Zs), false.

Таким образом, хотя этот фрагмент по-прежнему настаивает на том, что первый аргумент равен [_|_], он не принимает во внимание оставшийся член. Таким образом, цель не исчезнет.

Если вы хотите узнать больше, посмотрите failure- срез. В равной степени рассмотрим используя cTI. Чтобы развить хорошую интуицию, вам нужно будет попробовать это самостоятельно.

person false    schedule 14.01.2015