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:
% if A and B then C means if(then(and(A,B),C))
:-op(900,fx,if).
:-op(800,xfx,then).
:-op(700,yfx,and).
% object-level rules
if has_feathers and lays_eggs then is_bird.
if has_gills and lays_eggs then is_fish.
if tweety then has_feathers.
if tweety then lays_eggs.
Suppose we want to prove that Tweety is a bird. That is, we want to show that the rule
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:
% meta-program
derive(if Assumptions then Goal):-
if Body then Goal,
derive(if Assumptions then Body).
derive(if Assumptions then Goal1 and Goal2):-
derive(if Assumptions then Goal1),
derive(if Assumptions then Goal2).
derive(if Assumptions then Goal):-
assumed(Goal,Assumptions).
assumed(A,A).
assumed(A,A and _As).
assumed(A,_B and As):- assumed(A,As).
The three clauses for the derive predicate represent the three possible cases:
a goal matches the head of a rule, in which case we should proceed with the body;
a goal is a conjunction (for instance, because it was produced in the previous step), of which each conjunct is derived separately;
a goal is among the assumptions.
As explained above, if is a predicate on the object-level, and a functor on the meta-level.
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:
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:
if the resolvent contains a single atom, find a clause with that atom in the head and proceed with its body;
if the resolvent contains various atoms, start with the first and proceed with the rest;
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:
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:
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
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 (Figure 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 3.14 The prove meta-interpreter embodies a declarative implementation of the resolution proof procedure, making use of built-in unification.#
Exercise 3.17 #
Draw the SLD-tree for the query ?-prove(is_bird(X)), given the following clauses:
is_bird(X):-has_feathers(X),lays_eggs(X).
is_fish(X):-has_gills(X),lays_eggs(X).
has_feathers(tweety).
lays_eggs(tweety).
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:
application of a different search strategy;
application of a different proof procedure;
enlargement of the set of clauses that can be handled;
extraction of additional information from the proof process.
The first variation will be illustrated in Section 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 Chapters 8 and 9. 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:
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.
% 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):
% display a proof tree
prove_p(A):-
prove_p(A,P),
write_proof(P).
% prove_p(A,P) <- P is proof tree of A
prove_p(true,[]):-!.
prove_p((A,B),[p((A,B),(A:-C))|Proof]):-!,
clause(A,C),
conj_append(C,B,D),
prove_p(D,Proof).
prove_p(A,[p(A,(A:-B))|Proof]):-
clause(A,B),
prove_p(B,Proof).
write_proof([]):-
write('...............[]'),nl.
write_proof([p(A,B)|Proof]):-
write((:-A)),nl,
write('.....|'),write('..........'),write(B),nl,
write('.....|'),write('..................../'),nl,
write_proof(Proof).
For instance, given the following clauses:
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:
:-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:
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 Section 10.2 (appendix) for details).
Tip
We can use the Graphviz rendering engine 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.
% display a proof tree using Graphviz
:-use_rendering(graphviz).
prooftree(A,digraph([Options|Edges])):-
gv_options(Options),
prove_p(A,Edges),
numbervars(Edges).
% prove_p(A,P) <- P is proof tree of A
prove_p(true,[]):-!.
prove_p((A,B),[((A,B)->D),(Clause->D)|Proof]):-!,
clause(A,C),
copy_term((A:-C),Clause),
conj_append(C,B,D),
prove_p(D,Proof).
prove_p(A,[(A->B),(Clause->B)|Proof]):-
clause(A,B),
copy_term((A:-B),Clause),
prove_p(B,Proof).
% example clauses
student_of(S,T):-teaches(T,C),follows(S,C).
teaches(peter,cs).
teaches(peter,ai).
follows(maria,cs).
follows(paul,ai).
is_bird(X):-has_feathers(X),lays_eggs(X).
is_fish(X):-has_gills(X),lays_eggs(X).
has_feathers(tweety).
lays_eggs(tweety).
% Graphviz formatting
gv_options(node([shape=none,fontname='Courier'])).
% from library
conj_append(true,Ys,Ys).
conj_append(X,Ys,(X,Ys)):-X\=true,X\=(_One,_TheOther).
conj_append((X,Xs),Ys,(X,Zs)):-conj_append(Xs,Ys,Zs).
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.