Я не понимаю имя вашего предиката. В любом случае, это отвлечение. Неравномерное именование переменных также отвлекает. Давайте используем некоторые нейтральные короткие однослоговые имена, чтобы сосредоточиться на самом коде в его самой ясной форме:
foo( H, [H | T], T). % 1st clause
foo( X, [H | T], [H | R]) :- foo( X, T, R). % 2nd clause
Так что это встроенный select/3. Ура! ..
Теперь вы спрашиваете о запросе foo( 2, [1,2,3], R) и как R правильно устанавливает его значение. Главное, чего не хватает в вашем кратком изложении, - это переименование переменных, когда выбрано соответствующее предложение. разрешение запроса выглядит так:
|- foo( 2, [1,2,3], R) ? { }
%% SELECT -- 1st clause, with rename
|- ? { foo( H1, [H1|T1], T1) = foo( 2, [1,2,3], R) }
**FAIL** (2 = 1)
**BACKTRACK to the last SELECT**
%% SELECT -- 2nd clause, with rename
|- foo( X1, T1, R1) ?
{ foo( X1, [H1|T1], [H1|R1]) = foo( 2, [1,2,3], R) }
**OK**
%% REWRITE
|- foo( X1, T1, R1) ?
{ X1=2, [H1|T1]=[1,2,3], [H1|R1]=R }
%% REWRITE
|- foo( 2, [2,3], R1) ? { R=[1|R1] }
%% SELECT -- 1st clause, with rename
|- ? { foo( H2, [H2|T2], T2) = foo( 2, [2,3], R1), R=[1|R1] }
** OK **
%% REWRITE
|- ? { H2=2, T2=[3], T2=R1, R=[1|R1] }
%% REWRITE
|- ? { R=[1,3] }
%% DONE
Цели между |- и ? являются резольвентой , уравнения внутри { } являются заменой . База знаний (КБ) неявно слева от |- в полном объеме.
На каждом шаге выбирается самая левая цель в резольвенте, а пункт с соответствующей головкой выбирается среди тех, что в КБ (в то время как переименовывает все Переменные предложения в согласованном порядке, так что никакая переменная в резольвенте не используется переименованным предложением, поэтому нет случайного захвата переменной) , и выбранная цель заменяется в резольвенте телом этого предложения, в то время как успешное объединение добавляется в замену. Когда резольвента пуста, запрос был проверен, и мы видим успешный и -ответвление в целом и / или дерево .
Вот как машина может это делать. Шаги «переписать» представлены здесь для облегчения понимания человеком.
Итак, мы видим здесь, что первый успешный выбор предложения приводит к уравнению
R = [1 | R1 ]
, а второй, -
R1 = [3]
, что в совокупности влечет за собой
R = [1, 3]
Эта постепенная нисходящая инстанцияция / списывание списков - очень характерный способ Пролога действовать.
В ответ на вызов за вознаграждение, касающийся функциональной зависимости в отношении foo/3 (то есть select/3): в foo(A,B,C) любые два основных значения для B и C однозначно определяют значение A (или его отсутствие):
2 ?- foo( A, [0,1,2,1,3], [0,2,1,3]).
A = 1 ;
false.
3 ?- foo( A, [0,1,2,1,3], [0,1,2,3]).
A = 1 ;
false.
4 ?- foo( A, [0,1,2,1,3], [0,1,2,4]).
false.
f ?- foo( A, [0,1,1], [0,1]).
A = 1 ;
A = 1 ;
false.
Попытка опровергнуть его контраргументом:
10 ?- dif(A1,A2), foo(A1,B,C), foo(A2,B,C).
Action (h for help) ? abort
% Execution Aborted
Прологу не удается найти контраргумент.
Стремление более внимательно увидеть, что происходит, с итеративным углублением:
28 ?- length(BB,NN), foo(AA,BB,CC), XX=[AA,BB,CC], numbervars(XX),
writeln(XX), (NN>3, !, fail).
[A,[A],[]]
[A,[A,B],[B]]
[A,[B,A],[B]]
[A,[A,B,C],[B,C]]
[A,[B,A,C],[B,C]]
[A,[B,C,A],[B,C]]
[A,[A,B,C,D],[B,C,D]]
false.
29 ?- length(BB,NN), foo(AA,BB,CC), foo(AA2,BB,CC),
XX=[AA,AA2,BB,CC], numbervars(XX), writeln(XX), (NN>3, !, fail).
[A,A,[A],[]]
[A,A,[A,B],[B]]
[A,A,[A,A],[A]]
[A,A,[A,A],[A]]
[A,A,[B,A],[B]]
[A,A,[A,B,C],[B,C]]
[A,A,[A,A,B],[A,B]]
[A,A,[A,A,A],[A,A]]
[A,A,[A,A,B],[A,B]]
[A,A,[B,A,C],[B,C]]
[A,A,[B,A,A],[B,A]]
[A,A,[A,A,A],[A,A]]
[A,A,[B,A,A],[B,A]]
[A,A,[B,C,A],[B,C]]
[A,A,[A,B,C,D],[B,C,D]]
false.
AA и AA2 всегда создаются для одной и той же переменной.
В числе 3 нет ничего особенного, поэтому с помощью обобщения можно с уверенностью предположить, что так будет всегда, при любой попытке.
Еще одна попытка прологологического доказательства:
ground_list(LEN,L):-
findall(N, between(1,LEN,N), NS),
member(N,NS),
length(L,N),
maplist( \A^member(A,NS), L).
bcs(N, BCS):-
bagof(B-C, A^(ground_list(N,B),ground_list(N,C),foo(A,B,C)), BCS).
as(N, AS):-
bagof(A, B^C^(ground_list(N,B),ground_list(N,C),foo(A,B,C)), AS).
proof(N):-
as(N,AS), bcs(N,BCS),
length(AS,N1), length(BCS, N2), N1 =:= N2.
Сравнивает количество успешных комбинаций B-C в целом с количеством A s, которые они производят. Равенство означает однозначное соответствие.
И вот так,
2 ?- proof(2).
true.
3 ?- proof(3).
true.
4 ?- proof(4).
true.
5 ?- proof(5).
true.
И так для любого N. Все медленнее и медленнее. Общий неограниченный запрос для написания тривиален, но замедление кажется экспоненциальным.