Декларативная и процедурная семантика программ на языке Пролог.

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

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

Декларативная семантика программы определяет, что истинно и при каких значениях переменных. С точки зрения декларативной семантики, утверждения программы являются формулами исчисления предикатов 1-го порядка.

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

Процедурная семантика Пролог¾программы состоит в интерпретации входящих в программу утверждений с точки зрения процесса установления истинностных значений задаваемых в вопросе утверждений. Процедурная семантика ¾ это процедура вычисления списка целей на основе заданной декларативной программы. Назовем эту процедуру именем «Вычислить».

Входными данными процедуры «Вычислить» являются логическая программа и список целей (вопрос).

Выходные данные процедуры «Вычислить» ¾ признак Успех/неуспех и конкретизация переменных.

Процедурная семантика языка Пролог определяет встроенные в Пролог¾систему механизмы логического вывода. Рассмотрим простейшие механизмы логического вывода.

v Факты в программе не содержат переменных, а
вопрос ¾ простой и основной. В этом случае используется правило совпадения: вопрос выводим из программы, если в программе имеется совпадающий с вопросом факт.

v Факты в программе не содержат переменные,
а вопрос ¾ простой и неосновной. В этом случае для вывода можно применить правило обобщения факта: вопрос Q выводим из программы, если найдется подстановкаq, что вопрос Qq выводим из программы. Процедура поиска ответа на простой, неосновной вопрос из программы, состоящей из фактов без переменных, сводится к поиску факта, являющегося примером вопроса. Побочным эффектом доказательства будет конкретизация переменных, входящих в вопрос. Конкретизацией называется присвоение переменной значения в процессе выполнения программы.

v Факты в программе не содержат переменных,
а вопрос¾конъюнктивный и неосновной:
?¾G1,G2.
Процедура поиска ответа на конъюнктивный, неосновной вопрос из программы, состоящей из фактов без переменных, сводится к поиску факта, являющегося примером цели G1, а затем после подстановки значений общих переменных в цель G2 производится поиск факта, являющегося примером цели G2 данного вопроса. Если такой факт обнаруживается, то выполняется конкретизация переменных цели G2, которые не являются общими с целью G1, и вычисление конъюнктивного вопроса завершается успешно.

Вычислительная модель логической программы.

Унификация термов.

Основой вычислительной модели языка Пролог является алгоритм унификации. Унификация (или сопоставление) — основной шаг процесса вычисления запроса, именно в результате унификации происходит конкретизация переменных и обеспечивается продвижение к успешному завершению логического вывода запроса. Операндами операции унификации являются логические термы.

Термы унифицируются по следующим правилам:

1. Если термы Т1 и Т2 — константы, то они унифицируются только в том случае, когда они одинаковы. Целые и вещественные числа сопоставимы только с равными им числам. Атомы сопоставимы только с идентичными атомами. Строки сопоставимы с одинаковыми строками.

2. Если терм Т1—константа или составной терм, а Т2 — неконкретизированная переменная, не содержащаяся в Т1, то Т1 и Т2 унифицируются, причем в результате переменная Т2 конкретизируется значением Т1.

3. Если термы Т1 и Т2 — неконкретизированные переменные, то их унификация успешна всегда, причем в результате унификации эти переменные становятся сцепленными, то есть при конкретизации одной из них, другая одновременно конкретизируется тем же значением.

4. Если Т1 и Т2 ¾составные термы, то Т1 и Т2 унифицируются успешно, когда они имеют одинаковые главные функторы и арности, и каждая пара соответствующих компонент составных термов успешно унифицируется.    

При выполнении логического вывода скрыто от пользователя выполняется большое число операций унификации, обусловленных встроенным в Пролог¾систему алгоритмом логического вывода.

Однако, у программиста имеется возможность задать в качестве одной из целей явное выполнение унификации двух термов с помощью операции сопоставления ‘=’. Знак ‘\=’ является знаком отрицания сопоставления. Пусть Т1 и Т2 ¾ произвольные термы. Выражение Т1=Т2 ¾ истина, когда термы Т1 и Т2 унифицируемы (сопоставимы). Выражение Т1\=Т2 ¾истина, когда Т1 и Т2 не сопоставимы.

Рассмотрим примеры использования операций сопоставления и отрицания сопоставления.

Пример 4.2.1.

?¾2+1=1+2.

no

Составные термы 2+1 и 1+2 не сопоставимы, и операция сопоставления этих термов неуспешна.

Пример 4.2.2.

?¾2+1\=1+2.

yes

Операция отрицания сопоставления термов 2+1 и 1+2 успешна.

Пример 4.2.3.

Операцию отрицания сопоставления можно использовать в правилах. Например, надо написать правило с заголовком sister(X,Y). Предикат sister(X,Y)¾истинен, если X¾сестра Y.

Правило записывается следующим образом:

sister(X,Y) :¾parent(Z,X),parent(Z,Y),person(X,’ж’,_),X\=Y.

Если в Пролог¾программе записаны утверждения примера в пункте 3.2.5, то в ответ на вопрос, кто является сестрой Y? мы получим 3 ответа:
?¾sister(X,Y).
X=’Элизабет’                   ответ 1
Y=’Джон’¾>;
X=’Анна’                          ответ 2 
Y=’Пат’¾>;
X=’Пат’                            ответ 3
Y=’Анна’¾>;
no

Ответ 2 читается как“Анна ¾ сестра Пат”, а ответ 3 означает “Пат ¾ сестра Анны”. Это два различных ответа, с точки зрения выше приведенной программы.