Checking whether the tree is avl-tree in prolog. error

My programm is not working correct. When I try to test it I have an error.

My example for testing:

if_avl_tree(t(t(t(nil/0, 3, nil/0)/1, 7, t(t(nil/0, 9, nil/0)/1, 11, nil/0)/2)/3, 16, t(nil/0, 25, t(nil/0, 40, nil/0)/1)/2)/4).

This is my code:

if_avl_tree(t(_,_,_)/_ ) :- T=t(_,_,_)/_ , is_binTree(T), if_avl_tree(T, _), !.
if_avl_tree(nil/0, 0).
if_avl_tree(t(nil/0,_, nil/0), 1).
if_avl_tree(t(L,_,R )/H, Hh) :- if_avl_tree(L, H1), 
                                if_avl_tree(R, H2), abs(H1 - H2) =< 1, !,                                                                                      
                                H3 is 1 + max(H1,H2), H3=:=Hh.

is_binTree(nil/0) :- !.
is_binTree(t(L,_,R)/_):- is_binTree(L), is_binTree(R).

And this is my error:

ERROR: Arguments are not sufficiently instantiated
ERROR: In:
ERROR:   [10] 1=:=_6218
ERROR:    [8] if_avl_tree(t(...,16,...)/4) at e:/prolog/tasks/lab06tomashchuk.pl:50
ERROR:    [7] <user>
ERROR: 
ERROR: Note: some frames are missing due to last-call optimization.
ERROR: Re-run your program in debug mode (:- debug.) to get more detail.

Solution

Your sample code is definitely along the right track, but has a few anomolies.

Let's start with a simple representation for a binary tree:

btree(Value, Left, Right)

This is pretty self explanatory. And if there is no subtree, the atom nil can be used.

If we want to validate whether a structure is a binary tree, we can do it this way:

is_binary_tree(nil).    % Allow for a nil tree with no values
is_binary_tree(btree(_, Left, Right)) :-
    is_binary_tree(Left),
    is_binary_tree(Right).

A binary tree is AVL if the heights of the two child subtrees of any node differ by at most one. If your binary tree representation already has the height of each tree as part of the tree representation, like so:

btree(Value, Left, Right)/Height

Then it must be assumed the Height is maintained when the tree contents or structure is changed. If they're not being changed, then the decision as to whether it's an AVL tree doesn't require and extra height argument to be carried around. The heights are already pre-calculated and maintained, so they only need to be checked:

is_AVL_tree(nil/0).
is_AVL_tree(btree(_, Left, Right)/_) :-
    Left = btree(_, _, _)/HeightLeft,
    Right = btree(_, _, _)/HeightRight,
    abs(HeightLeft - HeightRight) =< 1,
    is_AVL_tree(Left),
    is_AVL_tree(Right).

You don't need a separate base case for a height of 1. It's taken care of by the two rules above.

If you don't have the heights predetermined through maintenance of the tree as an argument in the term, then we'll need to carry along the heights as an argument and calculate them. t's not needed as part of the tree representation. That would be redundant and make the rules unnecessarily messy.

is_AVL_tree(nil, 0).
is_AVL_tree(btree(_, Left, Right), Height) :-
    is_AVL_tree(Left, HeightLeft),
    is_AVL_tree(Right, HeightRight),
    abs(HeightLeft - HeightRight) =< 1,
    Height is 1 + max(HeightLeft, HeightRight).