# Prolog Programs, Order of Evaluation, and Functional Equivalents

While teaching Prolog this semester I had a few thoughts about Prolog programs and their equivalent programs in a functional programming language like Haskell.

## 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.