Trying to write a tree-height predicate - do I need Peano-style natural numbers?

Question

As a basic Prolog exercise, I set myself the task of writing a binary tree height predicate that would work forwards and "backwards" - that is, as well as determining the height of a known binary tree, it should be able to find all binary trees (including unbalanced ones) of a known height. This is the best solution I've come up with so far...

tree_eq1([],s).  % Previously had a cut here - removed (see comments for reason)
tree_eq1([_|T],n(L,R)) :- tree_eq1(T,L), tree_eq1(T,R).
tree_eq1([_|T],n(L,R)) :- tree_eq1(T,L), tree_lt1(T,R).
tree_eq1([_|T],n(L,R)) :- tree_lt1(T,L), tree_eq1(T,R).

tree_lt1([_|_],s).
tree_lt1([_,X|T],n(L,R)) :- XX=[X|T], tree_lt1(XX,L), tree_lt1(XX,R).

The first argument is the height, expressed as a list - the elements are irrelevant, the length of the list expresses the height of the tree. So I'm basically abusing lists as Peano-style natural numbers. The reasons this is convenient are...

1. No concerns about negative numbers.
2. I can check for > or >= without knowing the exact number - for example, by matching two items on the head of the list, I ensure the list length is >=2 without caring about the length of the tail.

Neither of these properties seem to apply to Prolog numbers, and I can't think of a way so far to adapt the same basic approach to use actual numbers in place of these lists.

I've seen a few examples in Prolog using Peano-style numbers, so my question is - is this normal practice? Or is there some way to avoid the issue that I haven't spotted yet?

Also, is there a way to convert to/from a Peano-style representation that won't break the bidirectionality? The following don't work for fairly obvious reasons...

length(L,N), tree_eq1(L,X).
  % infinite set of lists to explore if N is unknown

tree_eq1(L,X), length(L,N)
  % infinite set of trees to explore if X is unknown

The best I can think of so far is an is-this-variable-instantiated test to choose between implementations, which seems like cheating to me.

BTW - I have some ideas for other methods which I don't want spoilers for - particularly a kind of dynamic programming approach. I'm really focused on fully understanding the lessons from this particular attempt.

Hoogh

Why the cut in the first clause of the tree_eq1/2 predicates? Specially when you want predicate bi-directionality? – Tommy

@Paulo - I tried to fix the problem a few ways. One very-quickly-proved-futile approach was with cuts (but how to decide when to cut?). That one case, though, looked completely safe at the time - knowing either argument and getting a match is sufficient to prove the other cases don't apply (neither height 0 nor stubs). Of course the fallacy there (as mats answer strongly hints) is that both arguments may validly be unknown, so now I think about it that way, that cut shouldn't be there. – Hoogh

@Paulo - I've been congratulating myself for working out that there is no backwards evaluation in Prolog even though it's sometimes described that way - just forwards evaluation using a method that can solve for different choices of unknowns - so I really should have considered the case of solving for all arguments unknown and noticed this earlier. Of course I'm ignoring any seemingly-backward-evaluation effects from backtracking and focusing on unification. – Hoogh

Related. – Quadratic

@dgilperez: There is already the tag successor-arithmetics – Quadratic

Answer 1

First: +1 for using lists lengths for counting, which sometimes really is quite convenient and a nice alternative for successor notation.

Second: For reversible arithmetic, you typically use constraints instead of successor notation, because constraints allow you to work with actual numbers and come with built-in definitions of the usual mathematical relations among numbers.

For example, with SICStus Prolog or SWI:

:- use_module(library(clpfd)).

tree_height(s, 0).
tree_height(n(Left,Right), Height) :-
        Height #>= 0,
        Height #= max(HLeft,HRight) + 1,
        tree_height(Left, HLeft),
        tree_height(Right, HRight).

Example query:

?- tree_height(Tree, 2).
Tree = n(s, n(s, s)) ;
Tree = n(n(s, s), s) ;
Tree = n(n(s, s), n(s, s)) ;
false.

Third, notice that the most general query, ?- tree_eq1(X, Y)., does not work satisfactorily with your version. With the snippet above, at least it gives an infinite number of solutions (as it should):

?- tree_height(T, H).
T = s,
H = 0 ;
T = n(s, s),
H = 1 ;
T = n(s, n(s, s)),
H = 2 .

I leave their fair enumeration as an exercise.

Quotidian

That's interesting. There's no sign of that in my (very old second hand) books, but as it's a library/extension I guess that's no surprise. By "fair enumeration" point, you mean so the solutions come in order of increasing size or increasing height? Something that means you don't have to do infinite enumerating just to find all the small solutions? – Hoogh

Most Prolog text books are way outdated (I mean by decades), so do not expect to see the more interesting stuff explained in books currently. (Finite domain constraints are available without loading any library in B-Prolog and GNU Prolog for example.) Fair enumeration means that every solution is (eventually) displayed. – Quotidian

Isn't Height #>= 1 better than Height #>= 0? – Quadratic

The point here is that, at least in this case, you do not even have to think further than what you already know about Height, and it still suffices. You know a tree height is #>= 0. Let CLP(FD) do the rest. Of course, we know that when we are describing a node that is not a leaf, Height must also be #> 0. Thus, if at all, I would recommend Height #> 0, so we more readily see that the clauses are exclusive. – Quotidian