Ответ 1

Одна возможность:

var_in_vars(V, Vs) :- \+ unify_with_occurs_check(V, Vs).

и короче:

var_in_vars(V, Vs) :- \+ subsumes_term(V, Vs).

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

В других обстоятельствах вы, скорее всего, больше выиграете от определения типа:

var_in_vars(V, Vs) :-
        must_be(list, Vs),
        once((member(X, Vs), V == X)).

Ответ 2

это определение проходит тесты, но... я скучаю по некоторой тонкости?

var_in_vars(V, [H|_]) :- V == H, !.
var_in_vars(V, [_|T]) :- var_in_vars(V, T).

Ответ 3

И вот еще один, хотя и немного сложнее:

var_in_vars(V, Vs) :-
   term_variables(Vs+V, Ws),
   Ws == Vs.

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

... появляются в соответствии с их первым вхождением в обход слева направо...

Недостатком этого определения является то, что он имеет минимальную стоимость, пропорциональную длине Vs. Но так как внутренний обход часто довольно эффективно реализуется, это не такая проблема.

У него есть одно большое преимущество: ему удается только, если Vs - список переменных.

Ответ 4

Альтернативное решение:

var_in_vars(V, Vs) :-
    \+ (V = Vs, acyclic_term(Vs)).

Но решения @mat лучше и элегантнее, а решение от @CapelliC было долгое время самым портативным (предикат subsumes_term/2 был стандартизирован недавно, а не все системы предоставили предикат unify_with_occurs_check/2),.

Ответ 5

Решение @false можно упростить до:

var_in_vars(V, Vs) :-
    term_variables(Vs+V, Vs).

Когда V является членом списка Vs, второй аргумент возвращает Vs (из-за обхода "Vs+V" слева направо). Если V не является членом Vs, второй аргумент возвращает список, содержащий еще один элемент, чем Vs и, следовательно, не может объединяться с ним. Несмотря на наличие неявного объединения во втором аргументе, в любом случае существует опасность создания циклического термина. То есть унификация, являющаяся STO, не является проблемой в этом упрощенном решении.

Но упрощение стоит it w.r.t. представление? Использование равенства (==)/2 имеет потенциал неудачи раньше и, таким образом, делает исходное решение быстрее.

Ответ 6

Синтез решения

Решение: Короткая

var_in_vars(V, Vs) :- \+ subsumes_term(V, Vs).

Альтернатива 1: Простой

var_in_vars(V, Vs) :- \+ unify_with_occurs_check(V, Vs).

Альтернатива 2: В зависимости от обстоятельств это может быть более подходящим

var_in_vars(V, Vs) :-
        must_be(list, Vs),
        once((member(X, Vs), V == X)).

Альтернатива 3: Более сложная

var_in_vars(V, Vs) :-
   term_variables(Vs+V, Ws),
   Ws == Vs.

Альтернатива 4: Другая возможность

var_in_vars(V, [H|_]) :- V == H, !.
var_in_vars(V, [_|T]) :- var_in_vars(V, T).

Ссылки:

Стандарт

Примечание: Контекст вопроса, который представляет собой специфическую проблему компактности, включающую экспрессивность предикатов ISO при данных обстоятельствах.