Вселенная Хербранда и Модель Наименьшего Хербранда

Я прочитал вопрос, заданный во вселенной Herbrand, Herbrand Базовая модель и модель Хербранда бинарного дерева (пролог) и данные ответы, но у меня немного другой вопрос, больше похожий на подтверждение, и, надеюсь, мое замешательство прояснится.

Пусть P — программа такая, что у нас есть следующие факты и правило:

q(a, g(b)).
q(b, g(b)).
q(X, g(X)) :- q(X, g(g(g(X)))).

Из приведенной выше программы Вселенная Хербранда

Up = {a, b, g(a), g(b), q(a, g(a)), q(a, g(b)), q(b, g(a)), q(b, g(b)), g(g(a)), g(g(b))...e.t.c}

База Herbrand:

Bp = {q(s, t) | s, t E Up}
  • Теперь перейдем к моему вопросу (простите меня за мое невежество), я включил q (a, g (a)) в качестве элемента в мою вселенную Гербранда, но на самом деле он утверждает q (a, g (b)). Означает ли это, что q(a, g(a)) там не предполагается?
  • Кроме того, поскольку модели Хербранда являются подмножеством базы Гербранда, как мне определить наименьшую модель Хербранда по индукции?

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


prolog logic-programming
person Plaix    schedule 27.01.2014    source источник

Ответы (2)


arrow_upward
8
arrow_downward

Имея факт q(a,g(b)), вы не можете заключить, присутствует ли q(a,g(a)) в модели. Сначала вам нужно будет сгенерировать модель.

Для определения модели начните с фактов {q(a,g(b)), q(b,g(b))}, а теперь попробуйте применить свои правила для ее расширения. Однако в вашем случае нет возможности сопоставить правую часть правила q(X,g(X)) :- q(X,g(g(g(X)))). с приведенными выше фактами. Таким образом, вы сделали.

Теперь представьте правило

q(a,g(Y)) :- q(b,Y).

Это правило можно использовать для расширения нашего множества. На самом деле экземпляр

q(a,g(g(b))) :- q(b,g(b)).

используется: Если присутствует q(b,g(b)), заключить q(a,g(g(b))). Обратите внимание, что мы используем здесь правило справа налево. Итак, мы получаем

{q(a,g(b)), q(b,g(b)), q(a,g(g(b)))}

тем самым достигнув фиксированной точки.

Теперь возьмем в качестве другого примера предложенное вами правило

q(X, g(g(g(X)))) :- q(X, g(X)).

Что позволяет (я больше не буду показывать конкретизированное правило) генерировать за один шаг:

{q(a,g(b)), q(b,g(b)), q(a,g(g(g(b)))), q(b, g(g(g(b))))}

Но это еще не конец, так как, опять же, правило можно применить, чтобы производить еще больше! По сути, теперь у вас есть бесконечная модель!

{g(a,gn+1(b)), g(b, gn+1(b))}

Это чтение справа налево часто очень полезно, когда вы пытаетесь понять рекурсивные правила в Прологе. Чтение сверху вниз (слева направо) часто довольно сложно, в частности, поскольку приходится учитывать возвраты и общую унификацию.

person false    schedule 27.01.2014
comment
Спасибо за объяснение, я думаю, что понял. Какое правило меняется, например, q(X, g(g(g(X)))) :- q(X, g(X))).? Также верна ли моя Вселенная Хербранда? - person Plaix; 28.01.2014
comment
@Plaix: Вселенная Хербранда — это все возможные комбинации. - person false; 28.01.2014

arrow_upward
3
arrow_downward

Относительно вашего вопроса:

«Кроме того, поскольку модели Хербранда являются подмножеством базы Гербранда, как мне определить наименьшую модель Хербранда по индукции?»

Если у вас есть набор P предложений рога, определенная программа, вы можете определить оператор программы:

T_P(M) := { H S | S is ground substitution, (H :- B) in P and B S in M }

Наименьшая модель:

inf(P) := intersect { M | M |= P }

Обратите внимание, что не все модели конкретной программы являются фиксированными точками оператора программы. Например, полная модель Гербранда всегда является моделью программы P, которая показывает, что определенные программы всегда непротиворечивы, но не обязательно является фиксированной точкой.

С другой стороны, каждая неподвижная точка программного оператора является моделью определенной программы. А именно, если у вас есть T_P(M) = M, то можно сделать вывод, что M |= P. Так что после некоторых дальнейших математических рассуждений (*) можно обнаружить, что наименьшая фиксированная точка также является наименьшей моделью:

lfp(T_P) = inf(P)

Но нам потребуются некоторые дополнительные соображения, чтобы мы могли сказать, что можем определить наименьшую модель с помощью своего рода вычислений. А именно легко заметить, что программный оператор непрерывен, т. е. сохраняет бесконечные объединения цепей, так как роговые предложения не имеют в своем теле кванторов forall:

union_i T_P(M_i) = T_P(union_i M_i)

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

union_i T_P^i({}) = lpf(T_P)

Пока

(*) Скорее всего, в этой книге вы найдете дополнительные подсказки по поводу необходимых математических рассуждений, но, к сожалению, я не могу вспомнить, какие разделы относятся к делу:
Основы логического программирования, Джон Уайли Ллойд, 1984
http://www.amazon.de/Foundations-Programming-Computation-Artificial-Intelligence/dp/3642968287

person Mostowski Collapse    schedule 02.02.2014