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:
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.
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:
- A single constant: .
- A single function symbol of arity 1: .
- 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:
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:
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:
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.