Wednesday 8 March 2023

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.

at