🚀 go-pugleaf

Some time ago <ok@quintus> wrote on Meta-circular interpreters:
>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.
>..... 
>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...
>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).

I appreciate O'Keefes very sophisticated solution utilizing difference
lists. But one should not compare it directly with the vanilla meta-
interpreter. The latter is more towards a specification while the 
former is more towards an implementation. The handling of built-in
predicates emphasizes this:
>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).
(Somebody might have the idea to add a rule for the conjunction ','/2,
as
it is also a built-in).

In fact, I will show that O'Keefes suggestion is a implementation
version derivable form a specification based on the vanilla meta-
interpreter.

>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...
I did experiments in AAIS-Prolog on the Mac and - surprise!,surprise! -
both the vanilla (as defined just below)  and meta-circular version 
have about the same speed and adding cuts to either of them does not 
increase speed significantly !

For the specification of the meta-interpeter I will use user defined 
rule/2 instead of the built-in clause/2:
    
    prove(true).
    prove((H,Hs)) :-
 	prove(H),
        prove(Hs).
    prove(H) :-
        rule(H, B),
        prove(B).

Now we derive the implementation. As it is the case with O'Keefes 
meta circular-meta-interpreter we do not handle left-paranthesized
subgoals (e.g. ((a,b),c) ). Therefore the first subgoal in a conjunction
can directly call rule/2:

    prove(true).
    prove((H,Hs)) :-
        rule(H,B),
	prove(B),
        prove(Hs).
    prove(H) :-
        rule(H, B),
        prove(B).

Next we change the representation of the rules from
	rule(A,(B1,B2..,Bn)) into rule(A,[B1,B2..,Bn])
so that every clause-body ends in the empty list '[]'. Therefore the 
third clause of prove/2 can be removed:

    prove([]).
    prove([H|Hs]) :-
        rule(H,B),
	prove(B),
        prove(Hs).

Now we fold the two recursive subgoals into one with help of append/3:
	
    prove([]).
    prove([H|Hs]) :-
        rule(H,B),
	append(B,Hs,H1),
	prove(H1).

Then we use difference lists in rule/2 to get rid of append again by
transforming 
	rule(A,[B1,B2..,Bn]) into rule(A,[B1,B2..,Bn|Gs],Gs)
and result in O'Keefes meta-circular-meta-interpreter:
   
    prove([]).
    prove([H|Hs]) :-
        rule(H,Hs1,Hs),
	prove(Hs1).

We could have also choosen the transformation
	rule(A,[B1,B2..,Bn]) into rule([A|Gs],[B1,B2..,Bn|Gs])
which gives in a strinkingly simple looking but less efficient version:

    prove([]).
    prove(Gs) :-
          rule(Gs, Gs1),
	  prove(Gs1).

Concluding, O'Keefes meta-circular-meta-interpreter is a 
master-piece resulting from year-long experience. Although there may
be applications where the vanilla version is more efficient.