Friday 3 March 2023

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.

at