Prolog:"chili" 表达调用堆栈和选择点的解释器

Prolog: "chili" interpreter that expresses call stack and choice points

通常的普通解释器使用 Prolog 回溯 本身存档回溯。我想这就是原因 为什么叫 "vanilla":

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

"chili" 解释器怎么样,它不使用任何 Prolog 回溯。基本上一个谓词first/?来获取 第一个解决方案和谓词 next/? 以获得进一步的解决方案。

如何在 Prolog 中实现这样的解释器。解决方案不必是纯粹的,也可以使用 findall 和 cut。尽管更纯粹的解决方案也可以说明问题。

此解决方案是 下 Markus Triska 的 A Couple of Meta-interpreters in PrologProlog 的力量 的一部分)中给出的解释器的略微简化版本具体化回溯。它有点冗长且效率较低,但可能比该代码更容易理解。

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 返回,我们继续其他选择。请注意当没有找到目标的子句时,即它 "fails"、Choices1[] 统一并且我们 "backtrack" 通过 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).

通过差异列表的规则和事实表示如下查找 Peano 算术:

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]]]