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

Question

The usual vanilla interpreter uses Prolog backtracking itself to archive backtacking. I guess this is the reason why its called "vanilla":

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

How about a "chili" interpreter, that doesn't use any Prolog backtracking. Basically a predicate first/? to obtain a first solution and a predicate next/? to obtain further solutions.

How would one go about it and realize such an interpreter in Prolog. The solution needs not be pure, could also use findall and cut. Although a purer solution could be also illustrative.

Answer 1

Here is a slight variation of reified backtracking, using difference lists.

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).

Representation of rules and facts via difference lists looks for Peano arithmetic as follows:

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).

And you can run queries as follows:

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

Answer 2

This solution is a slightly dumbed-down version of the interpreter given in Markus Triska's A Couple of Meta-interpreters in Prolog (part of The Power of Prolog) under Reifying backtracking. It is a bit more verbose and less efficient, but possibly a bit more immediately understandable than that code.

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

The idea is that the Prolog engine state is represented as a list of disjunctive Choices, playing the role of a stack of choice points. Each choice is of the form Goals-Query, where Goals is a conjunctive list of goals still to be satisfied, i.e. the resolvent at that node of the SLD tree, and Query is an instance of the original query term whose variables have been instantiated according to the unifications made in the path leading up to that node.

If the resolvent of a choice becomes empty, it's Query instantiation is returned as an Answer and we continue with other choices. Note how when no clauses are found for a goal, i.e. it "fails", Choices1 unifies with [] and we "backtrack" by proceeding through the remaining choices in Choices0. Also note that when there are no choices in the list, next/3 fails.

An example session:

?- 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])].

The problem with this approach is that findall/3 does a lot of copying of the resolvent i.e. the remaining conjunction of goals to be proved in a disjunctive branch. I would love to see a more efficient solution where terms are copied and variables shared more cleverly.