Skip navigation

In our Computational Logic seminar here at The University of Iowa, we are studying logic programming this semester.  We are using the very nice book “Logic, Programming, and Prolog”, freely available online.  We were talking today about the existence of a least Herbrand model for a definite program.  A definite program is just a set of clauses of the form A_0 \leftarrow A_1,\ldots,A_m, where each A_i is an atomic formula (predicate applied to terms).  (Free variables in clauses are interpreted universally.)  If m = 0, then we just have an atomic fact A_0 in the definite program.  A Herbrand interpretation is a first-order structure where each function symbol f of arity k is interpreted as \lambda x_1,\ldots,x_k. f(x_1,\ldots,x_k), and each predicate is interpreted as a subset of the set of ground (i.e., variable-free) atomic formulas.  A Herbrand model of a definite program P is then just a Herbrand interpretation which satisfies every clause in P.  It will be convenient below to identify a Herbrand interpretation with a subset of the set of all ground atomic formulas.  Such a subset determines the meanings of the predicate symbols by showing for which tuples of ground terms they hold.  We will pass tacitly between the view of a Herbrand interpretation as a first-order structure and the view of it as a set of ground atomic formulas.  The Herbrand base is the Herbrand interpretation corresponding to the set of all ground atomic formulas.  It says that everything is true.

What I want to talk about briefly in this post is the fact that the set of Herbrand models  of definite program P forms a complete partial order, where the ordering is the subset relation, the greatest element is the Herbrand base, and the greatest lower bound of a non-empty subset S of Herbrand models of P is the intersection of all the models in S.  In a complete partial order, every subset S of elements should have a greatest lower bound (though it need not lie in S).  Alternatively — and what I am interested in for this post — we can stipulate that every subset S should have a least upper bound.  The two formulations are equivalent, and the proof is written out below.  “Logic, Programming, and Prolog” contains a simple elegant proof of the fact that the intersection of a non-empty set of Herbrand models is itself a Herbrand model.

What I want to record here is the proof that in general, if in a partial order (X,\sqsubseteq) every subset S\subseteq X (including the empty set) has a greatest lower bound, then every such S also has a least upper bound.  The proof I have seen for this is a one-liner in Crole’s “Categories for Types”.  It took me some puzzling to understand, so I am writing it here as much for my own memory as for the possible interest of others, including others from the seminar who watched me fumble with the proof today!

Let S be a subset of X.  Let \textit{ub}(S) be the set of elements which are upper bounds of S (that is, the set of elements u which are greater than or equal to every element of S).  The claim is that the greatest lower bound of \textit{ub}(S) is the least upper bound of S.  By the assumption that every subset of X has a greatest lower bound, we know that there really is some element q which is the greatest lower bound of \textit{ub}(S).  As such, q is greater than or equal to every other lower bound of \textit{ub}(S).  Now here is a funny thing.  Every element x of S is a lower bound of \textit{ub}(S).  Because if y\in \textit{ub}(S), this means that y is greater than or equal to every element in S.  In particular, it is greater than or equal to x.  Since this is true for every y\in \textit{ub}(S), we see that x is a lower bound of \textit{ub}(S).  But q is the greatest of all such lower bounds by construction, so it is greater than or equal to the lower bound x.   And since this is true for all x\in S, we see that q is an upper bound of all those elements, and hence an upper bound of S.  We just have to prove now that it is the least of all the upper bounds of S.  Suppose u' is another upper bound of S.  This means u'\in\textit{ub}(S).  Since by construction q is a lower bound of \textit{ub}(S), this means that q \sqsubseteq u', as required to show that q is the least of all the upper bounds of S.

The final interesting thing to note about the complete partial order of Herbrand models of a definite program P is that while the greatest lower bound of a non-empty set S of models is their intersection, and while the greatest element is the Herbrand base (a universal Herbrand model), the intuitive duals of these operations are not the least element nor the least upper bound operation.  The intuitive dual of a universal Herbrand model would be, presumably, the empty Herbrand interpretation.  But this need not be a model at all.  For example, the definite program P could contain an atomic fact like p(a), and then the empty Herbrand interpretation would not sastisfy that fact.  Furthermore, if S is a non-empty set of Herbrand models, \bigcup S is not the least upper bound of S.  That is because \bigcup S need not be a Herbrand model of P at all.  Here is a simple example.  Suppose P is the definite program consisting of clauses \textit{ok}(h(a,b)) and \textit{ok}(h(x,y)) \leftarrow \textit{ok}(x),\textit{ok}(y).  Consider the following two Herbrand models H_1 and H_2 of this program P. In H_1 the interpretation of \textit{ok} contains all the terms built using h from a and h(a,b).  In H_2, the interpretation of \textit{ok} contains all the terms built using h from b and h(a,b).  If we take the intersection of H_1 and H_2, then it is a Herbrand model, in fact the minimal one: it says that \textit{ok}(h(a,b)) is true, as required by the first clause in P; and if two terms t_1 and t_2 are in the interpretation of \textit{ok}, then so is h(t_1,t_2).  But if we take the union of H_1 and H_2, what we get is not a Herbrand model of P at all.  Because H_1 \cup H_2 contains \textit{ok}(h(a,a)) and \textit{ok}(h(b,b)), for example, but not \textit{ok}(h(h(a,a),h(b,b))).  To get an upper bound of H_1 and H_2, it is not enough to take their union.  One must take their union and then close them under the deductive consequences of the program P.  That’s the intuition, though we would need to formally define closure under deductive consequences — and it would be a bit nicer to be able to apply a model-theoretic notion (since we are working model-theoretically here) rather than a proof-theoretic one.   Declaratively, we know we can get the least upper bound of a set S of Herbrand models as the intersection of the set of all Herbrand models which are supersets of every model in S.  But this is rather a hard definition to work with.

Anyhow, this is a nice example of finding an interesting abstract structure in semantics, as well as a good exercise in reasoning about such structures.

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: