Meta-Programming in Prolog – Part 2

Here is the story thus far: a meta-program is a program that takes another program as input or output. Based on this idea we wrote an interpreter for a simple logic programming language and later extended it to build a proof tree. A proof of concept, if you will. Meta-interpreters have lost a lot of steam in the last years. The reason being that they are just too hard to write in most popular programming languages. There’s no a priori reason that prevents us from writing a meta-interpreter in e.g. Python or Java, but the truth is that it’s such a lot of work that it’s not worth the trouble in most cases. The only exception that I can think of are integrated development environments which typically have at least some semantic awareness of the object language. But these languages doesn’t have a simple core and makes parsing awkward to say the least. In logic programming the situation is different. If an interpreter supports definite Horn clauses — facts and rules — and built-in operations it’s powerful enough to run quite a lot of real programs.

So what’s the purpose then? Is meta-programming just a sterile, academic exercise that has no place in real world software development? Since that was a rhetorical question, the answer is no. A resounding no! First, meta-interpreters are great for experimenting with new language features and implementation techniques. For instance we could ask ourself if it would be worthwhile to add support for new search rules in Prolog instead of defaulting to a simple depth-first search. Implementing a new search rule in a meta-interpreter can be done in a few hours, and the resulting program won’t be longer than perhaps a page of code (unless you screwed up, that is). Doing the same task in an imperative programming environment could take days or even weeks depending on the complexity of the existing code base. So meta-programming is useful for prototyping. What else? It can actually be a great aid in debugging. In the following sections we’re going to explain what debugging means in logic programming and develop a simple but functional system for squashing bugs.

Algorithmic debugging

Assume that we have a logic program and a goal query . Sterling and Shapiro cites three possible bugs in The Art of Prolog:

1. The interpreter could fail to terminate.
2. The interpreter could return a false solution . (incorrectness)
3. The interpreter could fail to return a true solution . (insufficiency)

Since the first problem is undecidable in general we shall focus on the latter two. But first we need to decide what the words true and false means in this context, and in order to do that some remarks about the semantics of logic programs have to be made. If you’re feeling a bit rusty, I urge you to read up a bit on Herbrand models. Wikipedia and my own earlier post are both good starting points. The basic idea is fortunately rather simple. Logic formulas and programs can be viewed as specifications of models. A model is an interpretation in which the program is true. In general there are many, infinitely many, models of any given definite logic program. Which one should we choose? In a model we are free to reinterpret the non-logical vocabulary in any way we see fit. Consider the following logic program:

It can be seen as a specification of either the set or the set . Notice the subtle difference. The latter model is simpler in the sense that it doesn’t take us outside the domain of the textual representation of the program itself. Such models are known as Herbrand models. Could we be so lucky that Herbrand models are the only kind of models that we need to pay attention to? This is indeed the case. If a logic program has a model then it also has a Herbrand model. But we still need to pick and choose between the infinitely many Herbrand models. The intuition is that a model of a logic program shouldn’t say more than it have to. Hence we choose the smallest Herbrand model as the meaning of a logic program. Or, put more succinct, the intersection of all Herbrand models. For a logic program , let denote the smallest Herbrand model of .

This is good news since we now know that every well-formed logic program has a meaning. Let’s return to the question of false solutions. This notion is only relevant if the programmer has an intended meaning that differs from the actual meaning of the program. In all but the most trivial programming tasks this happens all the time. An intended meaning of a logic program is the set of ground goals for which the program should succeed. Note the “should”. If we briefly return to , the intended meaning is nothing else than the actual meaning, i.e. the set . With this terminology it’s possible to give a precise definition of incorrectness and insufficiency of a logic program :

1. is incorrect iff .
2. is insufficient iff .

With these definitions we see that the program is neither incorrect nor insufficient. But let’s introduce some bugs in it:

Can you spot them? is incorrect since the base clause is too inclusive. is not a subset of since e.g. the element is not a member of . In the same vein, is insufficient since it’s equivalent to just .

Quite a lot of legwork to explain something which is actually rather simple! What remains is to put everything in practice. Due to space constraints we’ll focus on the incorrectness problem.

Incorrectness

A logic program is incorrect if it gives solutions that are not included in the intended model. In a real-world situation this means that the programmer has found a goal which the program should reject, but it doesn’t, and hence it contains at least one bug. The purpose is to find the part in the program that is responsible for the bug. In logic programming terms this is of course a clause. A clause is false iff is true and is false. The purpose of the algorithm is to traverse the proof tree and find such a clause. With this in mind we can at least write the top-level predicate:

   false_solution(Goal, Clause) :-
       %Build a proof tree.
       interpreter::prove(Goal, Tree),
       %Find a false clause.
       false_goal(Tree, Clause).

Well, that wasn’t too hard. What about ? The tree is of the form . Hence there are two cases: either is false or it’s true. If it’s false, then we must continue the search in . If it’s true, then the current clause is the clause that we’re looking for. To determine whether is false we need an auxiliary predicate, , where the first argument is the conjunction of nodes and the second argument is the false clause (if it exists).

   false_goal((A :- B), Clause) :-
       (    false_conjunction(B, Clause) ->
            true
       ;    Clause = (A :- B1),
            %Necessary since we don't want the whole tree.
            extract_body(B, B1)
       ).

By the way, this is a fine example of top-down development. In each step we’re breaking the original problem into easier problems and assume that we’re able to solve them later. is a bit trickier. The first argument is a conjunction of nodes of the form . Just like before there are two cases since is either false or true. If it’s true, then we move on to the rest of the nodes. If it’s false, then we’d like to know whether is true or false. Luckily we’ve already solved this problem before — a call to will do the trick just fine.

   false_conjunction(((A :- B), _Bs), Clause) :-
       query_goal(A, false),
       !,
       false_goal((A :- B), Clause).
   %Almost the same case as above, but with only one element.
   false_conjunction((A :- B), Clause) :-
       query_goal(A, false),
       !,
       false_goal((A :- B), Clause).
   false_conjunction((_A, As), Clause) :-
       %A is implicitly true.
       false_conjunction(As, Clause).

Only the most perplexing predicate remains: . The second argument is if is true and if it’s false. How can we know this? This is where the programmer’s intended model enters the picture. For now, we’re just going to use her/him as an oracle and assume that all choices are correct. The predicate is then trivial to write:

   query_goal(G, Answer) :-
       %Change later.
       write('Is the goal '),
       write(G),
       write(, ' true?'),
       nl,
       read(Answer).

In essence the user will be asked a series of questions during a session with the program. Depending on the answers, i.e. the intended model, the program will dive deeper and deeper into the proof tree in order to find the troublesome clause. As an example, here’s an append program where the base case is wrong:

append([_X], Ys, Ys) :- true.
append([X|Xs], Ys, [X|Zs]) :-
    append(Xs, Ys, Zs).

And the session with the program would look like this:

[1]  ?- debugging::false_solution(append([a,b,c], [d,e], Xs), Clause).
Is the goal append([b,c],[d,e],[b,d,e]) true?
|: false.
Is the goal append([c],[d,e],[d,e]) true?
|: false.
Xs = [a, b, d, e],
Clause = (append([c], [d, e], [d, e]):-true)

And we clearly see that it’s the base case that’s wrong.

Summary

The algorithm was taken from The Art of Prolog. Some simplifying assumptions have been made. Among other things there’s currently no support for built-in operations. This is rather easy to fix, however. A more serious question is if it would be possible to minimize the role of the oracle, since it’s now queried every time a decision needs to be made. There are two techniques for coping with this. Either we do a smarter traversal of the proof tree with e.g. divide and conquer, or we find a way to approximate the intended model of the program without the use of an oracle.

Source code

The source code is available at https://gist.github.com/1351227.

A Gentle Introduction to Herbrand Models

Almost related pun of the day: Some interpretations are more equal than others.

I’ve not yet encountered a single person — including myself — who have grasped the concept and utilities of Herbrand interpretations at a first glance. This might lead one to believe that the theory is so hard and abstract that it’s not really related to every day logic programming anyway, but nothing could be further from the truth. On the contrary, the problem is rather that the definition of a Herbrand interpretation is too simple to make any sense — a wolf in sheep’s clothing. Hence we have a good subject at hand and a splendid opportunity for me to confuse you further with deceptive didacticism.

A logic program is a finite set of rules and facts. Let’s not bother ourselves by giving a formal definition and instead cut right to the chase with an example:

From a pragmatic perspective it should be construed as: is natural (i.e. a natural number), and if it is known that is a natural number, then it’s the case that is a natural number. I’ll be the first one to admit that it’s not a very interesting program, but it’ll have to do for the moment. Following this intuition it’s possible to answer queries to the program in two different ways: top-down and bottom-up. Let our query be . Here’s how the two different strategies differ:

Top-down

To solve , we unify with and obtain the unifier . Then we recursively solve the new goal obtained from the right-hand side of the rule: . This can be done in one step, and since there are no more goals to resolve we’re done.

Bottom-up

We begin to note that holds. A solid start! Then, since the body of the second clause is true with the unifier (the same as before), we conclude that must also be true. Since this is the same as the original query there’s no reason to continue.

I’ve admittingly danced over a lot of intricate details, but I should at least mention that the top-down approach corresponds to SLD-resolution while the bottom-up approach corresponds to unit-resolution (sometimes called hyper-resolution). The difference between the two lies in the application of the resolution rule: in SLD-resolution we produce resolvents between a head of clause and a goal clause, in unit-resolution we produce resolvents between a unit-clause and the body of a clause. So we have two ways of answering a query, but how do we know that they are correct? For that we need to backtrack (pun not intended) and carefully explicate the meaning of the program. This is formally done with a model. The content of this particular program is:

1. A single constant: .
2. A single function symbol of arity 1: .
3. A single predicate symbol of arity 1: .

And to provide a meaning to the program we need to explain exactly what these symbols mean. We need two functions: one for the constant symbol, , and one for the function symbol, . In the domain of the natural numbers these can be defined as:

1. 
2. 

Which may then be combined into a single function, , that allows us to recursively compute the value of any term in the program. It is defined as:

For example:

The only predicate symbol, , must be mapped to a relation on the domain. The simplest such is just the set . And we’re done with this particular model.

Is it a good model? That depends. In the context of our logic program it seems to be a bit overkill. Previously we only had to worry about the symbols that actually appeared in the program: , and ; but now we’ve introduced arithmetical notation that so to speak goes beyond the original interpretation. There’s really no reason at all to demand that must be evaluated to and that must be evaluated to . They are just two different representations. With this in mind we can construct a simpler model:

1. 
2. 

And in the same vein as before this may be combined into a single function . Applied to the same term as before we obtain:

We’re back with what we started with! This means that the terms in the program are just mapped to themselves, and why not? The predicate symbol will now be mapped to the relation instead of .

These kinds of models are known as Herbrand models. The general definition closely mimics the earlier one, with the effect that all terms are mapped to themselves and that predicates are mapped to relations over the universe of terms (the Herbrand universe). Since the only interesting part of a Herbrand model is the mapping of predicates, it’s often presented as a set that enumerates the values for which the predicates should be true. In our example, which is in fact a least Herbrand model, this was . As should be evident by now this is precisely the set that we already had in mind as programmers, it’s the intended meaning of the program.

But was this just a fluke? Could there be cases where it’s impossible to find a Herbrand model even though there’s exists another model? Fortunately the answer is no: if there exists a model for a logic program then there also exists a Herbrand model. This provides a theoretical justification for both SLD- and unit-resolution. In the first case we use this in our search for unsatisfiable sets of ground clauses from the Herbrand universe, in the second case we actually build the (least) Herbrand model from bottom up.