Our previous meta-interpreter can work with prolog programs that consist only of rules with zero or one goal in their body. Here we'll extend it to work with rules that have multiple goals. We'll then test our improved meta-interpreter with recursive programs.
We'll also see how to extend our meta-interpreter to work with programs that use built-ins like unification =/2.
% Example 18 - Meta-Interpreter For Multiple Goals
% are two lists the same?
same([],[]).
same([H1|T1],[H2|T2]) :- H1=H2, same(T1,T2).
% meta-interpreter for rules with multiple goals
prove(true) :- !.
prove(A=B) :- !, A=B.
prove((A,B)):- !, prove(A), prove(B).
prove(H) :- clause(H,B), prove(B),
write(H), write(" ← "), writeln(B).
We'll use the property same/2 we developed earlier to test if two lists are the same. It is a short definition, but it is recursive, has a rule with more than one goal, and also uses a built-in =/2, so it will be a good test for our meta-interpreter.
Unification =/2 Is A Property
Seeing unification written as =/2 might seem odd, but it is a property just like any other.
We write =/2 with an arity of 2 because it takes two parameters. Prolog's canonical form is =(A,B). Let's try it.
?- =(A,3), =(B,[A,A]).
A = 3
B = [3,3]
The infix form A=B is for our convenience.
Head And Tail Of Many Goals
Let's review how our previous meta-interpreter handles rules where the body has at most one goal.
prove(true) :- !.
prove(H) :- clause(H,B), prove(B).
If a rule matches the head H, the variable B is left unified with that single body goal. If the rule is a fact, then B is simply true, and this is resolved by prove(true):-!. If the rule is a relation, then B is a single goal, resolved recursively by prove(B) until it succeeds with a fact, or fails.
What happens if the rule has more than one goal? To explore this, let's create a test(X) rule that has three goals, one(X), two(X), and three(X).
% test rule with three goals
test(X) :- one(X), two(X), three(X).
We want to retain the recursive nature of our meta-interpreter as we work our way through this conjunctive sequence of goals. To do this we need a way to pick off the head of a sequence of goals, just like [H|T] picks off the head of a list of things.
Luckily, prolog allows us to do this just as easily. Let's see how it works.
?- clause(test(X), B).
B = (one(X),two(X),three(X))
We've used clause/2 to get the body of test(X) as B. Prolog reports B=(one(X),two(X),three(X)). We can see the sequence of goals grouped inside a pair of round brackets ().
Let's now pick off the first goal.
?- clause(test(X), B), B=(H1, T1).
B = (one(X),two(X),three(X)),
H1 = one(X),
T1 = (two(X),three(X))
We've unified B with (H1,T1). This leaves H1=one(X), the first goal in B, and T1 becomes the sequence of remaining goals. H1 and T1 are, in effect, the head and tail of the sequence B.
Let's continue and pick off the first goal from the sequence T1.
?- clause(test(X), B), B=(H1, T1), T1=(H2, T2).
B = (one(X),two(X),three(X)),
H1 = one(X),
H2 = two(X),
T1 = (two(X),three(X)),
T2 = three(X)
Unifying T1 with (H2,T2) results in H2=two(X), the first goal in T1, and the second goal in B.
Here T2=three(X) is not left as a goal wrapped in round brackets, but a single goal itself. This is different to how [H|T] works with lists, where the last tail is a list of one item. This doesn't cause any problems because our meta-interpreter already handles proving single goal bodies.
Meta-Interpreter For Rules With Multiple Goals
Let's update our meta-interpreter.
% meta-interpreter for rules with multiple goals
prove(true) :- !.
prove((A,B)):- !, prove(A), prove(B).
prove(H) :- clause(H,B), prove(B),
write(H), write(" ← "), writeln(B).
We've only added a single rule to our meta-interpreter, prove((A,B)). Let's talk through how it works.
If a rule has a body with multiple goals, then clause(H,B) will leave B as a sequence of goals wrapped in round brackets. The new meta-interpreter rule prove((A,B)) matches such a sequence of goals wrapped in round brackets and, as we have just seen, A is unified with the first goal, and B is unified with the remaining sequence. The first goal is handled by prove(A), and the remaining sequence is handled recursively by prove(B). Eventually B will be a single goal, handled as before by the meta-interpreter.
As is common with prolog, that short line of code belies the amount of thinking behind it.
Meta-Interpreting A Recursive Program
Let's be ambitious and test our updated meta-interpreter on a recursive program. We could ask our meta-interpreter to explain the proof that two lists are the same, prove(same([1,2,3],[1,2,3])).
Before we can do this, we need one small extension to our meta-interpreter because the definition of same/2 uses unification =/2 to test if the heads of two lists are the same. Our meta-interpreter needs to know how to handle unification.
The extension is simple. To execute a goal matched as A=B, we simply ask prolog to execute A=B.
% meta-interpreter for rules with multiple goals
prove(true) :- !.
prove(A=B) :- !, A=B.
prove((A,B)):- !, prove(A), prove(B).
prove(H) :- clause(H,B), prove(B),
write(H), write(" ← "), writeln(B).
The rule prove(A=B):-!,A=B might seem like an unnecessary tautology. If it didn't exist then our meta-interpreter would not know how to execute goals of the form A=B, even if prolog itself does.
Let's finally test our meta-interpreter.
?- prove(same([1,2,3],[1,2,3])).
same([],[]) ← true
same([3],[3]) ← 3=3,same([],[])
same([2, 3],[2, 3]) ← 2=2,same([3],[3])
same([1, 2, 3],[1, 2, 3]) ← 1=1,same([2, 3],[2, 3])
true
Our meta-interpreter has correctly executed the recursive program, and also explained why the lists [1,2,3] and [1,2,3] are the same.
Let's read the explanation:
[1,2,3]and[1,2,3]are the same because1=1, and[2,3]and[2,3]are the same.[2,3]and[2,3]are the same because2=2, and[3]and[3]are the same.[3]and[3]are the same because3=3, and[]and[]are the same.[]and[]are the same is a simple fact.
This is quite impressive for such a small meta-interpreter.
Key Points
- A sequence of goals can be grouped as one goal in round brackets, for example
(one(X),two(X),three(X)). - Just as
[H|T]matches the head and tail of a list,(A,B)matches the first and remaining goals in a grouped sequence. - This means
prove((A,B)):-!,prove(A),prove(B)can be used to recursively prove rule bodies with multiple goals. - A meta-interpreter can be extended to handle simple prolog built-ins with rules that mirror them, for example
prove(A=B):-!,A=B.