Why does this expression not unifiy

Question

I have defined the following knowledge base:

leaf(_).
tree(X) :- leaf(X).

and was expecting the query:

leaf(X) = tree(X).

to return true ., because any leaf should per definition be a tree.

Unfortunately activating trace doesn't yield any useful results. Here is a link to this minimal example if you'd like to play around with it.

Answer 1

Short answer: you here check if the term leaf(X) can be unified with tree(X). Since these are terms that consist out of different functors, this will fail.

The tree/1 and leaf/1 in your statement leaf(X) = tree(X) are not the predicates. What you basically here have written is:

=(leaf(X), tree(X))

So you call the (=)/2 predicate, with leaf(X) and tree(X) terms.

Now in Prolog two terms are unifiable if:

1. these are the same atom; or
2. it is a term with the same functor and arity, and the arguments are elementwise unifiable.

Since the functor leaf/1 is not equal to the functor tree/1, this means that leaf(X) and tree(X) can not be equal.

Even if we would define a predicate with the intent of checking if two predicates are semantically the same, this would fail. Here you basically aim to solve the Equivalence problem, which is undecidable. This means that one, in general, can not construct an algorithm that verifies if two Turing machines decide the same language. Prolog is a Turing complete language, we basically can translate any predicate in a Turing machine and vice versa. So that means that we can not calculate if two predicates accept the same input.