Математическое введение в декларативное программирование. Зюзысов В.М. - 42 стр.

UptoLike

ВУЗ: 

ТГУ | Томск

Составители: 

Рубрика: 

7 Логическое программирование
Методология логического программирования – подход, согласно которому про-
грамма содержит описание проблемы в терминах фактов и логических формул, а решение
проблемы система выполняет с помощью механизма логического вывода.
Идея использования языка логики предикатов первого порядка в качестве языка
программирования возникла еще в 60-ые годы, когда создавались многочисленные систе-
мы автоматического доказательства теорем и основанные на них вопросно-ответные сис-
темы. Суть этой идеи заключается в том, чтобы программист не указывал машине после-
довательность шагов, ведущих к решению задачи, как это делается во всех процедурных
языках программирования, а описывал на логическом языке свойства интересующей его
области, иначе говоря, описывал мир своей задачи. Другие свойства и удовлетворяющие
им объекты машина находила бы сама путем построения логического вывода.
После открытия метода резолюций он, по предложению Грина (Cordell Green),
вскоре был использован в качестве основы нового языка программирования. Алан Колме-
роэ (Alain Colmerauer) создал язык логического программирования Prolog в 1971 году. В
основе логических языков лежит теория хорновских дизъюнктов. Логическое программи-
рование пережило пик популярности в середине 80-х годов 20 века, когда оно было поло-
жено в основу проекта разработки программного и аппаратного обеспечения вычисли-
тельных систем пятого поколения [11].
Можно выделить два основных метода, присущих методологии логического про-
граммирования:
метод единообразного применения механизма логического доказательства ко всей
программе;
•
• метод унификации – механизм сопоставления с образцом для создания и декомпози-
ции структур данных.
7.1 Стратегия метода резолюций в Прологе
Поиск ответов на запросы к программам на Прологе осуществляется путем по-
строения логического вывода в системе SLD-резолюции. Прежде чем дать формальное
определение SLD–резолюции введем некоторые понятия [4, с. 359–361].
Как уже говорили, все переменные, содержащиеся в фактах и правилах, находятся
в области действия (явно не указанных) кванторов всеобщности. Поэтому, не меняя смыс-
ла программы, мы можем изменять имена переменных, избегая тем самым их коллизии
при унификации. Переименованием переменных в выражении E
1
относительно выражения
E
2
называется любая подстановка вида θ = {Y
1
/X
1
,…, Y
n
/X
n
} такая, что Y
1
,…, Y
n
– различ-
ные переменные не входящие в E
1
, и выражения E
1
θ
и E
2
общих переменных не имеют.
Состоянием будем называть всякую пару вида <G, θ>, где G - запрос, а θ - подста-
новка (пустой запрос принято обозначать через , а пустую подстановку - через ε). Для
каждой программы P определим на множестве состояний бинарное отношение →. Допус-
тим, что G имеет вид A
1
, .., A
n
и в программе P присутствует правило
B:-B
1
, ..., B
k
.
(или факт B, если k=0). Пусть далее θ
1
- переименование B, B
1
, ..., B
k
относительно G, и
пусть θ
2
= {t
1
/X
1
, ..., t
n
/X
n
} - наиболее общий унификатор A
i
и Bθ
1
при некотором i
(1≤i≤n), причем термы t
i
и формулы A
i
не имеют общих переменных. В этом случае мы
пишем
<( A
1
, .., A
n
), θ> → <(A
1
, ..., A
i
−
1
, B
1
θ
1
, ..., B
k
θ
1
, A
i
+1
, ..., A
n
) θ
2
, θθ
2
>
и называем запрос
(A
1
, ..., A
i
−
1
, B
1
θ
1
, ..., B
k
θ
1
, A
i
+1
, ..., A
n
) θ
2
резольвентой запроса G и указанного выше правила.
42

Страницы