|
НАЗАД
Рассмотрим пример запроса к процедуре 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). % Пр1
rev([],Y,Y). % Пр2
rev([H|Xs],L,Y):¾rev(Xs,[H|L],Y). % Пр3
В процедуре revers2 введен дополнительный предикат rev с тремя аргументами¾списками, где первый аргумент ¾ исходный список, второй аргумент ¾ накапливающийся список, а третий аргумент ¾ результирующий, обращенный список.
Декларативное определение предиката rev формулируется следующим образом:
v если первый аргумент есть пустой список, то второй и третий аргументы представляют собой один и тот же список;
v первый аргумент¾ непустой список [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]}.
НАЗАД
|
