Path: utzoo!utgpu!water!watmath!clyde!bellcore!rutgers!cmcl2!nrl-cmf!ames!joyce!sri-unix!quintus!ok
From: ok@quintus.uucp (Richard A. O'Keefe)
Newsgroups: comp.lang.prolog
Subject: Re: meta-circular-meta-interpreters (long)
Message-ID: <307@quintus.UUCP>
Date: 24 Aug 88 08:49:18 GMT
References: <1170@tuhold>
Sender: news@quintus.UUCP
Reply-To: ok@quintus.UUCP (Richard A. O'Keefe)
Organization: Quintus Computer Systems, Inc.
Lines: 42

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.