Metacircular Interpreter (Prolog)

A metacircular interpreter is an interpreter written in its own language which means it can interpret itself.


The following code can be found in the examples directory of the Barry's Prolog distribution.

The following Prolog code implements a metacircular Prolog interpreter — to be correct it is a metacircular interpreter for a pure Prolog. The heart of the interpreter is the procedure demo(Goal, Clauses). This succeeds if we can prove that Goal is a logical consequence of Clauses. The procedure demo/2 is an interpreter for pure Prolog which makes use of the following built-in predicates:

The reason for copy_term/2 is because we need a fresh copy of the clauses when we search to find a clause head that matches Goal. Since the intention is for demo/2 to be applied to itself, we implement these built-in predicates in demo/2 itself.

Although demo/2 uses member/2, the predicate member/2 doesn't have to be a built-in predicate, we can include a definition for it in Clauses. This is what we will do below.

demo((Goal1, Goal2), Clauses) :-             %%% Conjunction.
	demo(Goal1, Clauses),
	demo(Goal2, Clauses).
demo((Goal1; Goal2), Clauses) :-             %%% Disjunction.
	demo(Goal1, Clauses)
	demo(Goal2, Clauses).
demo(true, _) :- true.                       %%% Built-in predicate true/0.
demo(copy_term(A, B), _) :-                  %%% Built-in predicate copy_term/2
	copy_term(A, B).
demo(Goal, Clauses) :-                       %%% Look up a clause
	copy_term(Clauses, ClausesCopy),
	member((Goal :- Body), ClausesCopy),
	demo(Body, Clauses).

A call of metacircular_demo(Goal) succeeds if we can prove that we can prove Goal. This is the interpreter top-level. We collect all of the clauses for demo/2 and add in clauses for member/2. We then pass these these along with Goal to demo/2 via demo/2, i.e we use demo/2 to interpret demo/2 — we have a metacircular interpreter.

metacircular_demo(Goal) :-
	findall((demo(G, C) :- Body), clause(demo(G, C), Body), Clauses),
	AllClauses = [(member(A, [A|_]) :- true), (member(A, [_|T]) :- member(A, T))|Clauses],
	demo(demo(Goal, AllClauses), AllClauses).