How to express a Total Order Relation in Prolog?

Question

What is the best way to express a total order relation in Prolog ?

For example, say I have a set of facts

person(tim)
person(ana)
person(jack)
...

and I want to express the following truth about a person's fortune: for each two persons X and Y, if not(X==Y), either X is richer than Y or Y is richer than X.

So my problem is that the richer clause should be capable of instantiating its variables and also to ensure that it is never the case that richer(X, Y) and richer(Y, X) at the same time.

Here is a better example to see what I mean:

person(tim).
person(john).
happier(tim, john).

hates(X, Y) :- person(X), person(Y), richer(Y, X).
hates(X, Y) :- person(X), person(Y), richer(X, Y), happier(Y, X).

Now the answer to the query hates(john, tim) should return true, because if richer satisfies the mentioned property, one of those two hates clauses must be true. In a resolution based inference engine I could assert the fact (richer(X, Y) V richer(Y, X)) and the predicate hates(john, tim) could be proved to be true. I don't expect to be able to express this the same way in Prolog with the same effect. However, how can I implement this condition so the given example will work ?

Note also that I don't know who is richer: tim or john. I just now that one is richer than the other.

Thank you.

Answer 1

you cannot write in pure Prolog that a predicate should be a total order: that would require higher order logic since you want to declare a property about a predicate.

this is a predicate that checks if a relationship is total order on a finite set:

is_total_order(Foo,Set):-
    forall(
           (member(X,Set),
        member(Y,Set)),
           (
        XY =.. [Foo,X,Y],
        YX =.. [Foo,Y,X],
        (call(XY);call(YX)),                %checking if the relationship is total
        \+ (call(XY),call(YX), X\=Y)        %checking if it's an order
           )
          ).

the operator =../2 (univ operator) creates a predicate from a list (ie: X =.. [foo,4,2]. -> X = foo(4,2)) and the predicate call/1 calls another predicate. As you can see we use meta-predicates that operate on other predicates.

For an total order on infinite sets things get more complicated since we cannot check every single pair as we did before. I dont even think that it can be written since proving that a relationship is a total order isn't something trivial.

Still, this doesnt declare that a predicate is a total order; it just checks if it is.

Answer 2

So I believe your question is the best way to represent the relation between these 3 people. If you don't actually care about their wealth #'s, just their relative order, you could add predicates like this -

is_richer(tim, anna).
is_richer(anna, jack).

and then a predicate to find all people who X is richer than -

richer(X, Z) :-
   is_richer(X, Z).
richer(X, Z) :-
   is_richer(X, Y),
   richer(Y, Z).

If your is_richer predicate contains cycles though (in this example, if you added is_richer(jack, tim)), this could explode. You need to track where you have visited in this tree.

An example run of richer would be:

?- richer(X, Y).
X=tim
Y=anna ;
X=anna
Y=jack ;
X=tim
y=jack ;
no