Comment by Avshalom | Hacker News Reader

Comment by Avshalom | Hacker News Reader

Parent Full thread

Mode declarations aren't really a feature so much as they are additional information provided by the programmer to the compiler. In Prolog if you have a predicate

  foo(X,Z) :- 
    bar(X,Y), 
    baz(Y,Z).

Traditionally if you call foo(1,Z) it will try to find an answer for bar(1,Y) first then feed that Y value into baz, if you call foo(X,3) it will still try to find values for bar(X,Y) first. Sometimes that's okay because the engine will be like well yeah there's something that'll work so we'll say bar is true and move on to baz but some times it tell you to go suck eggs.

You could write two different versions of foo

  %foo(in,out)
  foo(X,Z) :- 
    ground(X),
    bar(X,Y), 
    baz(Y,Z).
  %foo(out,in)
  foo(X,Z) :- 
    ground(Z),
    baz(Y,Z),
    bar(X,Y).

but having to do that sucks. First it's forcing you to think about Prolog's implementation rather than the logical relationship between X and Z; second it's repetitive and forces you to keep both versions in sync with each other which is gonna get rough for more complex predicates.

One of the things Mercury uses that mode info for is to re-arrange the body of foo(X,Y). So if you tell it that you will use both foo(in,out) and foo(out,in) it will compile two different versions of foo and dispatch appropriately.

>> One of the things Mercury uses that mode info for is to re-arrange the body of foo(X,Y). So if you tell it that you will use both foo(in,out) and foo(out,in) it will compile two different versions of foo and dispatch appropriately.

Very good point (missing from my essay below). To add some context, in Prolog at least, because of the depth-first-search implementation of the search for answers (more corretly, but formally: for resolvents) the order in which the clauses of a program are placed in the source file can make the difference between the program entering an infinite recursion when it is called in a certain mode, and the program terminating in the same mode.

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, or is that not meaningful here? PL theory is not my area, just throwing out a wild idea :)

I had been studying make and working on some topological sorting algorithms lately, is how I thought of the idea.

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.

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 :)

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 :)

No problem, and thank you again :)

And third, it produces redundant solutions for ground queries.

Reply on news.ycombinator.com