Равенство двух списков переменных

Как определить мета-логический предикат, который тестирует (таким образом, преуспевает или не удается только), если два списка уникальных переменных содержат точно такие же переменные, используя встроенные функции от текущего стандарта ISO (ISO/IEC 13211-1:1995, включая Cor.2).

Иными словами, предикат должен преуспеть, если один список уникальных переменных является перестановкой другой. По аналогии с library(ordsets), позвоните в этот мета-логический предикат varset_seteq(As, Bs).

Обратите внимание, что в отличие от ord_seteq/2 этот предикат не может быть просто As == Bs.

Ответы

Ответ 1

В предлагаемом решении используется term_variables/2, чтобы проверить, не имеет ли Bs дополнительных переменных над As и что As не имеет переменной, которая не отображается в Bs.

varset_seteq(As, Bs):-
    term_variables(As-Bs, As),
    term_variables(Bs-As, Bs).

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

 | ?- varset_seteq([A], [a]).

 A = a

 yes

Чтобы избежать этого, унификация может быть заменена тестом эквивалентности:

varset_seteq(As, Bs):-
    term_variables(As-Bs, A0),
    A0 == As,
    term_variables(Bs-As, B0),
    B0 == Bs.

Ответ 2

Если мы можем предположить, что два списка содержат уникальные переменные, то работает следующее двойное отрицание:

varset_seteq(As, Bs) :-
    \+ \+ (numbered_from(As, 1),
           sort(Bs, SBs),
           As == SBs).

numbered_from([], _).
numbered_from([X|Xs], X) :-
    X1 is X + 1,
    numbered_from(Xs, X1).

Это похоже на решение Пауло, но устраняет проблему того, что переменное упорядочение требуется только в соответствии с ISO/IEC 13211-1 в соответствии с одним выполнением sort/2.

Ответ 3

Другим решением, меньше эффективным, чем умное решение Tudor, и тем самым не, но все же стоит упомянуть здесь, поскольку я вижу, что он используется несколько раз:

varset_seteq(As, Bs) :-
    sort(As, Sa), sort(Bs, Sb), Sa == Sb.

Ответ 4

Другой подход. Если мы предоставим себя этим предикатам более высокого порядка (каждый из которых полезен сам по себе),

select_with(_, _, [], []).
select_with(P, X, [Y|Ys], Ys)     :- call(P, X, Y), !.
select_with(P, X, [Y|Ys], [Y|Ks]) :-
    select_with(P, X, Ys, Ks).

foldl(_,[],Vn,Vn).
foldl(P,[X|Xs],V0,Vn) :- 
    call(P,X,V0,V1),
    foldl_(P,Xs,V1,Vn).

то мы можем легко определить предикат, который является истинным, если каждый член один имеет равный элемент в другом (используя ==/2):

members_equal(A, B :-
    foldl(select_with(==), A, B, []).

Этот предикат может быть специализированным для заявленной цели, если мы проверим, что входящие аргументы являются varsets. Следующее - лучшее, что я смог придумать в этом направлении (но он съедает немало выводов):

is_varset([]).
is_varset([V|Vs]) :-
    var(V),
    maplist(\==(V), Vs),
    is_varset(Vs).

(По крайней мере, в SWI Prolog с использованием sort/2 выполняется меньше выводов, чем указано выше. Предположительно, это связано с тем, что сортировка выполняется на C. Кроме того, этот ответ по-прежнему не подходит к элегантности подхода term_vars/2 Такова сила "семантического восхождения":)