Herbrand universe and Least herbrand Model

Question

I read the question asked in Herbrand universe, Herbrand Base and Herbrand Model of binary tree (prolog) and the answers given, but I have a slightly different question more like a confirmation and hopefully my confusion will be clarified.

Let P be a program such that we have the following facts and rule:

q(a, g(b)).
q(b, g(b)).
q(X, g(X)) :- q(X, g(g(g(X)))).

From the above program, the Herbrand Universe

Up = {a, b, g(a), g(b), q(a, g(a)), q(a, g(b)), q(b, g(a)), q(b, g(b)), g(g(a)), g(g(b))...e.t.c}

Herbrand base:

Bp = {q(s, t) | s, t E Up}

• Now come to my question(forgive me for my ignorance), i included q(a, g(a)) as an element in my Herbrand Universe but from the fact, it states q(a, g(b)). Does that mean that q(a, g(a)) does not suppose to be there?
• Also since the Herbrand models are subset of the Herbrand base, how do i determine the least Herbrand model by induction?

Note: I have done a lot of research on this, and some parts are well clear to me but still i have this doubt in me thats why i want to seek the communities opinion. Thank you.

Answer 1

From having the fact q(a,g(b)) you cannot conclude whether or not q(a,g(a)) is in the model. You will have to generate the model first.

For determining the model, start with the facts {q(a,g(b)), q(b,g(b))} and now try to apply your rules to extend it. In your case, however, there is no way to match the right-hand side of the rule q(X,g(X)) :- q(X,g(g(g(X)))). to above facts. Therefore, you are done.

Now imagine the rule

q(a,g(Y)) :- q(b,Y).

This rule could be used to extend our set. In fact, the instance

q(a,g(g(b))) :- q(b,g(b)).

is used: If q(b,g(b)) is present, conclude q(a,g(g(b))). Note that we are using here the rule right-to-left. So we obtain

{q(a,g(b)), q(b,g(b)), q(a,g(g(b)))}

thereby reaching a fixpoint.

Now take as another example you suggested the rule

q(X, g(g(g(X)))) :- q(X, g(X)).

Which permits (I will no longer show the instantiated rule) to generate in one step:

{q(a,g(b)), q(b,g(b)), q(a,g(g(g(b)))), q(b, g(g(g(b))))}

But this is not the end, since, again, the rule can be applied to produce even more! In fact, you have now an infinite model!

{g(a,gn+1(b)), g(b, gn+1(b))}

---

This right-to-left reading is often very helpful when you are trying to understand recursive rules in Prolog. The top-down reading (left-to-right) is often quite difficult, in particular, since you have to take into account backtracking and general unification.

Answer 2

Concerning your question:

"Also since the Herbrand models are subset of the Herbrand base, how do i determine the least Herbrand model by induction?"

If you have a set P of horn clauses, the definite program, then you can define a program operator:

T_P(M) := { H S | S is ground substitution, (H :- B) in P and B S in M }

The least model is:

inf(P) := intersect { M | M |= P }

Please note that not all models of a definite program are fixpoints of the program operator. For example the full herbrand model is always a model of the program P, which shows that definite programs are always consistent, but it is not necessarily a fixpoint.

On the other hand each fixpoint of the program operator is a model of the definite program. Namely if you have T_P(M) = M, then one can conclude M |= P. So that after some further mathematical reasoning(*) one finds that the least fixpoint is also the least model:

lfp(T_P) = inf(P)

But we need some further considerations so that we can say that we can determine the least model by a kind of computation. Namely one easily observes that the program operator is contiguous, i.e. preserves infinite unions of chains, since horn clauses do not have forall quantifiers in their body:

union_i T_P(M_i) = T_P(union_i M_i)

So that again after some further mathematical reasoning(*) one finds that we can compute the least fixpoint via iteration, witch can be used for simple induction. Every element of the least model has a simple derivation of finite depth:

union_i T_P^i({}) = lpf(T_P)

Bye

(*) Most likely you find further hints on the exact mathematical reasoning needed in this book, but unfortunately I can't recall which sections are relevant:
Foundations of Logic Programming, John Wylie Lloyd, 1984
http://www.amazon.de/Foundations-Programming-Computation-Artificial-Intelligence/dp/3642968287