3. Предикаты revers1 и revers2.

Предикаты revers1 и revers2 являются предикатами обращения списков и определяют одно и то же отношение различными способами. Схема отношения этого предиката имеет вид:

revers(<список>,<список>).

Предикат revers(X,Y) истинен, если список Y содержит все элементы списка Х, которые записаны в списке Y в обратном порядке. Перестановку элементов списка в обратном порядке можно произвести путем многократного выполнения процедуры append.

Процедура revers определяется двумя способами:

• простым обращением;

• обращением с накоплением.

Простое обращение выполняется процедурой revers1, которая использует процедуру append (см. 5.4.5) и состоит из двух предложений:

revers1([],[]).

revers1([H|Xs],Zs):revers1(Xs,Ys), append(Ys,[H],Zs).

Декларативное определение предиката revers1 формулируется следующим образом:

• обращенный пустой список есть пустой список;

• если список Х можно разделить на голову Н и хвост Xs, то Zs есть обращенный список, если Ys обращенный хвост списка X, Zs получен путем присоединения к Ys головы Н списка X.

Рассмотрим пример запроса к процедуре revers1(X,Y).

?  revers1([1,2,3],Zs).

ТР: revers1([1,2,3],Zs).

Шаг 1: ТЦ: revers1([1,2,3],Y).

Пр1: [1,2,3] не сопоставим []  неуспех

Пр2: revers1([1|[2,3]],Zs): revers1(Xs1,Ys1),append(Ys1,[1],Zs).

Xs1=[2,3]

ТР: revers1([2,3],Ys1),append(Ys1,[1],Zs).

Шаг 2: ТЦ: revers1([2,3],Ys1).

Пр1: [2,3] не сопоставим [] неуспех

Пр2: revers1([2|[3]],Ys1): revers1(Xs2,Ys2),append(Ys2,[2],Ys1).

где Xs2=[3].

ТР: revers1([3],Ys2),append(Ys2,[2],Zs).

Шаг 3: ТЦ: revers1([3],Ys2).

Пр1: [3] не сопоставим [] неуспех

Пр2: revers1([3|[]],Ys2):revers1(Xs3,Ys3),append(Ys3,[3],Ys2).

где Xs3=[].

ТР: revers1([],Ys3),append(Ys3,[3],Ys2).

Шаг 4: ТЦ: revers1([],Ys3).

Пр1: [] сопоставим [] успех

Получается подстановка {Ys3=[]}.

ТР: append(Ys3,[3],Ys2).

Шаг 5: ТЦ: append(Ys3,[3],Ys2).

Получается подстановка {Ys2=[3]}.

ТР: append(Ys2,[2],Ys1).

Шаг 6: ТЦ: append(Ys2,[2],Ys1).

Получается подстановка {Ys1=[3,2]}.

ТР: append(Ys1,[1],Zs).

Шаг 6: ТЦ: append(Ys1,[1],Zs).

Получается подстановка {Zs=[3,2,1]}.

ТР: .

Результат вычисления запроса: revers1([1,2,3],Zs).  успех

при подстановке {Zs=[3,2,1]}.

Обращение списка с накоплением выполняется процедурой revers2, состоящей из трех предложений и содержит дополнительный предикат rev:

revers2(X,Y):rev(X,[],Y).

rev([],Y,Y).

rev([H|Xs],L,Y):rev(Xs,[H|L],Y).

В процедуре revers2 введен дополнительный предикат rev с тремя аргументамисписками, где первый аргумент  исходный список, второй аргумент  накапливающийся список, а третий аргумент  результирующий, обращенный список.

Декларативное определение предиката rev формулируется следующим образом:

• если первый аргумент есть пустой список, то второй и третий аргументы представляют собой один и тот же список;

• первый аргумент непустой список [H|Хs], и его можно разделить на голову Н и хвост Xs; в этом случае применение предиката rev к списку [H|Хs] и накапливающемуся списку L равносильно применению предиката rev к хвосту списка Xs и списку [H|L]; при этом получается обращенный список Y.

Рассмотрим пример запроса к процедуре revers2(X,Y).

?  revers2([1,2,3],Y).

ТР: revers2([1,2,3],Zs).

Шаг 1: ТЦ: revers2([1,2,3],Y).

Пр1: revers2([1,2,3],Y):rev([1,2,3],[],Y)  успех

ТР: rev([1,2,3],[],Y).

Шаг 2: ТЦ: rev([1,2,3],[],Y).

Пр2: [1,2,3] не сопоставим [] неуспех

Пр3: rev([1|[2,3]],[],Y): rev(Xs2,[1|[]],Y).

где Xs2=[2,3].

ТР: rev([2,3],[1]],Y).

Шаг 3: ТЦ: rev([2,3],[1]],Y).

Пр2: [2,3] не сопоставим [] неуспех

Пр3: rev([2|[3]],[],Y): rev(Xs3,[2|[1]],Y).

где Xs3=[3].

ТР: rev([3],[2,1],Y).

Шаг 4: ТЦ: rev([3],[2,1],Y).

Пр2: [3] не сопоставим [] неуспех

Пр3: rev([3|[]],[2,1],Y): rev(Xs4,[3|[2,1]],Y).

где Xs4=[].

ТР: rev([],[3,2,1] ,Y).

Пр2: [] сопоставим [] успех

Получается подстановка {Y=[3,2,1]}

ТР: .

Истинность ТЦ на шаге 4 влечет истинность цели на шаге 3.

Истинность ТЦ на шаге 3 влечет истинность цели на шаге 2.

Истинность ТЦ на шаге 2 влечет истинность цели на шаге 1.

Результат вычисления запроса: revers2([1,2,3],Zs)  успех при подстановке {Zs=[3,2,1]}.