ok@quintus (07/26/88)
I have finally seen the "vanilla interpreter" one time too many:
prove(true).
prove((A,B)) :-
prove(A),
prove(B).
prove(H) :-
clause(H, B),
prove(B).
It is time somebody told the truth about this:
(1) it is DISGUSTING
(2) in DEC-10 Prolog, it worked (well, sort of) only by accident
(3) it doesn't work in Quintus Prolog
(4) it is intrinsically inefficient.
Why is it disgusting? Because the third clause claims to be
applicable in ALL cases (it imposes no restrictions whatsoever
on H), but that isn't really so. Consider, for example, the
query
| ?- prove((true, not_so)).
where clause(not_so, _) fails. What happens?
(a) prove((true, not_so)) matches, *leaving a choice-point behind*
then calls prove(true)
(b) prove(true) matches *leaving a choice-point behind*
and succeeds
(c) prove((true, not_so)) continues,
and calls prove(not_so)
(d) prove(not_so) calls clause(not_so, B), which fails.
(e) THE CHOICE POINT LEFT IN STEP b IS REACTIVATED.
prove(true) matches the third clause,
and calls clause(true, B).
This either succeeds with B=true (in which case we have a loop),
or fails (DEC-10 Prolog), or reports an error (Quintus Prolog).
Similarly, the choice point left in step a can be reactivated.
The point is that clause 3 is applied in cases where it is not appropriate.
So, it is intrinsically inefficient because every true and (_,_) leaves
a choice point behind. To eliminate those choice points, a compiler would
have to know that clause(true, _) and clause((_,_), _) fail (which would
have to be true).
In DEC-10 Prolog, clause(BuiltIn, _) failed. It is not clear that this
was deliberate: assert((BuiltIn :- Anything)) would succeed quietly (with
no detectable change to the data base or the builtin).
In Quintus Prolog, any attempt to apply clause/2 to a predicate which has
not been explicitly declared :-dynamic is reported as an error.
(This is to be consistent with clause/3, which must report the error,
otherwise you would have a back-door way of changing things.)
What can you do instead?
It is possible to correct the program as it stands by adding a cut to
each of the first two clauses, or by adding an explicit test (in
Quintus Prolog:
predicate_property(H, (dynamic)) )
to the third clause. The first alternative is ugly, and the second
is inefficient.
A general rule for "defaulty" representations (such as here, where a
user goal is identified as such only by not being recognised as
anything else) is to translate them to a clean representation and
work on the clean version. In this case, a good representation for
H :- B1, ..., Bn.
is
rule(H, [B1,...,Bn|C], C).
You can hook built-in predicates into this representation thus:
rule(p(X,..,Z), C, C) :- p(X,...,Z).
e.g.
rule(rule(H,B0,B), C, C) :-
rule(H, B0, B).
With this representation, we have
prove_goal(G) :-
prove_conj([G]).
prove_conj([]).
prove_conj([G|Gs]) :-
rule(G, Gs1, Gs),
prove_conj(Gs1).
If you want to experiment with this, here is the definition of rule/3
for naive reverse and a meta-circular version of prove_goal/1:
rule(reverse([],[]), C, C).
rule(reverse([H|T], R), [
reverse(T, L),
append(L, [H], R) |C], C).
rule(append([],R,R), C, C).
rule(append([H|T], L, [H|R]), [
append(T, L, R) |C], C).
rule(prove_goal(G), [
prove_conj([G]) |C], C).
rule(prove_conj([]), C, C).
rule(prove_conj([G|Gs]), [
rule(G, Gs1, Gs),
prove_conj(Gs1) |C], C).
rule(rule(H, B0, B), C, C) :-
rule(H, B0, B).
Question: can a meta-_circular_ interpreter be (finitely) well-typed?
Note that this prove_goal/1 and its associated clauses are plain Horn
clauses (e.g. no cuts), so it is quite easy to manipulate it formally.