Почему это выражение не унифицировано?

Question

Я определил следующую базу знаний:

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

и ожидал запроса:

leaf(X) = tree(X).

вернет true ., потому что любой лист должен по определению быть деревом.

К сожалению, активация трассировки не дает никаких полезных результатов.Вот ссылка на этот минимальный пример, если вы хотите поиграть с ним.

Answer 1

Краткий ответ : вы здесь проверяете, можно ли объединить термин leaf(X) с tree(X).Так как это термины, состоящие из разных функторов, произойдет сбой.

tree/1 и leaf/1 в вашем утверждении leaf(X) = tree(X) являются , а не предикатами.В основном вы здесь написали:

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

Итак, вы называете предикат (=)/2 с leaf(X) и tree(X) терминами.

Теперь в Прологе два термина unifiable , если:

1. это один и тот же атом;или
2. это термин с тем же функтором и арностью, а аргументы элементарно не различимы.

Поскольку функтор leaf/1 не равен функтору tree/1,это означает, что leaf(X) и tree(X) не могут быть равны.

Даже если бы мы определили предикат с целью проверки, являются ли два предиката семантически одинаковыми, это не получится,Здесь вы в основном стремитесь решить проблему эквивалентности , которая неразрешима .Это означает, что в общем случае нельзя создать алгоритм, который проверяет, принимают ли две машины Тьюринга один и тот же язык.Пролог - это полный язык Тьюринга , мы в основном можем перевести любой предикат в машине Тьюринга и наоборот.Таким образом, это означает, что мы не можем вычислить, если два предиката принимают один и тот же вход.