`less/2` relation in Peano arithmetic

Question

This less-than predicate in Peano arithmetic

less(0, s(_)).
less(s(X), s(Y)) :- less(X, Y).

loops when

?- less(X, Y), X=s(0), Y=0.

Is there a better way to write less/2 (using Horn clauses only)?

Tsuda

Note that @false's comment #65427891 is about a "naive" neq/2 built on top of less/2. It's not pointing out a problem with less/2, it's saying that in Prolog the disjunction of two goals that each have infinite solutions will not behave fairly. – Kimble

@IsabelleNewbie You don't find this behavior of less/2 troubling on its own? – Tsuda

Not if you want a less/2 that is capable of enumerating answers. If it can enumerate answers, then this query says "enumerate all pairs of N, M such that N < M, until you find a pair that I know cannot exist". This enumeration loops necessarily. The difference to neq/2 is important since there, unlike for less/2, the assignment X=s(0), Y=0 is a valid solution. When you ask neq/2 to search for this solution, looping is unnecessary. – Kimble

@IsabelleNewbie I see what you and @ false mean now. Thanks. – Tsuda

@IsabelleNewbie: "disjunction of two goals that each have infinite solutions will not behave fairly" counterexample: ( X = f(_) ; X = g(_) ). This is a disjunction of two goals with infinite solutions each. And it even terminates, thus enumerates the solutions fairly. What needs to be required further is that these infinite solutions can only be described with infinitely many answers. Otherwise I completely agree with you, indeed. – Consignment

@Consignment Yes, thank you for the clarification. I try to be precise about solutions vs. answers, but sometimes I'm sloppy. – Kimble

Answer 1

You can use when/2. Making it not anymore an infinitely enumerating predicate and still keeping it 100% pure. The when/2 modifies the S (selection rule) in SLD-Resolution, an idea that can be traced back to Alain Colmerauer.

less(X, Y) :- when((nonvar(X),nonvar(Y)), less2(X,Y)).
less2(0, s(_)).
less2(s(X), s(Y)) :- less(X, Y).

The rewriting of less/2 into less/2 and less2/2 is similary like tabling rewriting. You insert a stub and rename the clause head. But the recursive call in the body is not rewritten, is then a call to the stub again.

You now get steadfastness:

?- less(s(s(0)), s(s(s(0)))).
true.

?- less(X, Y), X = s(s(0)), Y = s(s(s(0))).
X = s(s(0)),
Y = s(s(s(0))).

And even failfastness and truefastness sometimes:

?- less(s(s(_)), s(0)).
false.

?- less(s(0), s(s(_))).
true.

Some Prolog systems even provide a table/1 like directive, so that you don't need to do the rewriting, only make the declaration. One such system is SICStus Prolog. In SICStus Prolog, thanks to the block/1 directive,

you would only write:

:- block less(-,?), less(?,-).
less(0, s(_)).
less(s(X), s(Y)) :- less(X, Y).

For a 1980's Paper see for example:

An Implementation of dif and freeze in the WAM
Mats Carlsson - December 18, 1986
http://www.softwarepreservation.com/projects/prolog/sics/doc/Carlsson-SICS-TR-86-12.pdf/view

Cuttie

less(X, 0) now flounders. – Consignment

Right, you would need even more complex conditions or intermediary predicates. – Consignment

The question rather is: is floundering really better than looping? – Consignment

Let us continue this discussion in chat. – Cuttie