Блог

Обычный ванильный интерпретатор использует обратное отслеживание Prolog для архивирования обратного отслеживания. Я думаю, это причина, по которой его называют «ванильным»:

 solve(true).
solve((A,B)) :- solve(A), solve(B).
solve(H) :- clause(H, B), solve(B).
 

Как насчет интерпретатора «чили», который не использует никакого
обратного отслеживания пролога. В основном сначала предикат /?чтобы получить
первое решение и следующий предикат /?для получения дальнейших решений.

Как бы это сделать и реализовать такой интерпретатор в Prolog. Решение не обязательно должно быть чистым, также можно использовать findall и cut . Хотя более чистое решение также может быть иллюстративным.

Это решение представляет собой слегка упрощенную версию интерпретатора, приведенную в книге Маркуса Триски «Пара метаинтерпретаторов в Prolog» (часть возможностей Prolog), использующую повторное отслеживание. Он немного более подробный и менее эффективный, но, возможно, немного более понятный, чем этот код.

 first(Goal, Answer, Choices) :-
    body_append(Goal, [], Goals),
    next([Goals-Goal], Answer, Choices).

next([Goals-Query|Choices0], Answer, Choices) :-
    next(Goals, Query, Answer, Choices0, Choices).

next([], Answer, Answer, Choices, Choices).
next([Goal|Goals0], Query, Answer, Choices0, Choices) :-
    findall(Goals-Query, clause_append(Goal, Goals0, Goals), Choices1),
    append(Choices1, Choices0, Choices2),
    next(Choices2, Answer, Choices).

clause_append(Goal, Goals0, Goals) :-
    clause(Goal, Body),
    body_append(Body, Goals0, Goals).

body_append((A, B), List0, List) :-
    !,
    body_append(B, List0, List1),
    body_append(A, List1, List).
body_append(true, List, List) :-
    !.
body_append(A, As, [A|As]).
 

Идея заключается в том, что состояние движка Prolog представляется в виде дизъюнктивного списка Choices , играющего роль стека точек выбора. Каждый выбор имеет вид Goals-Query , где Goals представляет собой объединенный список целей, которые еще предстоит выполнить, то есть разрешающий элемент в этом узле дерева SLD, и Query является экземпляром исходного термина запроса, переменные которого были созданы в соответствии с объединениями, выполненными на пути, ведущем к этому узлу.

Если разрешающая способность выбора становится пустой, его Query экземпляр возвращается как Answer , и мы продолжаем с другими вариантами. Обратите внимание, как, когда для цели не найдено ни одного предложения, т. Е. Она «терпит неудачу», Choices1 объединяется с [] , и мы «возвращаемся назад», проходя через оставшиеся варианты в Choices0 . Также обратите внимание, что, когда в списке нет вариантов, next/3 происходит сбой.

Пример сеанса:

 ?- assertz(mem(X, [X|_])), assertz(mem(X, [_|Xs]) :- mem(X, Xs)).
true.

?- first(mem(X, [1, 2, 3]), A0, S0), next(S0, A1, S1), next(S1, A2, S2).
A0 = mem(1, [1, 2, 3]),
S0 = [[mem(_G507, [2, 3])]-mem(_G507, [1, 2, 3])],
A1 = mem(2, [1, 2, 3]),
S1 = [[mem(_G579, [3])]-mem(_G579, [1, 2, 3])],
A2 = mem(3, [1, 2, 3]),
S2 = [[mem(_G651, [])]-mem(_G651, [1, 2, 3])].
 

Проблема с этим подходом заключается в том, что findall/3 выполняется большое копирование разрешающей способности, т.Е. Оставшегося соединения целей, которые должны быть доказаны в дизъюнктивной ветви. Мне бы хотелось увидеть более эффективное решение, в котором термины копируются, а переменные используются более разумно.

Вот небольшая вариация овеществленного обратного отслеживания с использованием списков различий.

 first(G, [[]|L], R) :- !, first(G, L, R). %% choice point elimination
first([A], L, [A|L]) :- !.
first([H|T], L, R) :- findall(B, rule(H,B,T), [B|C]), !, first(B, [C|L], R).
first(_, L, R) :- next(L, R).

next([[B|C]|L], R) :- !, first(B, [C|L], R).
next([_|L], R) :- next(L, R).
 

Представление правил и фактов с помощью списков различий ищет арифметику Пеано следующим образом:

 rule(add(n,X,X),T,T).
rule(add(s(X),Y,s(Z)),[add(X,Y,Z)|T],T).

rule(mul(n,_,n),T,T).
rule(mul(s(X),Y,Z),[mul(X,Y,H),add(Y,H,Z)|T],T).
 

И вы можете запускать запросы следующим образом:

 ?- first([mul(s(s(n)),s(s(s(n))),X),X],[],[X|L]).
X = s(s(s(s(s(s(n))))))
L = []

?- first([add(X,Y,s(s(s(n)))),X-Y],[],[X-Y|L]).
X = n
Y = s(s(s(n)))
L = [[[add(_A,_B,s(s(n))),s(_A)-_B]]]

?- first([add(X,Y,s(s(s(n)))),X-Y],[],[_|L]), next(L,[X-Y|R]).
L = [[[add(_A,_B,s(s(n))),s(_A)-_B]]],
X = s(n)
Y = s(s(n))
R = [[[add(_C,_D,s(n)),s(s(_C))-_D]]]