Пролог удалить: не удаляет все элементы, которые объединяются с элементом

Question

У меня проблема с предикатом delete/3 SWI-Пролога.Самый простой способ - это быстрый пример:

?- delete([(1,1),(1,2),(3,2)], (1,_), List).
List = [(1,2),(3,2)].

Я бы ожидал, что (1,2) также будет удален, поскольку (1,_) объединяется с (1,2).Справка SWIPL гласит:

Удалить всех членов List1, которые одновременно объединяются с Elem и объединяют результат с List2.

Почему это так и как я могу удалить все, что объединено с (1,_)?

Answer 1

"Удалить всех членов List1, которые одновременно объединены с Elem и объединить результат с List2."

(1, X) сначала объединяется с (1,1). следовательно, X объединяется с 1 и не может быть объединено с 2 для удаления (1,2). проблема не в том, что он не удаляет всех членов; это то, что он не объединяется одновременно с (1,2) и (1,1) (попробуйте удалить ([(1,1), (1,2), (1,1), (3,2)], (1, _), список).

кстати, согласно руководству по swi-прологу :

удалить (? List1,? Elem,? List2)
Истинно, когда Lis1 при всех удаленных элементах приводит к List2.

также, delete / 3 устарела:

Слишком много способов удалить элементы из списка, чтобы оправдать имя. Подумайте о соответствии (= vs. ==), сначала удалите все, будьте детерминированными или нет.

Так что самый простой способ - написать свой собственный предикат. Что-то вроде:

my_delete(Pattern,[Pattern|T],TD):-
   my_delete(Pattern,T,TD).
my_delete(Pattern,[H|T],[H|TD]):-
   my_delete(Pattern,T,TD).

возможно

проверка исключить / 3, включить / 3, раздел / 4

Answer 2

Использовать мета-предикат texclude/3 в сочетании с предикатом равенства термина reified (=)/3!

Сначала мы попробуем использовать (=)/3 напрямую ...

?- texclude(=((1,V)), [(1,1),(1,2),(3,2)], KVs).
KVs = [      (1,2),(3,2)],     V=1            ;
KVs = [(1,1),      (3,2)],               V=2  ;
KVs = [(1,1),(1,2),(3,2)], dif(V,1), dif(V,2).

Не совсем! Для наших следующих попыток мы будем использовать лямбда-выражения .

:- use_module(library(lambda)).

Давайте запросить --- один раз с texclude/3, один раз с tinclude/3 и один раз с tpartition/4:

?- texclude(  \ (K,_)^(K=1), [(1,1),(1,2),(3,2)], Fs).
Fs = [(3,2)].                                     % succeeds deterministically

?- tinclude(  \ (K,_)^(K=1), [(1,1),(1,2),(3,2)], Ts).
Ts = [(1,1),(1,2)].                               % succeeds deterministically

?- tpartition(\ (K,_)^(K=1), [(1,1),(1,2),(3,2)], Ts,Fs).
Ts = [(1,1),(1,2)], Fs = [(3,2)].                 % succeeds deterministically

Хорошо! Получим ли мы те же решения, если элементы списка связаны после texclude/3 вызова?

?- texclude(\ (K,_)^(K=1), [A,B,C], Fs), A = (1,1), B = (1,2), C = (3,2).
A = (1,1), B = (1,2), C = (3,2), Fs = [(3,2)] ;   % succeeds with choice point
false.

Да! Наконец, рассмотрим следующий довольно общий запрос:

?- texclude(\ (K,_)^(K=1), [A,B], Fs).
Fs = [   ], A = (  1,_A1), B = (  1,_B1)                         ;
Fs = [  B], A = (  1,_A1), B = (_B0,_B1),             dif(_B0,1) ;
Fs = [A  ], A = (_A0,_A1), B = (  1,_B1), dif(_A0,1)             ;
Fs = [A,B], A = (_A0,_A1), B = (_B0,_B1), dif(_A0,1), dif(_B0,1).

---

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

?- texclude(\ (K,_)^(K=1), [x,_], _).
<b>false</b>.

Answer 3

Этот ответ пытается обобщить идею, представленную в предыдущем ответе .

Давайте определим конкретизированный вариант subsumes_term/2:

list_nonvardisj([A],C) :- 
   !, 
   C = nonvar(A).
list_nonvardisj([A|As],(nonvar(A);C)) :-
   list_nonvardisj(As,C).

subsumes_term_t(General,Specific,Truth) :-
   subsumes_term(General,Specific),
   !,
   term_variables(General,G_vars),
   free4evrs(G_vars),
   Truth = true.
subsumes_term_t(General,Specific,Truth) :-
   Specific \= General,
   !,
   Truth = false.
subsumes_term_t(General,Specific,Truth) :-
   term_variables(Specific,S_vars),
   (  S_vars = [V]
   -> freeze(V,subsumes_term_t(General,Specific,Truth))
   ;  S_vars = [_|_]
   -> list_nonvardisj(S_vars,S_wakeup),
      when(S_wakeup,subsumes_term_t(General,Specific,Truth))
   ;  throw(error(instantiation_error, subsumes_term_t/3))
   ),
   (  Truth = true
   ;  Truth = false
   ).

Приведенное выше определениеРеализованный предикат subsumes_term_t/3 использует free4evrs/1, чтобы гарантировать, что "общий" термин, переданный в subsumes_term/2, больше не создается.

Для SICStus Prolog мы можем определить его следующим образом:

:- module(free4evr,[free4evr/1,free4evrs/1]).

:- use_module(library(atts)).

:- attribute nvrb/0.                       % nvrb ... NeVeR Bound

verify_attributes(V,_,Goals) :-
   get_atts(V,nvrb), 
   !,
   Goals = [throw(error(uninstantiation_error(V),free4evr/1))].
verify_attributes(_,_,[]).

attribute_goal(V,free4evr(V)) :-
   get_atts(V,nvrb).

free4evr(V) :-
   nonvar(V),
   !,
   throw(error(uninstantiation_error(V),free4evr/1)).
free4evr(V) :-
   (  get_atts(V,nvrb)
   -> true
   ;  put_atts(Fresh,nvrb),
      V = Fresh
   ).

free4evrs([]).
free4evrs([V|Vs]) :-
   free4evr(V),
   free4evrs(Vs).

Давайте использовать subsumes_term_t/3 для использования!

?- texclude(subsumes_term_t(1-X), [A,B,C], Fs), A = 1-1, B = 1-2, C = 3-2.
A = 1-1, B = 1-2, C = 3-2, Fs = [C], free4evr(X) ? ;   % succeeds with choice-point
no

?- texclude(subsumes_term_t(1-X), [x,1-Y,2-3], Fs).
Fs = [x,2-3], free4evr(X) ? ;
no

Что произойдет, если мы создадим переменную X в запросе выше через некоторое время после вызова texclude/3?

?- texclude(subsumes_term_t(1-X), [x,1-Y,2-3], Fs), X=something.
! error(uninstantiation_error(something),free4evr/1)