negation \+ and vanilla meta-interpreter

Question

The following is the classic "textbook" vanilla meta-interpreter for prolog.

% simplest meta-interpreter
solve(true) :- !.
solve((A,B)):- !, solve(A), solve(B).
solve(A) :- clause(A,B), solve(B).

The following is simple program which establishes facts two relations which are "positive" and one relation which makes use of negation by failure \+.

% fruit
fruit(apple). 
fruit(orange). 
fruit(banana).

% colour
yellow(banana).

% Mary likes all fruit 
likes(mary, X) :- fruit(X).

% James likes all fruit, as long as it is yellow
likes(james, X) :- fruit(X), yellow(X).

% Sally likes all fruit, except yellow fruit
likes(sally, X) :- fruit(X), \+ (yellow(X)).

The meta-interpeter can handle goals related to the first two relations ?-solve(likes(mary,X)) and ?- solve(likes(james,X)_.

However it fails with a goal related to the third relation ?- solve(likes(sally,X). The swi-prolog reports a stack limit being reached before the program crashes.

Question 1: What is causing the meta-interpreter to fail? Can it be easily adjusted to cope with the \+ negation? Is this related to the sometimes discussed issue of built-ins not being executed by the vanilla meta-interpreter?

Question 2: Where can I read about the need for those cuts in the vanilla meta-interpreter?

---

Tracing suggests the goal is being grown endlessly:

clause(\+call(call(call(call(yellow(apple))))),_5488)
 Exit:clause(\+call(call(call(call(yellow(apple))))),\+call(call(call(call(call(yellow(apple)))))))
 Call:solve(\+call(call(call(call(call(yellow(apple)))))))
 Call:clause(\+call(call(call(call(call(yellow(apple)))))),_5508)
 Exit:clause(\+call(call(call(call(call(yellow(apple)))))),\+call(call(call(call(call(call(yellow(apple))))))))
 Call:solve(\+call(call(call(call(call(call(yellow(apple))))))))

Answer 1

Change solve(A) into:

solve(Goal) :-
    writeln(Goal),
    sleep(1),
    clause(Goal, Body),
    solve(Body).

... and we see:

?- solve_mi(likes(sally,X)).
likes(sally,_8636)
fruit(_8636)
\+yellow(apple)
\+call(yellow(apple))
\+call(call(yellow(apple)))
\+call(call(call(yellow(apple))))
...

clause/2 determines the body of \+yellow(apple) to be \+call(yellow(apple)), which is not a simplification.

Can use instead:

solve_mi(true) :-
    !.
solve_mi((Goal1, Goal2)):-
    !,
    solve_mi(Goal1),
    solve_mi(Goal2).
solve_mi(\+ Goal) :-
    !,
    \+ solve_mi(Goal).
solve_mi(Goal) :-
    clause(Goal, Body),
    solve_mi(Body).

Result in swi-prolog:

?- solve_mi(likes(sally,X)).
X = apple ;
X = orange ;
false.

I'm using solve_mi because solve conflicts with e.g. clpBNR, and I'm not using variable names A and B because they convey no meaning.

For understanding the cuts, I'd recommend gtrace, to see the unwanted unification with other goals that would otherwise take place.