Избыточные ответы овеществленного варианта предиката append/3

Я хотел предложить логически чистое решение для некоторых другая недавняя проблема на этом форуме.

Для начала я реализовал материализованный вариант append/3 и назвал его appendR/4. Он основан на предикатах if_/3 и (=)/3, реализованных @false в Prolog union для AUBUC:

appendR([],Ys,Zs,T) :- 
    =(Ys,Zs,T).
appendR([X|Xs],Ys,ZZs,T) :-
    if_([X|Zs] = ZZs, appendR(Xs,Ys,Zs,T), T = false).

Реализация в основном работает, о чем свидетельствуют следующие запросы:

?- appendR([1,2],Ys,[2,3,4],T).
T = false ? ;
no

?- appendR([1,2],[3,4],Xs, T).
T = true,  Xs = [1,2,3,4],                       ? ;
T = false, Xs = [1,2|_A],  prolog:dif([3,4],_A)  ? ;
T = false, Xs = [1|_A],    prolog:dif([2|_B],_A) ? ;
T = false,                 prolog:dif([1|_A],Xs) ? ;
no

Пока все хорошо... А вот и сложная часть:

?- appendR([1,2],Ys,[1,2,3,4],T).
T = true,  Ys = [3,4]                   ? ;
T = false, prolog:dif(Ys,[3,4])         ? ;
T = false, prolog:dif([2|_A],[2,3,4])   ? ;
T = false, prolog:dif([1|_A],[1,2,3,4]) ? ;
no

Я хочу получить первые два ответа, но не последние два. Помогите, пожалуйста!


list prolog logical-purity reification
person repeat    schedule 04.04.2015    source источник
comment
Я до сих пор не знаю хорошего ответа, но пока факт append([], Xs, Xs). является намеренным обобщением. Я не уверен, что имеет смысл материализовывать само обобщение.   -  person false    schedule 25.10.2015

Ответы (2)


arrow_upward
1
arrow_downward

Я также закодировал альтернативный вариант appendRR/4:

appendRR([],Ys,Zs, T) :- 
    =(Ys,Zs,T).
appendRR([_|_],_,[], false).
appendRR([X|Xs],Ys,[Z|Zs], T) :-
    if_(X=Z, appendRR(Xs,Ys,Zs,T), T = false).

Он не дает лишних ответов:

?- appendRR([1,2],Ys,[1,2,3,4],T).
T = true,  Ys = [3,4]           ? ;
T = false, prolog:dif(Ys,[3,4]) ? ;
no

Однако цель appendRR([1,2],_,foo,T) не удается. Я бы предпочел получить ответ T = false. Меня это немножко беспокоит.

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

person repeat    schedule 07.04.2015

arrow_upward
1
arrow_downward

Следующая попытка: append_t/4. Он должен сочетать в себе «лучшее» из appendR/4 и appendRR/4.

Во-первых, мы определяем материализованный предикат проверки непустого списка cons_t/2:

cons_t(V,T) :- 
   (  nonvar(V)                         % we can decide right now!
   -> (  V = [_|_]
      -> T = true
      ;  T = false
      )
   ;  V = [_|_],          T = true      % go nondet!
   ;  freeze(V,V\=[_|_]), T = false
   ).

Основываясь на cons_t/2, (=)/3 и if_/3, мы определяем append_t/4 следующим образом:

append_t([],Bs,Cs,T) :-
   =(Bs,Cs,T).
append_t([A|As],Bs,Cs0,T) :-
   if_(cons_t(Cs0),
       (Cs0=[C|Cs], if_(A=C, append_t(As,Bs,Cs,T), T=false)),
       T=false).

Давайте зададим вопросы и сравним полученные ответы! Плохие результаты выделяются (выделены жирным шрифтом).

  1. ?- appendR([1,2],[3,4],Cs,T).
  T = true ,     Cs=[1,2,3,4]
; T = false,     Cs=[1,2|_X] , dif(_X,[3,4])
; T = false,     Cs=[1|_X]   , dif(_X,[2|_])
; T = false, dif(Cs,[1|_]).

?- appendRR([1,2],[3,4],Cs,T).
  T = false, Cs = []
; T = false, Cs = [1]
; T = true , Cs = [1,2,3,4]
; T = false, Cs = [1,2|_X] , dif(_X,[3,4])
; T = false, Cs = [1,_X|_] , dif(_X,2)
; T = false, Cs = [_X|_]   , dif(_X,1).

?- append_t([1,2],[3,4],Cs,T).
  T = true , Cs = [1,2,3,4]
; T = false, Cs = [1,2|_X] , dif(_X,[3,4])
; T = false, Cs = [1,_X|_] , dif(_X,2)
; T = false, Cs = [1|_X]   , freeze(_X,_X\=[_|_])
; T = false, Cs = [_X|_]   , dif(_X,1)
; T = false, freeze(Cs,Cs\=[_|_]).

  2. ?- appendR([1,2],Bs,[1,2,3,4],T).
  T = true ,     Bs=[3,4]
; T = false, dif(Bs,[3,4])
; T = false
; T = false.

?- appendRR([1,2],Bs,[1,2,3,4],T).
  T = true ,     Bs=[3,4]
; T = false, dif(Bs,[3,4]).

?- append_t([1,2],Bs,[1,2,3,4],T).
  T = true ,     Bs=[3,4]
; T = false, dif(Bs,[3,4]).

  3. ?- appendR([1,2],_,[2,3,4],T).
T = false.

?- appendRR([1,2],_,[2,3,4],T).
T = false.

?- append_t([1,2],_,[2,3,4],T).
T = false.

  4. ?- appendR([1,2],_,non_list,T).
T = false.

?- appendRR([1,2],_,non_list,T).
false.

?- append_t([1,2],_,non_list,T).
T = false.

Вывод: appendR/4 и appendRR/4 терпят неудачу в некоторых тестовых примерах, append_t/4 нет.

person repeat    schedule 24.10.2015
comment
Случаи с non_list не являются ни истинными, ни ложными: они выходят за рамки! Подумайте о append_t(non_list, _, _, T), где все ваши версии терпят неудачу. То же самое относится и к другим аргументам. - person false; 25.10.2015
comment
Верно! OTOH, общее определение append/3 асимметрично относительно. обобщение аргументов, тестирование типов, индексирование и (возможно) многое другое. - person repeat; 25.10.2015
comment
Обобщение факта append/3 здесь для того, чтобы облегчить более эффективное выполнение. Ничего больше. - person false; 25.10.2015