Переменная появление в списке переменных

Question

Рассмотрим (мета-логический) предикат var_in_vars(Var, Vars) который принимает переменную Var и список переменных Vars и преуспевает, если Var происходит в Vars. Поэтому нам не нужно гарантировать, что Var является переменной, или что Vars - это список переменных.

Что является самым компактным и каноническим способом выразить это в ISO Prolog? Вот overview of the built-ins в ISO/IEC 13211-1: 1995, включая Cor.2: 2012.

?- var_in_vars(V, [U,V,W]). 
true. 

?- var_in_vars(V, [X,Y,Z]). 
false. 

Answer 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)). 

Answer 2

Это определение проходит испытания, но ... я пропустил некоторые тонкости?

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

Answer 3

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

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

Так это полагается на точный как перемещаются переменные. И так как это well defined в стандарте мы можем рассчитывать, что они

... появляются в соответствии с их первого появления в левой направо обходе ...

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

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

Answer 4

Решение Синтез

Решение: Short

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). 

Ссылка:

Standard

---

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

Answer 5

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

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

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

Answer 6

Раствор @false может быть упрощено до:

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

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

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