🚀 go-pugleaf

In article <1170@tuhold> thom@tuhold (Thom Fruehwirth) writes:
>Some time ago <ok@quintus> wrote on Meta-circular interpreters:
>I appreciate O'Keefe's 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.

But the "vanilla meta-interpreter" is broken as a specification:
it demands that clause(true, Body) and clause((X,Y), Body) *should*
be called, and should fail.  In a Prolog system which distinguishes
between predicates you can change and predicates you can't, you are
likely to get error messages when you run the "vanilla meta-interpreter".
If the V M-I were written as
	prove(true).
	prove((X,Y)) :-
		prove(X),
		prove(Y).
	prove(H) :-
		H ~= true,
		H ~= (_,_),
		clause(H, B),
		prove(B).
then the "it's only a specification" argument would go be valid.
{I claim that clause((_,_), _) SHOULD report an error in every Prolog;
 (_,_) has a definition, it's just that the Prolog system refuses to
 show it do you.}
Alternatively, the last clause of the V M-I could be written as
	prove(H) :-
		current_predicate(_, H),
		clause(H, B),
		prove(B).
to make it explicit that clause/2 is only to be called on user-defined
predicates.

>In fact, I will show that O'Keefe's suggestion is an implementation
>version derivable from a specification based on the vanilla meta-
>interpreter.

The derivation in question does not preserve semantics.  (The V M-I can
be talked into calling rule(true, _) and rule(_,_), _), the "derived"
version can't.)  When P and Q compute different functions, it is not
clear that P can be regarded as an implementation of Q.