(sec:3.8)=
# Meta-programs #
Prolog represents a clause `Head:-Body` in the same way as a term `:-(Head,Body)`. Thus, it is easy to write programs that manipulate clauses. In the first case, '`:-`' is treated as a predicate, and in the second case it is treated as a functor. The combination of these two interpretations occurs frequently in Prolog programs, and can be applied to any predicate `p`. Such programs are called *meta-programs*; the interpretation of `p` as a predicate occurs on the *object-level*, and the interpretation as a functor occurs on the *meta-level*. (Note that the difference between meta-predicates and higher-order predicates is that meta-predicates take object-level *clauses* as arguments, while the latter take lower-order *predicates* as arguments.)
+++
For instance, suppose we have the following biological knowledge, expressed as propositional if-then rules:
```{swish} swish:3.8.1
```
Suppose we want to prove that Tweety is a bird. That is, we want to show that the rule
```Prolog
if tweety then is_bird.
```
follows logically from the given rules. This can be done by a meta-program, which manipulates the rules on the object-level:
```{swish} swish:3.8.2
---
inherit-id: swish:3.8.1
---
```
The three clauses for the `derive` predicate represent the three possible cases:
1. a goal matches the head of a rule, in which case we should proceed with the body;
1. a goal is a conjunction (for instance, because it was produced in the previous step), of which each conjunct is derived separately;
1. a goal is among the assumptions.
As explained above, `if` is a predicate on the object-level, and a functor on the meta-level.
```{exercise} ex:3.16
```
+++
Since propositional definite clauses are similar to the above if-then rules, one could view this program as a propositional Prolog simulator. In fact, it is possible to push the resemblance closer, by adopting the Prolog-representation of clauses at the object-level. One minor complication is that the clause constructor '`:-`' is not directly available as an object-level predicate. Instead, Prolog provides the built-in predicate `clause`: a query `?-clause(H,B)` succeeds if `H:-B` unifies with a clause in the internal Prolog database (if `H` unifies with a fact, `B` is unified with `true`). A further modification with respect to the above program is that Prolog queries do not have the form `if Assumptions then Goal`; instead, the `Assumptions` are added to the object-level program, from which a proof of `Goal` is attempted.
+++
Following these observations, the predicate `derive` is changed as follows:
```Prolog
prove(Goal):-
clause(Goal,Body),
prove(Body).
prove((Goal1,Goal2)):-
prove(Goal1),
prove(Goal2).
prove(true).
```
This program nicely reflects the process of constructing a resolution proof:
1. if the resolvent contains a single atom, find a clause with that atom in the head and proceed with its body;
1. if the resolvent contains various atoms, start with the first and proceed with the rest;
1. if the resolvent is empty, we're done.
Some Prolog interpreters have problems if `clause` is called with the first argument instantiated to `true` or a conjunction, because `true` and '`,`' (comma) are built-in predicates. To avoid these problems, we should add the conditions `not A=true` and `not A=(X,Y)` to the first clause. A less declarative solution is to reorder the clauses and use cuts:
```Prolog
prove(true):-!.
prove((A,B)):-!,
prove(A),
prove(B).
prove(A):-
/* not A=true, not A=(X,Y) */
clause(A,B),
prove(B).
```
We will adopt this less declarative version for pragmatic reasons: it is the one usually found in the literature. As this program illustrates, whenever you use cuts it is normally a good idea to add a declarative description of their effect between comment brackets.
+++
A meta-program interpreting programs in the same language in which it is written is called a *meta-interpreter*. In order to 'lift' this propositional meta-interpreter to clauses containing variables, it is necessary to incorporate unification into the third clause. Suppose we are equipped with predicates `unify` and `apply`, such that `unify(T1,T2,MGU,T)` is **true** if `T` is the result of unifying `T1` and `T2` with most general unifier `MGU`, and `apply(T,Sub,TS)` is **true** if `TS` is the term obtained from `T` by applying substitution `Sub`. The meta-interpreter would then look like this:
```Prolog
prove_var(true):-!.
prove_var((A,B)):-!,
prove(A),
prove(B).
prove_var(A):-
clause(Head,Body),
unify(A,Head,MGU,Result),
apply(Body,MGU,NewBody),
prove_var(NewBody).
```
Prolog's own unification predicate `=` does not return the most general unifier explicitly, but rather unifies the two original terms implicitly. Therefore, if we want to use the built-in unification algorithm in our meta-interpreter, we do not need the `apply` predicate, and we can write the third clause as
```Prolog
prove_var(A):-
clause(Head,Body),
A=Head,
prove_var(Body)
```
If we now change the explicit unification in the body of this clause to an implicit unification in the head, we actually obtain the propositional meta-interpreter again! That is, while this program is read **declaratively** as a meta-interpreter for propositional programs, it nevertheless operates **procedurally** as an interpreter of first-order clauses ({numref}`fig:3.14`).
Note that this meta-interpreter is able to handle only 'pure' Prolog programs, without system predicates like cut or `is`, since there are no explicit clauses for such predicates.
```{figure} /src/fig/part_i/image048.svg
---
name: 'fig:3.14'
width: 80%
---
The `prove` meta-interpreter embodies a declarative implementation of the resolution proof procedure, making use of built-in unification.
```
```{exercise} ex:3.17
```
+++
A variety of meta-interpreters will be encountered in this book. Each of them is a variation of the above 'canonical' meta-interpreter in one of the following senses:
1. application of a different search strategy;
1. application of a different proof procedure;
1. enlargement of the set of clauses that can be handled;
1. extraction of additional information from the proof process.
The first variation will be illustrated in {numref}`sec:5.3`, where the meta-interpreter adopts a breadth-first search strategy. In the same section, this meta-interpreter is changed to an interpreter for full clausal logic (3). Different proof procedures are extensively used in {numref}`Chapters %s` and {numref}`%s`. Here, we will give two example variations. In the first example, we change the meta-interpreter in order to handle general clauses by means of negation as failure (3). All we have to do is to add the following clause:
```Prolog
prove(not A):-
not prove(A)
```
This clause gives a declarative description of negation as failure.
+++
The second variation extracts additional information from the SLD proof procedure by means of a proof tree (4). To this end, we need to make a slight change to the meta-interpreter given above. The reason for this is that the second clause of the original meta-interpreter breaks up the current resolvent if it is a conjunction, whereas in a proof tree we want the complete resolvent to appear.
```Prolog
% meta-interpreter with complete resolvent
prove_r(true):-!.
prove_r((A,B)):-!,
clause(A,C),
conj_append(C,B,D),
prove_r(D).
prove_r(A):-
clause(A,B),
prove_r(B).
%%% conj_append/3: see Section 10.2 (appendix)
```
We now extend `prove_r/1` with a second argument, which returns the proof tree as a list of pairs `p(Resolvent,Clause)`:
```{swish} swish:3.8.2_2
---
source-text-end: 3.8.2_2-end
---
```
For instance, given the following clauses:
```Prolog
student_of(S,T):-teaches(T,C),follows(S,C).
teaches(peter,cs).
teaches(peter,ai).
follows(maria,cs).
follows(paul,ai).
```
and the query `?-prove_p(student_of(S,T))`, the program writes the following proof trees:
```Prolog
:-student_of(maria, peter)
.....|..........student_of(maria, peter):-teaches(peter, cs),follows(maria, cs)
.....|..................../
:-teaches(peter, cs),follows(maria, cs)
.....|..........teaches(peter, cs):-true
.....|..................../
:-follows(maria, cs)
.....|..........follows(maria, cs):-true
.....|..................../
...............[]
:-student_of(paul, peter)
.....|..........student_of(paul, peter):-teaches(peter, ai),follows(paul, ai)
.....|..................../
:-teaches(peter, ai),follows(paul, ai)
.....|..........teaches(peter, ai):-true
.....|..................../
:-follows(paul, ai)
.....|..........follows(paul, ai):-true
.....|..................../
...............[]
```
+++
Note that these are propositional proof trees, in the sense that all substitutions needed for the proof have already been applied. If we want to collect the uninstantiated program clauses in the proof tree then we should make a copy of each clause, before it is used in the proof:
```Prolog
prove_p((A,B),[p((A,B),Clause)|Proof]):-!,
clause(A,C),
copy_term((A:-C),Clause), % make copy of the clause
conj_append(C,B,D),
prove_p(D,Proof)
```
The predicate `copy_term/2` makes a copy of a term, with all variables replaced by new ones. It is a built-in predicate in many Prolog interpreters, but could be defined by means of `assert/2` and `retract/2` (see {numref}`Section %s (appendix)` for details).
````{tip}
We can use the [Graphviz rendering engine](https://swish.swi-prolog.org/example/render_graphviz.swinb) in SWISH to save having to lay out the proof trees ourselves. To this end we collect a list of edges of the from `Query -> New Query` and `Clause -> NewQuery`, and return a term of the form `digraph([Options|Edges])`, where `digraph` indicates a directed graph.
```{swish} swish:prooftree
```
This program includes the `copy_term/2` calls referred to above, and also calls `numbervars/1` before rendering the tree to display symbolic variable names `A`, `B`, `C` etc. Notice that, by the nature of the meta-interpreter, all substitutions found in the proof are applied retrospectively to all intermediate queries, and hence displayed in the proof tree.
````