Экзистенциальный классификатор в прологе, используя setof / bagof

Question

У меня был быстрый вопрос повторно. экзистенциальный классификатор, использующий setof в прологе (то есть ^).

используя SICStus, кажется, что (несмотря на то, что утверждают многие веб-сайты), S действительно выглядит количественно в приведенном ниже коде (используя стандарт болота, мать / потомок фактов, которые я здесь не включил):

child(M,F,C) :- setof(X,(mother(S,X)),C).

я проверяю объединение используя:

child(M,F,C) :- setof(X-S,(mother(S,X)),C).

поэтому следующий код с экзистенциальным оператором, похоже, не имеет значения:

child(M,F,C) :- setof(X,S^(mother(S,X)),C).

Есть идеи, почему это? В какой ситуации вам понадобится объединитель?

Спасибо!

Answer 1

Хорошо, я не уверен, что могу объяснить это отлично, но позвольте мне попробовать.

Это связано с тем, что вы запрашиваете 2-арное отношение, mother/2, В этом случае с помощью X-S так как шаблон оказывает аналогичное влияние на набор результатов C как используя S^ перед целью. В X-S вы используете обе переменные в шаблоне, и поэтому каждое возможное связывание X и S включено в C. Вы получаете тот же эффект, используя S^ перед целью, как это говорит "игнорировать привязки S при построении результата".

Но разница между ними становится более ясной, когда вы запрашиваете 3-арное отношение. Руководство SWI имеет этот пример:

foo(a, b, c).
foo(a, b, d).
foo(b, c, e).
foo(b, c, f).
foo(c, c, g).

Теперь выполните аналогичные запросы, как в вашем примере

setof(X-Z, foo(X,Y,Z), C).

а также

setof(Z, X^foo(X,Y,Z), C).

и вы получите разные результаты.

Это не просто проверка объединения, X-Z эффективно меняет ваш набор результатов.

Надеюсь, это поможет.

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

?- setof(X-Z, foo(X,Y,Z), C).   
Y = b
C = [a-c, a-d] ;
Y = c
C = [b-e, b-f, c-g] ;
No

Второй дает:

?- setof(Z, X^foo(X,Y,Z), C).
Y = b
C = [c, d] ;
Y = c
C = [e, f, g] ;
No