Ответ 1

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

Например, давайте возьмем этот простой случай:

same_term(X, X).

Это предикат, который определяет связь между двумя аргументами. Через объединение говорится, что первый и второй аргументы одинаковы, если они объединены (и это определение зависит от нас, авторов предиката). Таким образом, same_term(a, a) будет успешным, same_term(a, b) завершится неудачей, а same_term(a, X) будет успешным с X = a.

Вы также можете написать это в более явной форме:

same_term(X, Y) :-
    X = Y.  % X and Y are the same if they are unified

Теперь давайте посмотрим на ваш пример, val_and_remainder/3. Во-первых, что это значит?

val_and_remainder(X, List, Rest)

Это означает, что X является элементом List а Rest является списком, состоящим из всех остальных элементов (без X). (ПРИМЕЧАНИЕ: Вы не объяснили это значение сразу, но я определяю это значение из реализации вашего примера.)

Теперь мы можем написать, чтобы описать правила. Во-первых, простой базовый случай:

val_and_remainder(X,[X|Xs],Xs).

Это говорит о том, что:

Xs - это остаток списка [X|Xs] без X

Это утверждение должно быть достаточно очевидным по определению синтаксиса [X|Xs] для списка в Прологе. Вам нужны все эти аргументы, потому что третий аргумент Xs должен объединяться с хвостом (остатком) списка [X|Xs], который также является Xs (переменные с одинаковыми именами, по определению, унифицированы). Как и раньше, вы можете написать это более подробно как:

val_and_remainder(X, [H|T], R) :-
    X = H,
    R = T.

Но краткая форма на самом деле более понятна.

Теперь рекурсивное предложение гласит:

val_and_remainder(X, [Y|Ys], [Y|R]) :- 
    val_and_remainder(X, Ys, R).

Итак, это означает:

[Y|R] является остатком списка [Y|Ys] без X если R является остатком списка Ys без элемента X

Вам нужно подумать об этом правиле, чтобы убедить себя, что оно логически верно. Y является одинаковым во втором и третьем аргументах, потому что они ссылаются на один и тот же элемент, поэтому они должны объединяться.

Таким образом, эти два предложения предиката формируют два правила, которые охватывают оба случая. Первый случай - это простой случай, когда X является первым элементом списка. Второй случай - это рекурсивное определение, когда X не является первым элементом.

Когда вы делаете запрос, например, val_and_remainder(2, [1,2,3], R). Пролог ищет, может ли он объединить термин val_and_remainder(2, [1,2,3], R) с фактом или val_and_remainder(2, [1,2,3], R) одного из ваших предикатных предложений. Он терпит неудачу в своей попытке объединиться с val_and_remainder(X,[X|Xs],Xs) потому что ему нужно объединить X с 2, что означает, что ему нужно объединить [1,2,3] с [2|Xs] что не удается, поскольку первый элемент в [1,2,3] равен 1, но первый элемент в [2|Xs] равен 2.

Таким образом, Пролог val_and_remainder(2, [1,2,3], R) и успешно объединяет val_and_remainder(2, [1,2,3], R) с val_and_remainder(X,[Y|Ys],[Y|R]), объединяя X с 2, Y с 1, Ys с [2,3] и R с [Y|R] (ПРИМЕЧАНИЕ, это важно, переменная R в вашем вызове НЕ совпадает с переменной R в определении предиката, поэтому мы должны назвать это R1 чтобы избежать этой путаницы). Мы назовем ваш R как R1 и скажем, что R1 объединен с [Y|R].

Когда выполняется тело второго предложения, оно вызывает val_and_remainder(X,Ys,R). или, другими словами, val_and_remainder(2, [2,3], R). Теперь это объединится с первым предложением и даст вам R = [3]. Когда вы раскручиваете все это, вы получаете, R1 = [Y|[3]], и, вспоминая, что Y был связан с 1, в результате получается R1 = [1,3].

Ответ 2

Из комментария:

Насколько верен результат R, потому что, если вы посмотрите на мой прогон вызова программы, значение Xs не равно [1,3], что в итоге и выдает; вместо этого [3] объединяется с R (ясно, что я что-то упускаю по пути, но я не уверен, что это такое).

Это правильно:

% Initial call
val_and_remainder(2, [1,2,3], R).

val_and_remainder(2, [1|[2,3]], [1|R]) :- val_and_remainder(2, [2,3], R).

% Hits base case
val_and_remainder(2, [2|[3]], [3]).

однако Prolog не похож на другие языки программирования, где вы входите с помощью input и выходите с помощью output в операторе return. В Прологе вы продвигаетесь вперед по предикатным операторам, объединяющим и продолжающим работу с предикатами, которые являются истинными, а после возврата также объединяете несвязанные переменные. (Это технически неверно, но для некоторых это легче понять, если вы думаете об этом таким образом.)

Вы не приняли во внимание несвязанные переменные, которые теперь связаны с возвратом.

Когда вы попали в базовый случай, Xs был связан с [3],

но когда вы возвращаетесь назад, вы смотрите на

val_and_remainder(2, [1|[2,3]], [1|R])

и, в частности, [1|R] для третьего параметра.

Поскольку Xs был объединен с R в обращении к базовому случаю, т.е.

val_and_remainder(X,[X|Xs],Xs).

R теперь имеет [3].

Теперь третий параметр позиции в

val_and_remainder(2, [1|[2,3]], [1|R])

это [1|R] есть [1|[3]] который в качестве синтаксического сахара равен [1,3] а не только [3].

Теперь, когда запрос

val_and_remainder(2, [1,2,3], R).

был запущен, третий параметр запроса R был объединен с третьим параметром предиката

val_and_remainder(X,[Y|Ys],[Y|R])

таким образом, R был объединен с [Y|R] который отменяет обратное отслеживание, является [1,3] и, таким образом, значение, связанное с переменной запроса R является [1,3]

Ответ 3

Пошаговое воспроизведение механизма Пролог часто приводит к большей путанице, чем помогает. У вас, вероятно, есть такие понятия, как "возвращение", означающее нечто очень конкретное - более подходящее для императивных языков.

Вот разные подходы, которые вы всегда можете использовать:

Задайте самый общий запрос

... и пусть Пролог объяснит вам, о чем идет речь.

| ?- val_and_remainder(X, Xs, Ys).
     Xs = [X|Ys]
  ;  Xs = [_A,X|_B],
     Ys = [_A|_B]
  ;  Xs = [_A,_B,X|_C],
     Ys = [_A,_B|_C]
  ;  Xs = [_A,_B,_C,X|_D],
     Ys = [_A,_B,_C|_D]
  ;  Xs = [_A,_B,_C,_D,X|_E],
     Ys = [_A,_B,_C,_D|_E]
  ; ...

Таким образом, Xs и Ys имеют общий префикс списка, после которого Xs имеет X, за которым следует общий остаток. Этот запрос будет продолжать производить дальнейшие ответы. Иногда вы хотите увидеть все ответы, тогда вам нужно быть более конкретным. Но не будьте слишком конкретны:

| ?- Xs = [_,_,_,_], val_and_remainder(X, Xs, Ys).
     Xs = [X,_A,_B,_C],
     Ys = [_A,_B,_C]
  ;  Xs = [_A,X,_B,_C],
     Ys = [_A,_B,_C]
  ;  Xs = [_A,_B,X,_C],
     Ys = [_A,_B,_C]
  ;  Xs = [_A,_B,_C,X],
     Ys = [_A,_B,_C]
  ;  false.

Итак, здесь мы получили все возможные ответы для четырехэлементного списка. Все они.

Придерживайтесь наземных целей при прохождении определенных умозаключений

Так что вместо val_and_remainder(2, [1,2,3], R). (что, очевидно, val_and_remainder(2, [1,2,3], [1,3]).), рассмотрим val_and_remainder(2, [1,2,3], [1,3]). а затем val_and_remainder(2, [2,3],[3]). С этой стороны это должно быть очевидно.

Прочитайте правила Пролога справа налево

Смотрите правила Пролога как правила производства. Таким образом, всякий раз, когда все имеет место в правой части правила, вы можете заключить, что слева. Таким образом, :- это представление ранних 1970 - й года из ←

Позже вы можете подумать и о более сложных вопросах. подобно

Функциональные зависимости

Первый и второй аргументы однозначно определяют последний? Имеет ли место X, Xs → Ys?

Ниже приведен пример запроса, который запрашивает Ys и Ys2 быть различным для одной и той же X и Xs.

| ?- val_and_remainder(X, Xs, Ys), val_and_remainder(X, Xs, Ys2), dif(Ys,Ys2).
     Xs = [X,_A,X|_B],
     Ys = [_A,X|_B],
     Ys2 = [X,_A|_B],
     dif([_A,X|_B],[X,_A|_B])
  ;  ...

Таким образом, по-видимому, существуют разные значения Ys для данных X и Xs. Вот конкретный пример:

| ?- val_and_remainder(x, [x,a,x], Ys).
     Ys = [a,x]
  ;  Ys = [x,a]
  ;  false.

Здесь нет классического возвращения. Возвращается не один раз, а дважды. Это больше yield.

Тем не менее, есть на самом деле функциональная зависимость между аргументами! Вы можете найти это? И можете ли вы Прологом доказать это (так же, как Пролог действительно может сделать доказательство).

Ответ 4

Я не понимаю имя вашего предиката. В любом случае, это отвлечение. Неравномерное именование переменных также отвлекает. Давайте используем некоторые нейтральные короткие однослоговые имена, чтобы сосредоточиться на самом коде в его самой ясной форме:

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

Цели между |- и ? являются резольвентой, уравнения внутри { } являются заменой. База знаний (КБ) неявно слева от |- полностью.

На каждом шаге выбирается самая левая цель в резольвенте, из которых в КБ выбирается предложение с совпадающей головой ^{(при последовательном переименовании всех переменных предложения, так что ни одна переменная в резольвенте не используется переименованным предложением, поэтому нет случайного захвата переменной)} и выбранная цель заменяется в резольвенте этим телом предложения, в то время как успешное объединение добавляется в подстановку. Когда резольвента пуста, запрос был проверен, и мы видим единственную успешную ветвь and-in во всем дереве and-or.

Вот как машина может это делать. Этапы "переписать" представлены здесь для облегчения понимания человеком.

Итак, мы видим здесь, что первый успешный выбор предложения приводит к уравнению

     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.

Это сравнивает количество успешных комбинаций BC целом с количеством A они производят. Равенство означает однозначное соответствие.

И так мы имеем,

2 ?- proof(2).
true.

3 ?- proof(3).
true.

4 ?- proof(4).
true.

5 ?- proof(5).
true.

И так для любого N это имеет место. Все медленнее и медленнее. Обычный, неограниченный запрос писать тривиально, но замедление кажется экспоненциальным.