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