В функциональном программировании программы - это выражения, и их
исполнение заключается в вычислении их значения. В логическом
программировании программа представляет из себя некоторую теорию
(описанную на достаточно ограниченном языке), и утверждение, которое
нужно доказать. В доказательстве этого утверждения и будет заключаться
исполнение программы.
Логическое программирование и язык Пролог
появились в результате исследования группы французских ученых под
руководством Колмерье в области анализа естественных языков. В
последствии было обнаружено, что логическое программирование столь же
эффективно в реализации других задач искусственного интеллекта, для чего
оно в настоящий момент, главным образом, и используется. Но логическое
программирование оказывается удобным и для реализации других сложных
задач; например, диспетчерская система лондонского аэропорта Хитроу в
настоящий момент переписывается на Прологе. Оказывается, логическое
программирование является достаточно выразительным средством для
описания сложных систем.
В логике теории задаются при помощи аксиом и
правил вывода. То же самое мы имеем и в Прологе. Аксиомы здесь принято
называть фактами, а правила вывода ограничить по форме до так называемых
"дизъюнктов Хорна" - утверждений вида A <= B1& ...& Bn. В
Прологе такие утверждения принято записывать так:
a :- b1, ..., bn.
а факты, они же аксиомы, представлять как правила с пустой "посылкой":
a.
Переменные в утверждениях Пролога принято обозначать идентификаторами, начинающимися с заглавной буквы.
Пример простейшей программы на Прологе:
member(X, [X|_]).
member(X, [_|T]) :- member(X, T).
Эту
программу можно прочитать так: "Х является членом списка, если он
совпадает с головой списка, или является членом хвоста списка". В этой
программе объявлен один предикат - member.
Как вы заметили, это -
только набор аксиом и правил. Обычно Пролог-система работает в форме
диалога с пользователем. Утверждение, которое требуется доказать,
вводится с клавиатуры. Компилирующие версии трансляторов Пролога могут
располагать специальными синтаксическими средствами для задания
утверждений, которые требуется доказать. Такие утверждения в Прологе
принято называть целями.
Зададим Пролог-системе простейший вопрос: является ли 2 членом списка [1,2,3]? Для этого введем:
?- member(2, [1,2,3]).
Пролог-система
сначала попытается применить первое правило для предиката member,
сравнивая 2 с головой списка [1,2,3]. Это сравнение даст неуспех, в
результате чего система продолжит вывод по второму правилу, рекурсивно
вызывающему предикат member, с аргументами 2 и [2,3]. В этом рекурсивном
вызове сработает первое правило (так как 2 совпадает с головой списка
[2,3]), и Пролог-система выдаст нечто вроде:
yes ->
Так как
произвольная цель может быть доказана не единственным образом, система
предлагает нам решить, пытаться ли доказать это утверждение по-другому.
Ответим "да" (тем способом, как это предусмотрено в используемой
Пролог-системе). Осталось незадействованным второе правило для предиката
member для аргументов 2, [2,3], по которому следует пытаться доказать,
что 2 есть член списка [3]. Так как 2 =/= 3, первое правило для этой
цели не сработает, и доказательство пойдет дальше по второму правилу,
которое предписывает доказывать утверждение member(2, []). Так у для
пустых списков нет головы и хвоста, ни одно из правил для предиката
member не применимо, и Пролог-система выдаст ответ:
no.
Сведущие в
автоматизированном доказательстве теорем люди скажут, что
Пролог-система использует для доказательства утверждений "унификацию и
метод резолюций". Унификация - это сопоставление двух произвольных
термов, содержащих переменные, с целью определения того, можно ли
присвоить этим переменным такие значения, чтобы получились два
одинаковых терма. Например, унификация термов f(X, 2) и f(1, Y), где X, Y
- переменные, выдаст подстановку: X=1, Y=2. Унификация термов f(X) и Х
пройдет безуспешно. Метод резолюций заключается в последовательном
доказательстве отдельных утверждений, входящих в посылку дизъюнкта
Хорна, для доказательства его следствия. То есть, применение метода
резолюций к правилу a :- b, c. и утверждению a приведет к
последовательному доказательству утверждений b и c. Метод резолюций
имеет прямой аналог в обычной логике высказываний - правило modus
ponens, по которому (A & A=>B) => B.
Логическое
программирование допускает естественную параллельную реализацию. В
примере a :- b, c. порядок согласования целей b и c не имеет значения,
поэтому их можно доказывать параллельно. Говорят, что процессы
доказательства b и с образуют И-систему процессов: И-система успешно
доказывается, если каждый процесс, входящий в систему, успешен. В
примере с предикатом member два правила для него могли применяться
параллельно, образуя ИЛИ-систему процессов. ИЛИ-система успешно
доказывается, если хотя бы 1 процесс в системе успешен. Переменные,
общие для системы процессов(например, в случае a(X) :- b(X), c(Х).)
преобразуются в каналы связи между процессами в системе. Связывание
переменной (присвоение ей значения) аналогично посылке значения в канал.
В
настоящее время существует несколько "промышленных" реализаций языка
Пролог (наряду с большим количеством "исследовательских" версий).
"Промышленный" транслятор Пролога, как правило, порождает исполняемый
код, сопоставимый по эффективности с кодом аналогичной программы на
императивных языках; компилируемое им подмножество "чистого Пролога"
наделено строгой системой типов и возможностью вызывать процедуры,
написанные на других языках (Си, Паскаль, Ассемблер...).
Среди
экспериментальных расширений Пролога следует упомянуть такие языки, как
лямбда-Пролог (Пролог с элементами функционального программирования),
Goedel (язык, в котором семантический анализ может быть описан
алгоритмически средствами самого языка), Mercury (версия чистого
Пролога, предназначенная для промышленного использования и снабженная
системой полиморфных типов, аналогичной используемой в современных
функциональных языках).
