The Peano Naturals

The Peano numbers are a unary number system for positive natural numbers where the zero is represented by a Z (or 0, or any atom - it doesn't matter) and every successor of a natural number N is the function S applied to N. We would therefore represent the natural number 3 with the term S(S(S(Z))). To look at it differently: in the Peano axioms, the naturals are defined as the set that contains zero and a closure over the successor function. In haskell we would define the type of the naturals like this:

data N = Z | S N

In Prolog we don't need a type definition for the naturals, as terms are generated without types. Now we want a predicate that checks whether our input is a natural number as we've defined it. The idea is that the term is a natural, iff either the term is a Z or it has an S as its root and its parameter is a natural. In Prolog we would write it intuitively like this:

naturals(z).
naturals(s(X)) :- naturals(X).

And indeed this checks whether our input is a natural number. The query naturals(s(s(z))). returns true while naturals(foo). does not. Writing down this program in Haskell is not very useful since the type system does not allow us to have anything else but a natural as the function parameter but let's pretend:

naturals v = case v of
              S x -> naturals x
              Z -> True
              _ -> False

And of course, calling naturals $ S $ S Z in haskell has the correct type and returns true. But this haskell program only corresponds to the case where we actually call the Prolog predicate with a bound parameter. We could call the prolog predicate with a free binding pattern like naturals(X). and get bindings for X for every solution, so every natural number. The corresponding Haskell programm would be:

naturals_f  = [ Z ] ++ map S naturals_f

This might need some explaining: The list corresponds to some notion of non-determinism. In Prolog the non-determinism is baked into the language due to backtracking from failed predicate evaluations and us asking for more answers. The Prolog program essentially says: Z is a solution. Everything with an S is a solution, if the "content" of the S is a solution as well. That's the same for our haskell programm. In our list of solutions we know that Z is in it and for every solution we have, adding an S leads to another one. And evaluating naturals_f starts to calculate the infinite list of natural numbers.

Now consider the following Prolog program where we switched the order of the clauses:

naturals(s(X)) :- naturals(X).
naturals(z).

This still works nicely for the bound case where we call naturals(s(s(z)). But if we now call naturals(X) we quickly get ERROR: Out of local stack. The natural intuition might be that the order of clauses does not matter but it does in this case. Writing down the equivalent Haskell programm we are able to see why:

naturals_f  = map S naturals_f ++ [ Z ]

We have the recursion before we have any solution. Well, the solution is easy: just write the simple case in the first line and the recursive case in the second. But let's consider another problem.

Repeated Printing

Consider the problem of repeatedly printing a character:

repeat(0, _).
repeat(N, C) :- write(C), NN is N - 1, repeat(NN, C).

This looks very correct and is very wrong.

?- repeat(5, f).
fffff
true ;
ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff...

Now we see why it's nice to represent the naturals als Peano numbers. After hitting 0 there's a choice point left and asking for another solution leads to the negatives and printing our character in an infinite loop. So let's augment the second rule to prevent us from going into the negatives.

repeat(0, _).
repeat(N, C) :- N > 0, write(C), NN is N - 1, repeat(NN, C).
% query:
?- repeat(5, f).
fffff
true ;
false.

This looks better but we still have a choice point left over which might be not so nice. The problem is that the matched patterns are not disjoint and after the end of the recursion there's still a pattern left over that fits. We can't encode that N should be larger than 0 in the head of the rule. Remember that we can match naturals larger than 0 (or any other number) in the rule head using Peano numbers - that's why they are so cool.

But how do we fix our problem with the left-over choice point? There are two ways we can do it. We can either introduce a cut or reorder the rules.

% Variant 1a: The order doesn't matter but we introduce a cut
repeat(0, _) :- !.
repeat(N, C) :- N > 0, write(C), NN is N - 1, repeat(NN, C).

% Variant 1b: If we promise to be good and only call repeat with a positive numeric argument, we can even leave out the range check
repeat(0, _) :- !.
repeat(N, C) :- write(C), NN is N - 1, repeat(NN, C).

% Variant 2: The order does matter
repeat(N, C) :- N > 0, write(C), NN is N - 1, repeat(NN, C).
repeat(0, _).

I personally think that the variant without the cut is nicer. So for terminating rules, it might be better to have the "smaller" rule last as to not leave choice-points hanging around. Of course, this only works if the matched terms in the rules are proper subsets of each other so that we actually can order the rules in that fashion. In general, that might not be possible.

Conclusion

• The order of rules can (in theory) not affect termination. But if our rules are already non-terminating for our query, the order and timeliness of results does matter. Then order does matter.
• Disjoint rule heads are important to not have left-over choice points.
• If rules are terminating but the rule heads are not disjoint, they still should be ordered carefully.
• Implicit conditions (N > 0) can lead to non-obvious non-termination if they are not made explicit.
• By encoding data properties in the term structure we can make some implicit conditions explicit and make rule-heads disjoint.
• Having numerical conditions in rule-heads would be really nice. Maybe some Prolog implementation in the future allows for that.