Как анонимные переменные интерпретируются в Прологе?

Question

Быстрый и простой вопрос о том, какую роль играют анонимные переменные в разрешении запроса Пролог с учетом набора правил программы. Итак, насколько я понимаю, как работает простейшая форма разрешения SLD, дерево SLD строится путем взятия некоторого термина из набора терминов цели (на основе правила выбора, например, FIRST) и прохождения всех правил программы, чтобы увидеть, какие Левая часть правила (так сказать, последовательная) может быть объединена с имеющимся термином. Способ объединения двух заданных терминов состоит в том, чтобы взять набор разностей из двух терминов и посмотреть, могут ли переменные заменять термины таким образом, что разность исчезает, вы делаете это путем последовательного взятия самой левой разницы и проверки, если из двух наборов составляющая разницу, одна - это переменная, не появляющаяся в другой и составляющая вашу текущую подстановку с одной, отображающей переменную в термин (начиная с пустой или тождественной подстановки).

Теперь, когда анонимные переменные (_) Вступая в игру, я подозреваю, что хитрость в том, чтобы сделать это правильно и эффективно, заключается в изменении способа определения крайней левой разницы между двумя терминами, чтобы игнорировать пару терминов, когда один из них является анонимной переменной. Очевидный правильный способ сделать это - переименовать каждый экземпляр _ в цели и программе установить новое имя переменной и решить, используя их.

Как это на самом деле делается? Достаточно ли моей идеи или есть что-то большее? (Кроме того, я был бы очень признателен, если бы что-то не хватало, как я понимаю, работает разрешение SLD, исключая отрицание, вызов, capsuling, предикаты арифметики c и более сложные вещи.)

Answer 1

Анонимные переменные Prolog не играют роли в разрешении SLD или в объединении терминов, но играют практическую роль в коде Prolog и запросах Prolog. Фундаментальный аспект анонимных переменных заключается в том, что каждое вхождение анонимной переменной является отдельной переменной. Рассмотрим следующий запрос:

| ?- a(_, _) = a(1, 2).

yes

Объединение не удалось бы, если бы две анонимные переменные были одной и той же переменной. Теперь рассмотрим запрос:

| ?- a(X, _) = a(1, 2).

X = 1
yes

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

Анонимные переменные также упрощают написание определений предикатов, где они аналогично действуют как переменные "не заботятся". Рассмотрим в качестве примера обычное определение предиката member/2:

member(Element, [Element| _]).
member(Element, [_| List]) :-
    member(Element, List).

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

Обновление

Обратите внимание, что все различные переменные в запросе получают уникальные внутренние ссылки на переменные, не путать их с именами переменных, введенными пользователем. Имена переменных используются только интерпретатором верхнего уровня для сообщения о привязках для успешных запросов. Механизм вывода, используемый для доказательства запроса, использует переменные (внутренние) ссылки. Следующий запрос, использующий предикат стандарта ISO Prolog read_term/2 со стандартными опциями, может помочь:

| ?- read_term(Term, [variable_names(Names), variables(Variables)]).
a(X, _, Y, _).

Names = ['X'=A,'Y'=B]
Term = a(A,C,B,D)
Variables = [A,C,B,D]

yes

В термине read есть четыре разные переменные, но только две из них имеют (предоставленные пользователем) имена.

Answer 2

Это комментарий в ответе, поскольку комментарий не может отформатировать его при необходимости.

Использование SWI-Prolog

?- trace,(_=_).
   Call: (11) _1834=_1836 ? creep
   Exit: (11) _1834=_1834 ? creep
true.

Каждая анонимная переменная создается как отдельная переменная. Когда происходит объединение, одна переменная объединяется с другой переменной.