1

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

false
  • 10,264
  • 13
  • 101
  • 209
MWB
  • 11,740
  • 6
  • 46
  • 91
  • 1
    Note that @false's comment https://stackoverflow.com/questions/65427391/pure-prolog-peano-number-apartness#comment115687920_65427871 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. – Isabelle Newbie Dec 24 '20 at 16:40
  • @IsabelleNewbie You don't find this behavior of `less/2` troubling on its own? – MWB Dec 24 '20 at 16:55
  • 1
    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*. – Isabelle Newbie Dec 24 '20 at 17:41
  • @IsabelleNewbie I see what you and @ false mean now. Thanks. – MWB Dec 24 '20 at 19:46
  • 1
    @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. – false Dec 25 '20 at 12:57
  • @false Yes, thank you for the clarification. I try to be precise about solutions vs. answers, but sometimes I'm sloppy. – Isabelle Newbie Dec 25 '20 at 14:19

1 Answers1

4

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