- •Лекция №1 Логическая программа: основные конструкции
- •Лекция №2 Программирование баз данных
- •Структурированные и абстрактные данные
- •Логические программы и модель реляционной базы данных
- •Лекция №3 Рекурсивное программирование
- •Построение рекурсивных программ
- •Бинарные деревья
- •Работа с символьными выражениями
- •Лекция №4 Вычислительная модель логических программ
- •Абстрактный интерпретатор логических программ
- •Лекция №5 Теория логических программ Операционная и декларативная семантика. Интерпретация
- •Корректность программы
- •Лекция №6 Анализ структуры термов
- •Типовые предикаты
- •Составные термы
- •Лекция №7 Металогические предикаты
- •Типовые металогические предикаты
- •Сравнение неосновных термов
- •Использование переменных в качестве объектов
- •Доступность метапеременных
- •Лекция №8 Внелогические предикаты
- •Лекция №9 Недетерминированное программирование
- •Недетерминизм с произвольным выбором альтернативы и недетерминизм с неизвестным выбором альтернативы
- •Лекция №10 Неполные структуры данных
- •Лекция №11 Программирование второго порядка
- •Лекция №12 Методы поиска
- •Лекция №13 Нечеткая логика. Обработка нечетких данных
- •Лекция №14 Constraint-пролог: операционная семантика Программирование в ограничениях
- •Лекция №15 Применение логического программирования в задачах искусственного интеллекта. Тест Тьюринга.
- •Лекция №16 Введение в функциональное программирование
- •Лекция №17 Рекурсивные функции и лямбда-исчисление а.Черча
- •Лекция №18 Функциональные языки программирования Свойства функциональных языков
- •Лекция №19 Программирование в функциональных обозначениях Структуры данных и базисные операции
- •Типы в функциональных языках
- •Лекция №20 Представление и интерпретация функциональных программ Программная реализация
Лекция №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, отображающая интерпретации в интерпретации и определенная следующим образом:
TP(I) = {А|А принадлежит В(Р), А В, В,...,В, п0 – основной пример предложения в Р, В, В,...,В, принадлежат I}.
Данное отображение монотонно, так как если интерпретация I содержится в интерпретации J, то ТP (I) содержится в ТP (J).
Это отображение позволяет описать модели иным способом. Интерпретация I является моделью в том и только в том случае, если Т (I ) содержится в I.
Данное отношение является не только монотонным, но и непрерывным (понятие непрерывности здесь не определяется). Эти два свойства гарантируют, что для каждой логической программы Р отображение TPимеет наименьшую неподвижную точку, которая и является значением, определяемым денотационной семантикой программыР.
К счастью, все различные определения семантики в действительности описывают один и тот же объект. Показано, что операционная, денотационная и декларативная семантики совпадают. Это позволяет нам определить значение логической программы как минимальную модель программы.