Козьма Прутков. Мысли и афоризмы



страница1/6
Дата26.04.2016
Размер1.04 Mb.
  1   2   3   4   5   6

1. Введение


Лучшим каждому кажется то,

к чему он имеет охоту.

Козьма Прутков. Мысли и афоризмы

Цель написания любой программы для ЭВМ заключается в построении такой модели предметной области, которую можно использовать для решения некоторых возникающих в этой области задач. Качество модели при этом определяется как способностями программиста, так и тем набором инструментов (языков программирования), которые он использует. Очевидно, что при прочих равных условиях выбор языка может иметь решающее значение. Смысл программы на традиционном процедурном языке определяется в терминах поведения компьютера при исполнении этой программы, в то время как исходное понимание задачи не имеет машинно-ориентированной специфики. Поэтому неформальный этап разработки и реализации алгоритма решения требует от программиста значительных затрат времени и высокой квалификации.

Суть идеи логического программирования состоит в том, что компьютеру в качестве программы можно предоставить не алгоритм, а формальное описание предметной области в виде системы отношений между ее объектами (реляционную модель), поручив решение задачи на этой модели самому компьютеру. Тогда при наличии эффективного метода автоматизации доказательства (машины вывода) задача программиста сводится к аксиоматизации предметной области в машинно-независимых терминах. Практическая эффективность логического программирования при этом по-прежнему зависит как от удачной аксиоматизации задачи, так и (в еще большей степени) от качества интерпретатора, автоматизирующего доказательство. Однако машинно-независимый уровень описания модели задачи обещает существенную экономию усилий программиста. Наиболее известная и эффективная реализация идей логического программирования воплощена в языке Пролог1, который давно и успешно применяется для решения целого ряда задач. Среди них


  • разработка быстрых прототипов приложений,

  • автоматизация перевода естественных и искусственных языков,

  • разработка естественно-языковых интерфейсов,

  • создание экспертных систем и оболочек,

  • символьное интегрирование, дифференцирование и решение уравнений,

  • доказательство теорем.

В данном учебном пособии рассмотрены математические основы логического программирования, показаны возможности и ограничения реализации логических программ в среде ТурбоПролог, рассмотрены примеры использования этого языка для разработки быстрого прототипа системы качественного моделирования, а также реализация версии Пролог-машины на языке C++.

2. Основы логического программирования

Язык логики предикатов


После ряда наблюдений я установил с исключительной точностью, что каждая селедка – рыба, но не каждая рыба – селедка.

А. Некрасов. Приключения капитана Врунгеля

Формальное определение языка логики предикатов включает в себя следующие правила.



  • Терм – константа, переменная или кортеж f(x1,…xn) из n>0 термов xi, перед которым стоит функциональный символ (функтор) f.

  • Предикат P(x1,…,xn) – кортеж из n0 термов xi, перед которым стоит предикатный символ P. Предикат является атомарным элементом языка, имеющим истинностное значение.

  • Формула – предикат или выражение, построенное из формул при помощи логических функций (табл.1)1 и кванторов (табл. 2).

  • Предложение - это формула, в которой каждая входящая переменная находится в области действия квантора по этой переменной.

Множество всех предложений, построенных согласно вышеприведенным правилам, образует язык логики предикатов первого порядка. В этом языке термы используются для обозначения конкретных (константы) или абстрактных (переменные) объектов предметной области. Например, терм

книга(«Толкиен», «Властелин колец»)

описывает конкретный структурированный объект книга, атрибутами которого являются автор и название, заданные в виде текстовых констант, терм

книга(«Толкиен»,Y)

описывает абстрактный объект (некая книга Толкиена). Предикаты определяют отношения между объектами предметной области:

читает(человек, книга),

а предложения описывают логические свойства этих отношений:

читает(X, книга(«Гофман»,Y))  любит(X, «сказки»)

и в совокупности образуют аксиоматическую теорию.


Метод резолюций


На удочку насаживайте ложь

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

В. Шекспир. Гамлет

Язык логики предикатов, помимо бесспорных преимуществ над алгоритмическими языками в части формализации описания предметной области1, представляет собой исключительно благоприятную среду для автоматизации вывода. Наиболее подходящим для автоматизации вывода является так называемый метод резолюции. Суть его состоит в добавлении к аксиоматической теории T отрицания доказываемого утверждения Q (запроса) и последующих систематических попытках доказательства непоследовательности теории TQ, которая формально устанавливается по наличию фразы вида Q & Q. Наличие этой фразы означает, что дополнение теории отрицанием доказываемого утверждения привело к противоречию, и, следовательно, Q является следствием T. Напротив, неудача резолюции означает, что утверждение Q недоказуемо (но не ложно – своеобразная «презумпция невиновности»!) в теории T. Этот подход является общепринятым в математике и носит название доказательства от противного (reductio ad absurdum): отрицание опровергается путем демонстрации того, что его допущение ведет к противоречию. Метод резолюции применяется к подмножеству предложений, называемых фразами Хорна. Фразы Хорна – это предложения, построенные из положительных и отрицательных литералов2 при помощи связок “&” и “”, причем положительный литерал, если он присутствует в предложении, должен быть единственным. Фразы Хорна вида:



A B C D

A

B C D

называются соответственно правилом, фактом и запросом, и в результате тождественных преобразований (см. табл. 1) могут быть переписаны в удобном для прочтения виде1:
A:- B, C, D

A

 (B, C, D)


Аксиоматическая теория, в контексте которой выполняется доказательство запроса по методу резолюции, содержит только предложения в формате фактов и правил. В качестве примера представления теории множеством фраз Хорна рассмотрим следующие определения:
Мужчина(«Василий»).

Мужчина(«Сергей»).

Мужчина(«Александр»).

Мужчина(«Лев»).

Женщина(«Надежда»).

Женщина(«Ольга»).

Отец(«Сергей», «Александр»).

Отец(«Сергей», «Лев»).

Отец(«Сергей», «Ольга»).

Мать(«Надежда», «Александр»).

Мать(«Надежда», «Лев»).

Мать(«Надежда», «Ольга»).

Брат(X,Y):- Мужчина(X), Отец(F,X), Мать(M,X), Мужчина(Y), X<>Y, Отец(F,Y), Мать(M,Y).

Приведенные определения включают в себя факты Мужчина, Женщина, Отец, Мать, описывающие отношения между конкретными людьми (в данном случае – родственниками Пушкина), и общезначимое правило2, определенное в терминах абстрактных объектов – переменных. Семантика фактов очевидна, правило же утверждает, что братьями являются два любых (внешний квантор общности, связывающий переменные правила, не показан) различных мужчины, имеющих общего отца и общую мать.


Таблица 2.1

Логические функции



Аргументы

Функции

X1

X2

Отрица-ние

Конъюнкция

Дизъюнкция

Неравнозначность

Равнозначность

Импликация

Стрелка Пирса

Штрих Шеффера









&













0

-

1

-

-

-

-

-

-

-

1

-

0

-

-

-

-

-

-

-

0

0

-

0

0

0

1

1

1

1

0

1

-

0

1

1

0

1

0

1

1

0

-

0

1

1

0

0

0

1

1

1

-

1

1

0

1

1

0

0

Таблица 2.2

Кванторы

Наименование квантора

Обозначение

Пример использования

Интерпретация

Общности



(X)1 селедка(X)рыба(X)

Всякая селедка – рыба,

Существования



(X) рыба(X)селедка (X)

но не всякая рыба – селедка

Множество фактов, устанавливающих отношения между константными объектами, иногда называют базой данных, а все прочие предложения - базой знаний логической программы. Именно наличие в логической программе общезначимых предложений обеспечивает возможность вывода (путем доказательства) информации, отсутствующей в программе в явном виде. Так, результатом применения метода резолюции к представленной теории, дополненной запросом Брат(X, Y), будут два решения:

X = «Александр», Y = «Лев»,

X = «Лев», Y = «Александр».

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



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

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

  • Метод резолюции не смог доказать “братских” отношений между Сергеем и Василием, так как соответствующая информация теории недоступна. Это еще раз подчеркивает разницу между “недоказуемо” и “ложно”.

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

Рассмотрим теперь алгоритм резолюции на аксиоматической теории, составленной из фраз Хорна, более подробно, для чего введем необходимые понятия.

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

Под унификацией в логическом программировании понимается процедура попарного сопоставления термов, подчиняющаяся следующим правилам.


  • Константа может быть унифицирована сама с собой или со свободной переменной.

  • Свободная переменная может быть унифицирована с любым термом.

  • Функциональный терм унифицируется с другим функциональным термом при условии, что оба имеют один и тот же функтор и одинаковое количество попарно унифицируемых аргументов.

В результате унификации константы или связанной переменной со свободной переменной последняя приобретает статус связанной. Таким образом, механизм унификации обеспечивает выполнение трех функций:

  • Логической проверки равенства.

  • “Присваивания”1 значений переменным.

  • Анализа структур данных.

Элементарным шагом доказательства в методе резолюций является построение резольвенты (от resolve – разрешать). Резольвента – это фраза Хорна, построенная из двух исходных фраз, одна из которых имеет положительный P, а другая – одноименный отрицательный P литерал, причем аргументы этих двух литералов попарно унифицируемы, путем объединения всех литералов исходных фраз за исключением P и P. Например, резольвентой фраз P и P R S (при условии, что аргументы P и P попарно унифицируемы) будет фраза RS, резольвентой P и P будет, очевидно, пустая фраза (противоречие).

Алгоритм резолюции строит первую резольвенту с участием запроса, для которого последовательным просмотром предложений теории подыскивается подходящее для резольвирования, а все последующие – аналогичным способом с использованием резольвенты, полученной на предыдущем шаге. Процесс построения резольвент и сопутствующего связывания переменных продолжается до тех пор, пока не будет построена пустая фраза, либо построение очередной резольвенты окажется невозможным1. В первом случае принято говорить об успехе вычислений, которое обозначается меткой □, а во втором – об их неудаче, обозначаемой меткой ■. При успехе вычислений множество связанных переменных запроса представляет собой вариант решения, который может быть направлен на устройство вывода (единственный существенно необходимый побочный эффект!). При неудаче никаких сообщений не формируется. И в том, и в другом случае алгоритм резолюции продолжает работу, пытаясь найти другие варианты построения резольвент, начиная с последней. При этом все связывания переменных, имевшие место в результате прежнего резольвирования, отменяются, и соответствующие переменные вновь становятся свободными. Этот процесс называется возвратом. Процесс построения резольвент и возврата продолжается до тех пор, пока не останется неисследованных возможностей построения резольвент. Таким образом, порождается дерево вычислений, левосторонний фрагмент которого для доказательства запроса Брат(X, Y) представлен на рис. 2.1.

Рис. 2.1. Дерево вычислений


  1   2   3   4   5   6


База данных защищена авторским правом ©bezogr.ru 2016
обратиться к администрации

    Главная страница