Пролог ... определить предикат, который проверяет, являются ли оба аргумента / указывают на один и тот же атом

Question

У меня есть предикат пролога, который принимает два параметра (оба обозначены здесь X, поскольку они должны быть одинаковыми) и сравнивает их, чтобы увидеть, оценивают ли они один и тот же атом.Это намерение.Однако предикат неожиданно возвращает false, когда оба аргумента являются переменными.

Я пытаюсь определить понятие выражения в логике предложения / высказывании высказываний, находящемся в «нормальной форме импликации» в Прологе.Здесь подразумевается нормальная форма импликации, означающая, что все связки заменены на -> и falsum.

. В качестве базового случая я хочу сказать, что выражение, состоящее полностью из атома, уже находится в нормальной форме с самим собой.

Вот как я пытаюсь это выразить.Я повторяю имя параметра вместо того, чтобы делать какую-то проверку одинаковости между параметрами.

% foo.P
implication_normal(X, X) :- atom(X).

Это неполное, но все еще полезное определение предназначено для того, чтобы зафиксировать тот факт, что implication_normal(x, x) верноно implication_normal(x, y) неверно.

В некотором смысле это работает:

$ swipl -s foo.P

?- implication_normal(x, x).
true.

?- implication_normal(x, y).
false.

?- implication_normal(1, 1).
false.

Это неправильно с переменными (это должно быть перечисление пар "контекстов связывания", где X и Z указывают на один и тот же атом).

?- implication_normal(X, Z).
false.

Он также просто возвращает false, если вы дважды передаете ему одну и ту же переменную.

?- implication_normal(X, X).
false.

для какого-то странногопричина, поведение правильное, если вы задаете ему переменную и один атом (и вы получаете ошибку с целым числом).

?- implication_normal(X, z).
X = z.

?- implication_normal(X, 1).
false.

и аналогично, если переменная является второй.

?- implication_normal(z, X).
X = z.

?- implication_normal(1, X).
false.

Как изменить определение implication_normal, чтобы оно перечислялось во всех случаях, когда предоставляются переменные?

Answer 1

Стандартный предикат atom/1 является предикатом проверки типа .Он не перечисляет атомы.Он просто детерминистически проверяет, является ли его аргумент атомом.Более того, ваше определение предиката implication_normal /2 пытается объединить его два аргумента и, если объединение успешно, вызывает atom/1 с результирующим термином.Вот почему вызов, такой как implication_normal(X, z), завершается успешно: X объединяется с z, а atom(z) имеет значение true.

Обратите внимание, что некоторые системы Prolog предоставляют current_atom/1, который перечисляет атомы.В этих системах вы могли бы написать вместо:

implication_normal(X, X) :- current_atom(X).

Некоторые примеры вызовов с использованием SWI-Prolog:

?- implication_normal(X, Z).
X = Z, Z = '' ;
X = Z, Z = abort ;
X = Z, Z = '$aborted'
...

?- implication_normal(X, X).
X = '' ;
X = abort ;
X = '$aborted' ;
...

?- implication_normal(X, z).
X = z.

?- implication_normal(X, 1).
false.