Операционная и декларативная семантика. Интерпретация

Теория логических программ

Лекция №5

Семантика сопоставляет значение с программой. Обсуждение семантики позволит нам более формально описывать отношение, вычисляемое программой. Ранее значение программы неформально определялось как множество основных примеров, выводимых из Р путем конечного числа применения обобщенного правила modus ponens. Используем более формальный подход.

Операционная семантика позволяет процедурно описывать значение программы. Операционное значение логической программы Р –- это множество основных целей, являющихся примерами вопросов, которые программа Р решает с помощью абстрактного интерпретатора.

Декларативная семантика логических программ основана на стандартной теоретико-модельной семантике логики первого порядка. Для ее описания потребуется некоторая новая терминология.

Пусть P – логическая программа. Универсуум Эрбрана программы P, обозначаемый U (P) – это множество всех основных термов, которые могут быть построены из констант и функциональных символов, входящих в Р. Пусть, например, Р – программа 3.1, определяющая натуральные числа:

natural_number(0).

natural_number (s(X))¬ natural number (X).

В программе имеется один символ константы – 0 и один унарный функциональный символ – s. Универсум Эрбрана U (Р) данной программы есть {0, s (0),(s(s0)),...}. В общем случае универсуум Эрбрана бесконечен, если в программу входит хотя бы один функциональный символ. Если в программу не входят символы констант, то выбирается произвольным образом одна константа.

Базис Эрбрана, обозначаемый В (Р), есть множество всех основных целей, которые можно построить с помощью предикатов программы Р и термов универсуума Эрбрана. Если универсуум Эрбрана бесконечен, то бесконечен и базис Эрбрана. В нашем примере программа содержит один предикат – natural_number. Базис Эрбрана – {nalural_number (0), natural_number (s (0)),...}.

Интерпретация логической программы – это некоторое подмножество базиса Эрбрана. Интерпретация сопоставляет истинность и ложность элементам базиса Эрбрана.Цель, принадлежащая базису Эрбрана, является истинной относительно данной интерпретации, если цель входит в данную интерпретацию, в противном случае цель является ложной.

Интерпретация I является моделью логической программы, если каждый основной пример А ¬ В,...,B правила программы удовлетворяет следующему свойству: если В,...,B принадлежат I, то и А принадлежит I. Интуитивно ясно, что моделями являются интерпретации, согласованные с декларативным пониманием предложений программы.

В нашем примере цель natural_number(0) должна входить в каждую модель; кроме того, если natural_number(X) принадлежит модели, то и natural_number(s(Х)) принадлежит модели. Таким образом, любая модель программы 3.1 содержит весь базис Эрбрана.

Легко заметить, что пересечение двух моделей логической программы Р также является моделью. Это свойство позволяет определить пересечение всех моделей. Модель, полученная пересечением всех моделей, называется минимальной моделью и обозначается М(Р). Минимальная модель и есть декларативное значение программы.

Декларативное значение программы для natural_number, т.е. ее минимальная модель, совпадает с полным базисом Эрбрана – {natural_number (0),natural_number,(s (0)), natural_number (s (s (0))),...}.

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

Для заданной логической программы Р имеется естественная функция Т_P, отображающая интерпретации в интерпретации и определенная следующим образом:

T_P (I) = { А | А принадлежит В(Р), А ¬ В, В,...,В, п³0 – основной пример предложения в Р, В, В,...,В, принадлежат I }.

Данное отображение монотонно, так как если интерпретация I содержится в интерпретации J, то Т_P (I) содержится в Т_P (J).

Это отображение позволяет описать модели иным способом. Интерпретация I является моделью втом и только в том случае, если Т (I) содержится в I.

Данное отношение является не только монотонным, но и непрерывным (понятие непрерывности здесь не определяется). Эти два свойства гарантируют, что для каждой логической программы Р отображение T_P имеет наименьшую неподвижную точку, которая и является значением, определяемым денотационной семантикой программы Р.

К счастью, все различные определения семантики в действительности описывают один и тот же объект. Показано, что операционная, денотационная и декларативная семантики совпадают. Это позволяет нам определить значение логической программы как минимальную модель программы.

Дата добавления: 2014-01-07