20 - Meta-Interpreter 5: Fixed Depth Search

In this final example, we'll see how a meta-interpreter can change the way solutions are found for queries. This can be useful for some particularly challenging problem scenarios. 

Prolog's own search strategy is depth-first. It will try to resolve a goal, following all deductions, until it succeeds or fails. A weakness of this strategy is that it can get trapped in an endless search loop, causing it to miss solutions to be found along different search paths.

Here we'll implement a fixed-depth strategy which can help in scenarios where there are such endless search traps. 

% Example 20 - Meta-Interpreter With Fixed Depth Search

% maze locations and links
link(a,b). link(b,c). link(a,d).
link(d,e). link(e,f). link(d,g).
link(f,c). link(f,i).

% two rooms are connected if linked
connected(X,Y) :- link(X,Y).
connected(X,Y) :- link(Y,X).

% journey between two locations
journey(X, Y, [(X,Y)]) :- connected(X,Y).
journey(X, Y, J) :- [(X,A)|J1]=J, connected(X,A), journey(A,Y, J1).

% meta-interpreter with fixed depth search
prove(true, _) :- !.
prove(A=B, _) :- !, A=B.
prove((A,B), Depth):- !, prove(A, Depth), prove(B, Depth).
prove(H, Depth) :-
    Depth > 0,
    NextDepth is Depth-1,
    clause(H,B), prove(B, NextDepth).

The example program defines a maze, illustrated below. There are nine rooms, labelled a to i, with links between some of them, but not all of them.

A link between two adjacent rooms is encoded by a property link/2. For example, link(a,b) states that we can walk from a to b in one step. There is no link between rooms e and h, and so there is no link(e,h) listed in the program. 

Our challenge is to find journeys between any two distinct locations.

Journeys

Let's define a property journey(X,Y,J) where X is the starting location, Y is the target location, and J is a list of steps to get from X to Y.

The definition is naturally recursive:

• In the simplest case, there is a journey from X to Y if they are directly connected, and the journey is a list of just one step [(X,Y)].
• There is a journey from X to Y if they are indirectly connected, that is, if X and A are directly connected, and there is a journey from that A to Y. The journey list of steps from X to Y has (X,A) as its head.

We have to define a direct connection. Two rooms, X and Y, are directly connected no matter the direction of the link between them. That is, link(X,Y) is a fact, or link(Y,X) is a fact.

It is worth clarifying that J is a list of elements, each of which is a grouping of two adjacent rooms, for example (a,b). So J = [(a,b), (b,c), (c,f)] is a journey from a to f, taken in three steps, a → b, then b → c, and finally c → f.

The following definitions for connected/2 and journey/2 implement these ideas.

% two rooms are connected if linked
connected(X,Y) :- link(X,Y).
connected(X,Y) :- link(Y,X).

% journey between two locations
journey(X, Y, [(X,Y)]) :- connected(X,Y).
journey(X, Y, J) :- [(X,A)|J1]=J, connected(X,A), journey(A,Y, J1).

Basic Queries

Let's run some simple queries to check the basics are working.

?- connected(a,b).
true
false

?- connected(c,b).
true

connected(a,c).
false

Looking back at the maze illustration, we can see prolog has responded correctly to confirm that a and b are directly connected, as are c and b, but not a and c. 

The first query connected(a,b) returns true, backtracks and then returns false. We could avoid this inefficient backtracking with a green cut in the definition of connected/2, but we'll tolerate it because we want to keep our meta-interpreter simple by not implementing the cut. 

Journey Queries

The journey from a to b is one of the simplest, taking only one step. The query journey(a,b,[(a,b)]) is asking if there is a journey from a to b consisting of one step (a,b).

?- journey(a,b,[(a,b)]).

true
false

Prolog confirms the journey from a to b does indeed consist of one step (a,b).

Let's now ask “which journeys are possible from a to b?”

?- journey(a,b,J).

J = [(a,b)]
J = [(a,b), (b,c), (c,b)]
J = [(a,b), (b,c), (c,b), (b,c), (c,b)]
J = [(a,b), (b,c), (c,b), (b,c), (c,b), (b,c), (c,b)]
J = [(a,b), (b,c), (c,b), (b,c), (c,b), (b,c), (c,b), (b,c), (c,b)]
...

Prolog finds more than one journey is possible between a and b. In fact, we have to abort the query as the solutions appear to be endless. 

Let's look more closely at the first few.

• The very first solution has a single step a → b, clearly the most efficient journey.
• The second solution moves a → b, then steps away b → c, and finally steps back c → b. Not as efficient.
• The third solution is even less efficient, a → b, b → c, c → b, b → c, and c → b.

We can see all of the further solutions simply add redundant steps b → c, c → b to the journey. 

Prolog's search has fallen into a trap. The endless options for journeys which merely add the redundant steps b → c, c → b will prevent prolog from trying other journeys, such as those which start a → d.

A More Interesting Journey

Let's increase the challenge and ask about journeys from a to e. Looking back at the maze we can see there are two direct paths, clockwise a → b, b → c, c → f, f → e, and anti-clockwise a → d, d → e. 

Let's see how our prolog program copes.

?- journey(a,e,J).

Stack limit (0.2Gb) exceeded
  Stack sizes: local: 0.2Gb, global: 34.9Mb, trail: 11.6Mb
  Stack depth: 762,019, last-call: 0%, Choice points: 762,000
  Possible non-terminating recursion:
    [762,017] journey(b, e, [length:1])
    [762,016] journey(c, e, [length:2])
...

It seems this search is too challenging. Prolog has aborted the search after running out of memory.

We know journeys from a to e are possible, and we can ask prolog to confirm two specific journeys.

?- journey(a,e,[(a,b),(b,c),(c,f),(f,e)]).
true
false

?- journey(a,e,[(a,d),(d,e)]).
true
false

Let's see how a meta-interpreter can help.

Fixed Depth Search

How would we, with human brains, respond to being presented with long journeys like J=[(a,b), (b,c), (c,b), (b,c), (c,b), (b,c), (c,b)]? Our intuition would be to discard long journeys as good solutions because looking at the maze illustration suggests, visually, that shorter journeys should be sufficient.

Prolog's solution search strategy doesn't favour shorter solutions. However, with a meta-interpreter, we can gain control over the search strategy and change it. Changing it to only follow deductive paths up to a maximum given depth is fairly easy.

The following is an updated fixed-depth meta-interpreter prove/2.

% meta-interpreter with fixed depth search

prove(true, _) :- !.
prove(A=B, _) :- !, A=B.
prove((A,B), Depth):- !, prove(A, Depth), prove(B, Depth).
prove(H, Depth) :-
    write("Depth = "), writeln(Depth),
    Depth > 0,
    NextDepth is Depth-1,
    clause(H,B),
    write(H), write(" ← "), writeln(B),
    prove(B, NextDepth).

The first thing to notice is that the arity of prove has changed from 1 to 2. The first parameter remains the goal to be proved. The second parameter is the maximum permitted search depth. For example, prove(G, 5) asks prolog to prove the goal G with no more than 5 deductive resolution steps.

The core of the meta-interpreter remains the same as before. The rules to match true and A=B are the same, except for the additional depth parameter. Here the underscore is used for the depth, because the depth isn't used in the rule bodies.

The rule to pick off the first goal from a sequence (A,B) is also the same as before, and the additional depth parameter is simply passed onto the recursive calls to prove A and B.

The final rule prove(H,Depth) is where the maximum depth is enforced. The first condition Depth>0 ensures that the maximum depth has not been reduced to zero. A new variable NextDepth is assigned the arithmetic evaluation of Depth-1, and if the goal H does have a body B, that body is proved using prove(B, NextDepth), that is, with a maximum depth reduced by one. 

This meta-interpreter prints out the current depth as well as the current goal and body. This is to help us see what it is doing when we run simple tests. We'll remove this printing when we use it for more complex queries.

For proofs that require longer chains of deduction, the value of NextDepth will reach zero, and the subsequent call to prove(B, 0) will fail because the condition Depth>0 will be enforced. This is how the meta-interpreter fails proofs that require longer chains of deduction.

Testing Fixed-Depth

Let's test our fixed-depth meta-interpreter works as intended.

We know that to prove connected(a,b) requires two deductive steps. First, connected(a,b) is resolved to link(a,b), and second, link(a,b) is resolved to true.

?- prove(connected(a,b),2).

Depth = 2
connected(a,b) ← link(a,b)
Depth = 1
link(a,b) ← true
true

connected(a,b) ← link(b,a)
Depth = 1
false

We can see the meta-interpreter starting with a maximum depth of 2, and reducing it to 1 for the final goal. We can also see the redundant backtracking and retrying of connected(X,Y).

Let's now try the same query but start with a maximum depth of 1.

?- prove(connected(a,b),1).

Depth = 1
connected(a,b) ← link(a,b)
Depth = 0

connected(a,b) ← link(b,a)
Depth = 0
false

The meta-interpreter failed to prove connected(a,b) within 1 deductive step. The printed messages show how the search was stopped before link(a,b) or link(b,a) could be resolved.

Our fixed-depth meta-interpreter seems to work.

Fixed-Depth Journey Search

Let's return to our problematic query journey(a,e,J) and try again with a fixed-depth search.

?- prove(journey(a,e,J), 3).
false

?- prove(journey(a,e,J), 4).
J = [(a,d), (d,e)]
false

We can see that allowing a search depth of 3 is insufficient to find any solutions. However, allowing a depth of 4 does return one solution, a → d, d → e, and it is the shortest journey from a to e. 

Success! Our achievement is using a modified search strategy to find solutions where the default prolog strategy fails.

Let's extend the maximum depth.

?- prove(journey(a,e,J), 6).

J = [(a,b), (b,c), (c,f), (f,e)]
J = [(a,b), (b,a), (a,d), (d,e)]
J = [(a,d), (d,e)]
J = [(a,d), (d,e), (e,f), (f,e)]
J = [(a,d), (d,e), (e,d), (d,e)]
J = [(a,d), (d,g), (g,d), (d,e)]
J = [(a,d), (d,a), (a,d), (d,e)]

Our meta-interpreter has found seven solutions, including the shortest clockwise and anti-clockwise journeys.

Key Points

• A weakness of prolog's depth-first strategy for solutions is that it can get trapped in endless search loops.
• A meta-interpreter can enforce a maximum search depth. This avoids getting trapped in endless search loops, but will miss solutions that do require a deeper search.
• Iterative deepening is the technique of starting with a small maximum search depth, then progressively increasing it to reveal further solutions.

19 - Meta-Interpreter 4: The Cut

We've seen how to extend our meta-interpreter to interpret built-ins like is/2. The technique is the same for other simple built-ins like is/2 and >/2.

The cut, however, is one built-in that isn't as easy to simulate. 

In this example we'll see how it can be approximated fairly well using the mechanism of throwing and catching exceptions.

% Example 19 - Meta-Interpreter For The Cut

fruit(apple).
fruit(orange) :- !.
fruit(banana).

% meta-interpreter that handles the cut
prove(true) :- !.
prove(!) :- !, ( true ; throw(cut_exception) ).
prove((A,B)):- !, prove(A), prove(B).
prove(H) :- 
    catch((clause(H,B), prove(B)), cut_exception, fail),
    write(H), write(" ← "), writeln(B).

Our example uses the same program we used to introduce the cut.

Incorrectly Interpreting The Cut

Let's look again at how we implemented unification =/2 in our meta-interpreter.

prove(A=B) :- !, A=B.

When the meta-interpreter finds a goal of the form A=B, this rule executes A=B, thus achieving the effect of attempting to unify A=B, which can either succeed or fail. The cut here prevents the more general prove(H) being matched if this rule prove(A=B) has matched.

Let's look at an example of implementing another built-in, the arithmetic assignment is/2.

prove(A is B) :- !, A is B.

Again, this rule will match goals of the form A is B, and execute A is B, which has the desired effect of attempting to assign the arithmetic evaluation of B to A.

Now let's examine a naive attempt at simulating the cut, following the same pattern. 

prove(!) :- !, !.

Imagine our meta-interpreter is interpreting a rule H which has a cut as one of its goals. The meta-interpreter rule prove(!) will match that goal. This rule will succeed because cuts always succeed. This achieves the first effect of a cut. The second effect of a cut is to prevent backtracking. This doesn't work as we'd like because the cuts in prove(!):-!,! only prevent backtracking in the rule prove(!), and not in the rule H.

This is the reason we need a different approach to implementing the cut. We need a way to send a message from prove(!) back to the meta-interpreting of the parent rule H.

Throwing & Catching Exceptions

Like many languages, prolog supports the throwing and catching of exceptions. 

If you're not familiar with this idea, think about prolog stopping when a problem occurs, for example running out of memory due to an endless search. When prolog runs out of memory it throws an exception related to the problem. That exception can be thought of as a special signal, sent with a higher priority than the program itself, which causes the program to be paused. Such signals, or exceptions, are intended to be caught, and handled appropriately. By default, an out of memory exception is caught by prolog itself, handled by printing out an error message and aborting the program.

Let's look at an example. The following defines bad(X), intentionally designed to cause an endless search that runs out of memory.

% bad/1 will cause a resource error
bad(X) :- bad(bad(X)).

If we issue a query bad(X), after a short while, the program will crash and an error message will be printed out.

?- bad(X).

Stack limit (0.2Gb) exceeded
Stack sizes: local: 2Kb, global: 0.2Gb, trail: 0Kb
Stack depth: 13,390,437, last-call: 100%, Choice points: 12
...

What we see is prolog's exception handler for this resource error printing out an explanation of what went wrong.

We can catch and handle exceptions by declaring an interest in a specific one, or asking to catch all exceptions. To do this we use catch(Goal, Exception, Handler), where Goal is the goal from which we expect an exception, Exception is the type of exception, and Handler is another goal which will run in response to an exception being caught.

The following asks prolog to catch any exception raised from the goal bad(X), and write out a representation of that exception. Because E is a variable, it will match any exception.

?- catch(bad(X), E, write(E)).

error(resource_error(stack),
stack_overflow{choicepoints:13,
depth:13390419, environments:19,
globalused:209227, localused:3,
stack:
...

Let's have a look at throwing our own custom exception.

% numerology(X) throws an exception if X=13
numerology(X):- \+ X=13.
numerology(X):- X=13, throw(unlucky).

% testnumber handles that exception
testnumber(X) :- catch(numerology(X), unlucky, writeln("unlucky number")).

The property numerology(X) succeeds if X cannot be unified with 13. If however X=13, then it throws a custom exception, which we've named unlucky. 

The property testnumber(X) uses catch/3 to call numerology(X), watch for exceptions of the type unlucky, and handle them by printing “unlucky number”. Let's test it with 12 and 13.

?- testnumber(12).
true

?- testnumber(13).
unlucky number
true

We can see an exception was raised and caught in the case X=13. Notice how the prolog program did not abort after the exception was handled. It continued until it completed, reporting true. Exceptions don't abort a program unless the handler explicitly tells prolog to.

Meta-Interpreting The Cut

Having seen how to throw, catch and handle custom exceptions, we can now explore how to meta-interpret the cut.

The following is a new definition for prove(!). 

prove(!) :- true.
prove(!) := !, throw(cut_exception).

When the meta-interpreter finds a cut, it wants to execute prove(!). The first rule matches and succeeds with a true. Although it may appear redundant, this success is what allows solutions in the interpreted cut's parent clause to be confirmed. 

The second rule also matches and throws a custom exception, which we've called cut_exception. The lack of a cut in the body of the first rule allows this second one to execute.

The following uses prolog's semicolon ; to write the two rules as one. The semicolon means disjunction “or”, just like the comma means conjunction “and”.

prove(!) := !, (true; throw(cut_exception)).

We've already talked about why the handling of this exception needs to relate back to the entire rule in whose body the cut was found. Let's see how this is achieved.

prove(H) :- 
    catch((clause(H,B), prove(B)), cut_exception, fail),
    write(H), write(" ← "), writeln(B).

The catch/3 here asks to register an interest in the cut_exception from the grouped goals (clause(H,B),prove(B)), not just prove(B), even though the exception can only come from prove(B). We'll see why soon. The handling of the exception is simply to fail. 

Let's walk through how this works, step by step.

• If the rule for H has a cut ! in its body B, then it will eventually be matched by prove(!). 
• prove(!) will succeed with a true and confirm any solutions found up to that point.
• On backtracking prove(!) will also throw a custom exception given the name cut_exception.
• The cut_exception will be caught in the context of calling the grouped goals (clause(H,B),prove(B)). 
• The handling of this cut_exception is simply to fail. That means the full (clause(H,B),prove(B)) is failed.

At this point, any goals in the body B before the cut have already been meta-interpreted and executed, with any solutions found remaining valid. This mirrors how the cut works in prolog itself.

When the cut is reached, the entire (clause(H,B),prove(B) is failed. Because clause(H,B) is failed, no further attempts are made to find additional rules which also have a head H. The effect of this is to prevent further backtracking for the rule H. This also mirrors how the cut works in prolog.

Phew! This is probably the most complicated prolog we'll encounter on this particular journey, so feel free to work through it several times.

Testing

Let's remind ourselves of the expected behaviour of the program we want to meta-interpret.

?- fruit(X).

X = apple
X = orange

The solution X=banana is excluded by the cut in fruit(orange):-!.

Let's test our enhanced meta-interpreter.

?- prove(fruit(X)).

fruit(apple) ← true
X = apple

fruit(orange) ← !
X = orange

Success! Our meta-interpreter has correctly simulated the cut. The printed explanations also give a visual clue as to why no more solutions were found after X=orange.

Limitations

This approach to meta-interpreting the cut is relatively simple, given the non-trivial effect the cut actually has on the execution of prolog. This simplicity brings with it some limitations. 

First, this approach is computationally heavy, because throwing and handling exceptions is expensive. Exceptions are meant to be thrown, well, by exception, and not used in the normal execution of programs. 

Second, in the unlikely case the program to be meta-interpreted throws an exception of the type cut_exception, this approach will collapse. 

Key Points

• Because the cut effects the execution of its parent clause, it cannot be meta-interpreted in the same way as simple built-ins like =/2.
• The cut's behaviour can be approximated by throwing an exception when the cut is meta-interpreted, with the handler scoped to fail the group (clause(H,B), prove(B)). This results in no further searches for rules that match the parent goal H. 
• This method has limitations. Throwing and catching exceptions is computationally expensive. The method will also fail if the program to be interpreted throws exceptions of the same type.

18 - Meta-Interpreter 3: Recursion

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 because 1=1, and [2,3] and [2,3] are the same.
• [2,3] and [2,3] are the same because 2=2, and [3] and [3] are the same.
• [3] and [3] are the same because 3=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.

17 - Meta-Interpreter 2: Deduction

The meta-interpreter we just developed only works with prolog programs consisting of simple facts. Here we'll extend it to work with deductive programs, where a goal is proved by reasoning using relations between properties. 

% Example 17 - Meta-Interpreter for Deduction

% facts
mammal(dog).
mammal(cat).

% relations
animal(X) :- mammal(X).
lifeform(X) :- animal(X).

% meta-interpreter that covers deduction
prove(true) :- !.
prove(H) :- clause(H,B), prove(B),
   write(H), write(" ← "), writeln(B).

This program extends the previous one's two facts with two relations. First, if something is a mammal, then it is also an animal. Second, if something is an animal, then it is also a life form. 

Thought Experiment: Proof By Deduction

Let's work out how we might prove the query animal(dog), if we were the meta-interpreter again. We know from our earlier work that this requires deduction, not just simply looking up facts. 

• As always, we start by trying to match the query animal(dog) with the head of any rule, whether it is a fact or a relation. 
• We can use clause/2 to do this search of prolog's database. If successful, it will give us the body of the matching rule.
• The database contains animal(X):-mammal(X), so clause/2 will give us the body of this relation. Because our query was animal(dog), and not animal(X), the body will be grounded as mammal(dog).
• We now need to prove the body mammal(dog) as a new goal. 

We started with the query goal animal(dog), and have arrived at a new goal mammal(dog). To prove it, we apply our process again.

• We try to match the query mammal(dog) with the head of any rule in prolog's database.
• We again use clause/2 to do this search. If successful, it gives us the body of the rule.
• The database contains mammal(dog) as a simple fact, so the body simply contains true. 
• To conclude the proof, we test that the body is indeed true. 

We can see the proof process is repeated if a goal's body is another property. Planning ahead, it is very possible that there could be an entire chain of properties that must be resolved to complete a proof, and so a recursive meta-interpreter seems a good idea.

Meta-Interpreter For Deduction

Let's incorporate the process we just developed into our meta-interpreter.

% meta-interpreter that covers deduction

prove(true) :- !.
prove(H) :- clause(H,B), prove(B),
   write(H), write(" ← "), writeln(B).

Our meta-interpreter is now recursive, so has a termination rule and a continuation rule for prove/1. 

Let's start with the continuation rule. As before, it takes a query goal H, and tries to find a rule whose head unifies with it, leaving B unified with its body. Previously, when we were only considering a database of facts, the body could only ever be true. Now the body could be another property. 

What do we do with this property B? We prove it using the same method. That is, prove(B). This makes prove/1 recursive. 

Let's apply our earlier thinking about recursive algorithms to this continuation rule. Does it reduce the size of the problem by one unit? It does, because prove(B) has reduced the bigger problem prove(H) by one level of deduction.

Our continuation rule will be called again and again, as long as proving a property leads to another property. The search ends when a fact is reached. That is, a body that is simply true. This is our termination rule, prove(true). As usual, we place our termination rule above the continuation rule because we want it to match first.

The termination rule has a cut prove(true):-!. Let's see why. When a proof is almost complete, B is true, so the goal is prove(true). This unifies with the termination rule. It also unifies with the continuation rule because it has a more generic head prove(H). To prevent this, the termination rule has a simple cut.

Double Deduction

Let's test our updated meta-interpreter with the query animal(dog), which we know requires only one deduction.

?- prove(animal(dog)).

mammal(dog) ← true
animal(dog) ← mammal(dog)
true

Our meta-interpreter has correctly proved that animal(dog) is true. We didn't really need a meta-interpreter to do that. What the meta-interpreter has done for us is print an explanation of the proof. Reading it tells us that a dog is an animal because a dog is a mammal, and that a dog is a mammal is a basic fact.

Let's try the query lifeform(dog), which we know will require two deductive steps.

?- prove(lifeform(dog)).

mammal(dog) ← true
animal(dog) ← mammal(dog)
lifeform(dog) ← animal(dog)
true

We can see the additional deductive step in the proof explanation.

This ability to explain deductive proofs is powerful, and quite impressive for a 2-line meta-interpreter.

Queries With Variables

Let's see how our meta-interpreter copes with queries which contain variables. The query animal(X) asks “which X are animals?”

?- prove(animal(X)).

mammal(dog) ← true
animal(dog) ← mammal(dog)
X = dog

mammal(cat) ← true
animal(cat) ← mammal(cat)
X = cat

Our meta-interpreter correctly finds that both cats and dogs are animals, and provides explanations for each solution. 

Try tracing this query yourself to see how our meta-interpreter works with proofs that require backtracking. See if you can spot the retrying of clause(mammal(X),B) because it matches both mammal(dog) and mammal(cat).

Key Points

• For proofs that require multiple steps of deduction, a recursive meta-interpreter is a natural fit.
• Since deductive proofs end in basic facts, testing the truth of a basic fact becomes the termination rule.
• Deductive proofs link one property to another. This corresponds to the continuation rule which links proving a rule head to proving its body, thus reducing the size of the proof by one level.

16 - Meta-Interpreter 1: Facts

Meta-programming is using prolog itself to run prolog code. The aim is to gain additional control over how that code is run. 

In these final chapters we'll gradually build a small meta-interpreter, with a focus not on completeness, but on demonstrating key concepts.

% Example 16 - Minimal Meta-Interpreter For Facts

% facts
mammal(dog).
mammal(cat).

% simplest meta-interpreter
prove(H) :- clause(H,B), B=true,
    write(H), write(" ← "), writeln(B).

When we discussed negation/1 we saw how a variable G could be unified with a property, and the prolog code for that property could be executed with call(G). That was our first experience of meta-programming, using prolog to run prolog. 

Here we'll start to develop a simple meta-interpreter, a program that runs simple prolog programs, not just a single property. By simple, we mean a small, but still useful, subset of prolog. Our experience with other languages might suggest this is a rather ambitious and complicated thing to do. We'll see how prolog makes this surprisingly easy. 

Finding Rules With clause/2

At the very beginning of this journey we created and queried simple facts. It makes sense that a meta-interpreter would need to query the existence of facts and rules. We can see the “meta” in this transition from querying prolog facts, to querying the existence of prolog facts.

Prolog provides a built-in property clause(H,B) which succeeds if a prolog rule with head H exists. If it does exist, then B is left unified with the body of that rule. If the rule is a simple fact, with an empty body, then B is left as true.

The example program establishes two very simple facts, that cats and dogs are mammals. Let's see how clause/2 works querying these facts.

?- clause(mammal(dog), B).

B = true

Prolog has found a rule in the database whose head is mammal(dog). The rule is a simple fact, and so the body is returned as B=true. 

Let's try using clause/2 to find a rule we know doesn't exist.

?- clause(mammal(fish), B).

Because there is no rule with head mammal(fish), clause/2 fails. 

Thought Experiment: Proving Facts

Before we write any code, let's work out how we, if we were the meta-interpreter, might prove the query mammal(dog). 

• First we would have to find a rule with a head that matches the query mammal(dog). 
• We could use clause/2 to do this search. If successful, it would give us the body of the matching rule.
• The database contains mammal(dog) as a simple fact, so the body simply contains true.
• To conclude the proof, we test that the body is indeed true. 

This exercise helps us avoid skipping steps which are easily taken for granted.

Simplest Meta-Interpreter

Let's write in code what we've just described.

% simplest meta-interpreter

prove(H) :- clause(H,B), B=true.

This single line of code defines prove(H) as using clause(H,B) to find a rule whose head matches the query. If it finds one, B is unified with the body of that rule. 

For now, we're only considering a database of simple facts, so B can only ever be true. The last part of prove(H) simply tests whether B is true. 

Strictly speaking, we don't need to test B=true, because if there isn't a fact that matches H, clause(H,B) will fail, and so prove(H) will also fail. We'll keep it for clarity, and to remind us not to forget about proving simple facts when we further develop our meta-interpreter.

Let's test this meta-interpreter.

?- prove(mammal(dog)).
true

?- prove(mammal(cat)).
true

?- prove(mammal(fish)).
false

It's reassuring that proving mammal(fish) fails.

We should pause for a moment and appreciate what we've achieved. That single line of code prove(H):-clause(H,B),B=true really is a valid, albeit minimal, meta-interpreter. 

Verbose Meta-Interpreter

The important point about meta-interpreters, even the minimal one above, is that they give us control over how a query is proved.

For example, we can change the meta-interpreter to print the head and body of any goal it succeeded in proving.

% simplest meta-interpreter

prove(H) :- clause(H,B), B=true,
    write(H), write(" ← "), writeln(B).

Prolog provides write/1 and writeln/1 for printing, without and with a linefeed. We can see how longer lines of code can be broken over multiple lines, with an indent to aid readability.

Let's run the same queries again.

?- prove(mammal(dog)).
mammal(dog) ← true
true

?- prove(mammal(cat)).
mammal(cat) ← true
true

?- prove(mammal(fish)).
false

Our meta-interpreter is printing an explanation of how a query is proved to be true. The last query mammal(fish) can't be proved, so there is no explanation printed.

Again, it is worth pausing to appreciate how easy it is to extend the process by which prolog proves a query.

Key Points

• Meta-programming is using prolog to run prolog code, for the purpose of gaining additional control over how that code is run.
• clause(H,B) is used to search prolog's database for rules whose head matches H, leaving B unified with the body. If no rule matches, clause/2 fails. Simple facts are rules with an empty body, and leave B=true.
• A meta-interpreter can augment prolog by printing explanations for its proofs. This is easily done by printing the head and body of any goal it succeeds in proving.

15 - Negation

Up to this point we've only seen prolog used to define properties that are true. We've not yet seen how prolog expresses a property is not true.

We'll start with a simple example that builds on familiar ground.

% Example 15 - Negation By Failure

% fruit
fruit(apple). 
fruit(orange). 
fruit(banana).

% colour
yellow(banana).

% Mary likes all fruit 
likes(mary, X) :- fruit(X).

% James likes all fruit, as long as it is yellow
likes(james, X) :- fruit(X), yellow(X).

% Sally likes all fruit, except yellow fruit
likes(sally, X) :- fruit(X), negation(yellow(X)).

% negation as failure
negation(G) :- call(G), !, fail. 
negation(_).

Our program first defines three simple facts about apples, oranges and banana being fruit. It also defines a banana as being yellow.

Mary Likes All Fruit

The next part of the program defines which fruit Mary, James and Sally like. 

Mary likes all fruit. This is easily expressed in prolog.

% Mary likes all fruit
likes(mary, X) :- fruit(X).

Let's test it to leave no doubt.

?- likes(mary,X).

X = apple
X = orange
X = banana

As expected, prolog finds Mary likes apples, oranges and bananas.

James Likes Only Yellow Fruit

James is more particular in his taste, and likes all fruit as long as it is yellow. Again, this is easy to express in prolog.

% James likes all fruit, as long as it is yellow
likes(james, X) :- fruit(X), yellow(X).

The first part of the rule fruit(X) is satisfied by all fruit, the second part yellow(X) imposes the constraint that it must be yellow.

?- likes(james,X).

X = banana

Prolog finds that only bananas satisfy James' requirements.

Sally Likes All Fruit, Except Yellow Fruit

Sally has a broader taste than James, and likes all fruit, except yellow fruit. Expressing the idea of “except” in prolog is not something we've seen before. 

• We're familiar with creating general rules, for example likes(mary,X). 
• We know how to add positive constraints, for example likes(james,X) has the positive requirement that fruit is yellow. 
• We haven't yet seen how to add negative constraints, exceptions. 

These three scenarios are illustrated as follows.

We need a way to say “and not this property” in prolog. For now, let's imagine we have a property negation/1 that does this. So negation(yellow(X)) is true when the property yellow(X) is not true. 

% Sally likes all fruit, except yellow fruit
likes(sally, X) :- fruit(X), negation(yellow(X)).

The first part of the rule fruit(X) is satisfied by all fruit, but this time the second part negation(yellow(X)) is only satisfied if yellow(X) is not true. 

?- likes(sally,X).

X = apple
X = orange

Prolog correctly finds that Sally likes apples and oranges, but not bananas. 

Negation/1

Let's see how negation/1 works. 

% negation as failure
negation(G) :- call(G), !, fail. 
negation(_).

The property negation/1 has two rules. 

The first part of the first rule is call(G). The call/1 is a built-in prolog property which executes whatever property G represents. This is a new use for variables. Previously variables could represent things like apple, or lists like [1, 2, 3]. Here, the variable G is intended to unify with a prolog property.

It is worth pausing to really appreciate this. The ability of a variable to represent prolog code, code that can be executed, is quite powerful. It opens up new ways of programming called meta-programming that we'll explore later.

If the property G is satisfiable, then the next part of the rule is a cut, which always succeeds, but prevents backtracking across it. The last part of the rule is fail, which causes the entire rule to fail. The cut prevents prolog from backtracking to find another way to make the rule succeed. So, if G is satisfiable, then negation(G) fails.

The second rule is only executed if call(G) from the first rule fails. The rule has no body which means it is always true. That is, if G is not satisfiable, negation(G) is true. The second rule has an underscore _ in its head because some prologs don't like a variable in the head of a rule not being used in its body.

We can see how negation(G) acts like a logical inversion.

• If G is true, negation(G) is false.
• If G is false, negation(G) is true.

So negation(yellow(X)) is only true if yellow(X) is not satisfiable. This is what we wanted for our likes(sally,X) rule.

This form of negation is called negation as failure. It works by intentionally failing after a goal is shown to be true, and succeeding otherwise.

Negation As Failure Is Not Logical Negation

Negation as failure is useful, but it is not equivalent to logical negation. Let's see why.

The order of goals in a purely logical rule should not matter. The following query unifies X=fish and then tests negation(fruit(X)).

?- X=fish, negation(fruit(X)).

X = fish

Clearly fish is not a fruit, because it is not listed in the database of facts, and so fruit(X) fails. This leads to negation(fruit(X)) succeeding. Prolog reports the query succeeds with X=fish as a valid solution. 

Now let's swap the goal order.

?- negation(fruit(X)), X=fish.

false

This time, the variable X does not have a value when fruit(X) is called. Because there are valid solutions to fruit(X), it succeeds, which means negation(fruit(X)) is false. This leads to the entire query failing. Remember, the second goal X=fish is not reached if the first goal fails. So prolog reports false. A purely logical reading of this result would incorrectly suggest fish is indeed a fruit. 

The apparently contradictory responses from prolog demonstrate that negation/1 is not a purely logical property. A safe way to use failure by negation is to ensure the property being tested is fully grounded, that is, all variables have values.

\+ Not Satisfiable

Despite the caution, negation as failure is useful, and most prologs include it as standard. In swi-prolog it is provided as \+, which is read as “the following goal is not satisfiable”. Some prologs retain a not/1 property, but \+ is encouraged to emphasise that it is not logical negation.

The following shows how \+ can simplify our likes(sally,X) rule.

likes(sally, X) :- fruit(X), \+ yellow(X).

The body of the rule is read as “fruit(X) is satisfied, but yellow(X) is not satisfiable”. 

Key Points

• Negation as failure is a test that intentionally fails when a property is satisfiable, and succeeds otherwise. 
• Negation as failure is not logical negation, and should be used with care. 
• Negation as failure can be used safely if all variables in the property being tested are grounded.
• Prolog provides \+ for negation, and is read as “the following property is not satisfiable”. For example, \+ yellow(X) means “yellow(X) is not satisfiable”.
• Prolog variables can be unified with a prolog property, and call/1 can be used to execute its code.