Prolog и логическое программирование

Логическое программирование – это направление в программировании, основанное на идеях и методах математической логики. Термин логическое программирование в литературе по информатике трактуется в широком и узком смысле.

В широком толковании ЛП включает круг понятий, методов, языков и систем, в основе которого лежит идея описания задачи с совокупностью утверждений на некотором логическом языке и получение решения задачи путём построения логического вывода в некоторой формальной дедуктивной системе. Классы формул, используемые для описания задач, методы вывода и модели вычислений, используемые для описания задач, методы вывода и модели вычислений, используемые в таких системах, очень разнообразные, поэтому различные их комбинации образуют специфические стили программирования: концептуальная, функциональная (аппликативная) и др.

Наибольшие практические результаты достигнуты в системах программирования, где в качестве логических программ используются специальные классы логических формул: хорновские дизъюнкты, а в качестве способа их использования применяются специальные методы логического вывода-варианты метода резолюции.

Программирование с использованием таких систем называется хорновским или резолюционным, но чаще всего – логическим программированием, перенося узкую трактовку термина на более широкое понятие.

Самыми известными системами такого рода являются реализации языка Prolog (программирование в терминах логики – Programming in logic). Рассмотрим основные идеи и понятие ЛП в узком смысле.

Неформально логическая программа описывает множество объектов, множество функций и отношения этих объектов. Строится логическая программа как набор утверждений об объектах, функциях и отношениях. Такое описание является статистическим и никакого вычислительного процесса не задаёт, т.е. можно считать, что это описание определяет БД в которой хранятся объекты и заданные на них функции и отношения, например, в виде графиков. К конкретному применению логической программы относится понятие запроса (цели) – например, каково значение функции заданной логической программой при данном значении аргумента. Вычисление ответа на запрос соответствует доказательству существования такого объекта. Правила, по которым проводятся вычисления, образуют процедурно-операционную семантику логической программы. Успехи языка Prolog обусловлены тем, что с одной стороны, с помощью используемых в них логических формул – хорновских дизъюнктов – можно описать многие практические задания, а с другой – найдена простота интерпретации этих формул и построена достаточно эффективная реализация системы ЛП.

Правила в Prolog имеют вид , где – это заголовок, – атомы (тело правила). Тело может быть пустым (при m=0), такие правила называются фактами. Атом имеет вид , где – n-арный предикатный символ или имя отношения; а – термы.

Терм – это либо имя переменной, либо константа, либо составной терм вида , – это n-арный функциональный символ.

Функции, задаваемые при логическом программировании, представляются в виде отношений – n-местная функция представляется в виде (n+1) местного отношения вида .

Запрос (это цель) имеет вид: , где и – атомы.

Каждое правило допускает логическую и процедурную интерпретацию (в семантике). Логическая интерпретация правила – «истинность А₀ следует из истинности А₁…А_m» или «А₀ истинно только, если истинны А₁…А_m».

Т.о. правила рассматриваются, как формулы языка логики предикатов вида: , где:

– квантор общности.

– логическая связка «И».

– логическая связка «если, то»

В Prolog данные, формулы записываются в обратную сторону и используются другие обозначения:

или «and».

или «or».

или «: –» или .

Формулы с использованием связок может быть преобразовано в эквивалентную, но имеющую связки , формулу вида: .

Такие формулы и называются хорновскими дизъюнкциями, а стиль программирования хорновским.

Метод резолюции – получив на вход логическую программу с присоединёнными к ней запросами в виде множества хорновских дизъюнктов, пытается построить вывод пустого дизъюнкта, обозначаемого символом “□”. Если это ему удаётся, тогда цель допускается, в противном случае отвергается. Реализуется метод резолюции и помощью двух правил:

1 Правило резолюции или правило склейки, которое во время работы вызывает процедуру унификации – сопоставления.

Унификация – это процесс, на вход которого поступает два терма и для них находится унификатор.

Унификатором двух термов называется подстановка, которая делает термы одинаковыми и если унификатор существует, то термы называются унифицируемыми и для них отыскивается наиболее общий унификатор, если нет – процедура унификации сообщает об отказе.

Дата добавления: 2014-01-05