That's a very interesting topic and nice write-up, thank you for sharing!

For comparison, here is a small interpreter for a subset of Prolog, written in Prolog:

    mi([]).
    mi([G|Gs]) :-
            clause_(G, Body),
            mi(Body),
            mi(Gs).

This states that: First, the empty conjunction (of goals) is true, and second, if there is at least one goal left, than the conjunction is true if there is a suitable clause whose body evaluates to true, and the same holds for all remaining goals.

For example, we can define append/3 as follows in this representation:

    clause_(append([], Ys, Ys), []).
    clause_(append([X|Xs], Ys, [X|Zs]), [append(Xs,Ys,Zs)]).

and then evaluate it with our interpreter:

    ?- mi([append([a,b,c], [d,e], Ls)]).
    Ls = [a, b, c, d, e].

Characteristically, it also works in other directions. For example:

    ?- mi([append([a,b,c], Rs, [a,b,c,d,e])]).
    Rs = [d, e].

and also:

    ?- mi([append(As, Bs, [x,y])]).
    As = [],
    Bs = [x, y] ;
    As = [x],
    Bs = [y] ;
    As = [x, y],
    Bs = [] ;
    false.

Now the point: The clauses of the meta-interpreter itself can also be stated in this form, namely as:

    clause_(mi([]), []).
    clause_(mi([G|Gs]), [clause_(G,Body),mi(Body),mi(Gs)]).

Now we only have to define what clause_/2 means, which we can do with:

    clause_(clause_(G, Body), []) :- clause_(G, Body).

And now we can use our meta-interpreter to evaluate its own code as it interprets a program, arbitrarily deeply layered:

   ?- mi([mi([mi([append([a,b,c],[d,e],Ls)])])]).
   Ls = [a, b, c, d, e].

Hence, Prolog admits a meta-circular evaluator in at most 5 lines of code. With a better representation for clauses (using list differences), you can reduce the interpreter to 4 lines of code and at the same time make it tail-recursive.

Nice- but why only half a meta-interpreter? A complete Prolog meta-interpreter should still be able to interpret iself, no?

Yes, a complete Prolog meta-interpreter would definitely be meta-circular.

However, it is quite hard to write an interpreter for complete Prolog, both in Prolog and also in other languages. Take for example handling of !/0. It is not easy to add handling of !/0 to the meta-interpreter I showed, especially if you want to retain meta-circularity. You cannot simply use a !/0 on the meta-level, because that does not get cut transparency right. One way to express !/0 on the meta-level is to use catch/3 and throw/1. However, if you do this and want to retain meta-circularity, then you must also handle catch/3 and throw/1 correctly, and soon you really will have to handle almost the entire language, which is quite complex to implement even though it has a very simple syntactic structure.

With "cut transparency", I mean that the scope of !/0 depends on its context. For example, we have:

    ?- member(X, [a,b,c]), ( true -> ! ).
    X = a.

and on the other hand:

    ?- member(X, [a,b,c]), ( ! -> true ).
    X = a ;
    X = b ;
    X = c.

Such properties make an interpreter for complete Prolog rather complex, and for this reason I have shown a meta-circular interpreter that can handle only a (Turing-complete) subset of Prolog. Thank you for your interest!

Ah. My apologies. As usual I lack precision. I was thinking of a meta-interpreter for the logically pure subset of Prolog- no cuts, or exceptions.

That should be covered by the classic Prolog meta-interpreter, no? I mean this one:

  prove(true,_Ps).
  prove((L1,Ls),Ps):-
    prove(L1,Ps)
    prove(Ls,Ps).
  prove((L1),Ps):-
    clause(L1,B)
    prove(B,Ps).

This would work if clause/2 always failed if there is no matching clause. Indeed, in some systems, that was the case. But now, clause/2 may and will throw an error for example on:

    ?- clause(true, B).
    ERROR: No permission to access private_procedure `true/0'

See also the Prolog ISO standard:

    clause(+head, ?callable_term)

    8.8.1.3 Errors

      ...
      c) The predicate indicator Pred of Head is that of a
      private procedure
      - permission_error(access, private_procedure, Pred).
      ...

In this interpreter, the third clause of prove/2 is also applicable if the others are applicable, because L1 subsumes both true and terms of the form (X,Y). For this reason, we get for example:

   ?- prove((true,true), _), false.
   ERROR: No permission to access private_procedure `true/0'

whereas we expect this to succeed, because (true,true) does. Hence, to make this interpreter actually work, more must be added, and to make it meta-circular (i.e., able to interpret its own code), these features must then also be handled.

In the representation I used, these issues do not arise because I am using a so-called clean representation. With such a representation, I can tell for certain what the individual goals are, as the individual goals are symbolically distinguished from conjunctions of goals.