4 ms·

Interesting. Could some kind of topological sort of the clauses, like I think Unix make does for the rules defined in a makefile, be applicable and of help, o

• YeGoblynQueenne 6y ago
  Sort of, not quite far off. Basically it's possible to impose a total ordering over the Herbrand base (the set of atomic formulae from which clauses are composed) or the set of constants in a Prolog program in such a way that a program is guaranteed to terminate, provided it adheres to the given ordering, but that is something that has to be hand-crafted, i.e. there's no known way to come up with such an ordering beforehand. Sorry I can't think of a very good example right now, but suppose you have a program like this: p:- q q:- p Given Prolog's top-down evaluation, that will enter an infinite recursion. It is possible to avoid this by ordering the Herbrand base so that either p > q or q > p, which precludes one of the two clauses (so p>q is violated by "q:-p" because "p" must come before "q" in a clause). This means that some programs (like the example above) can't be written. With an ordering over constants also, termination can be guaranteed when the lexicographic ordering is violated so for instance, with the natural numbers ordered in descending order, the following program terminates: even(0). even(X):- r(X,Y), odd(Y). odd(X):- r(X,Y), even(Y). Because (given even/1 and odd/1 are relations over the naturals) r(X,Y) can only be a relation between X and Y where X > Y, so the predicate will only count down towards 0, rather than up towards infinity. This is basically the gist of stratification used to allow decidable recursion or negation in datalog languages. But that is an ordering of atoms within clauses and constants within atoms, not clauses. I don't know of any principled way to order clauses in a program to guarantee termination. That would be interesting to have.
  • vram22 6y ago
    Thanks for the detailed reply. >Sorry I can't think of a very good example right now No problem. I should say that I didn't understand your reply fully, due to not having the full necessary background. But I think I got the rough gist of the first half of the reply, and a part of the second half. I had learned only a little Prolog, many years ago, just out of interest, only from books, and did not have access to any machine to try it on at the time. But I do remember bits of it, fuzzily (pun intended). So let me take a guess at what the second program means: >even(0). That is a fact stating: 0 is even. >even(X):- r(X,Y), odd(Y). That is a rule, stating: X is even if there is a relation r between X and Y, and (comma means and in Prolog, IIRC) if Y is odd. >odd(X):- r(X,Y), even(Y). X is odd if there is a relation r between X and Y, and Y is even. I don't understand the rest of the second half of your reply, at present, although I did think about it a bit. Maybe I need to study it more, or maybe I lack some prequisite knowledge. >I don't know of any principled way to order clauses in a program to guarantee termination. That would be interesting to have. Yes, I too think it would. That was the idea and question I originally asked about. I did intuitively think it was a difficult problem, but who knows, it may get solved in the future. I think that would make Prolog quite a bit more powerful. Anyway, good to know that my idea was not totally off base, at least. Cheers :)
    • YeGoblynQueenne 6y ago
      Apologies, I assumed a background in logic programming -I should have explained things better. Yes, your interpretation of the second prorgam is correct and yes your idea is not off base at all :)
      • vram22 6y ago
        No problem, and thank you again :)