Это решение является слегка тупой версией интерпретатора, приведенного в Пара мета-интерпретаторов в Прологе (часть Сила Пролога ) в * 1005. * Рейтинг откат . Это немного более многословно и менее эффективно, но, возможно, немного более понятно, чем этот код.
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]).
Идея состоит в том, что состояние механизма Пролога представляется в виде дизъюнктивного списка 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
делает много копий резольвенты, то есть оставшегося сочетания целей, которые должны быть доказаны в дизъюнктивной ветви. Я хотел бы видеть более эффективное решение, где термины копируются, а переменные делятся более разумно.