Рассел С., Норвиг П. Искусственный интеллект: современный подход
Лорьер Ж.-Л. Системы искусственного интеллекта
Метакидес Г., Нероуд А. Принципы логики и логического программирования
Компаниец Р.И., Маньков Е.В., Филатов Н.Е. Системное программирование. Основы построения трансляторов
Порядок изложения в большей степени обязан книге Лорьера.
I. Формальная система – совокупность чисто абстрактных объектов, в которой представлены правила оперирования множеством символов в чисто синтаксической трактовке. Формальная система определена, если:
П.1. Задан конечный алфавит (конечное множество символов).
П.2. Определена процедура построения правильных слов (формул).
П.3. Выделено множество слов, называемых аксиомами.
П.4. Задано множество правил вывода, которые позволяют из множества аксиом получать новые формулы. Правило вывода в общем случае имеет вид: A1 и A2 и ... An –> B1 и B2 и ... Bm, где Ai и Bj – формулы, «–>» читается как «влечет».
1-й пункт определяет лексику, а 2-й пункт – синтаксис формального языка. Множества в п.3 и п.4 не обязательно конечны, они также могут быть рекурсивно-перечислимыми.
Определив формальную систему, мы создаем некий виртуальный мир, в котором можем жонглировать идеями, как захотим. Далее эта система, словно тамагочи, будет развиваться сообразно своей внутренней логике, т.е. той логике, которую мы в неё вложили в виде правил вывода и аксиом.
Различают:
П.4а. Правила, применяемые к формулам, рассматриваемым как единое целое. Например, (x
П.4б. Правила, применяемые к любой отдельной части формулы, причем сами эти части тоже являются формулами. Например, (x-x) –> (0). Их еще называют правилами переписывания.
И продукция, и правило переписывания имеют только одно направления вывода – слева направо.
Пример формальной системы: логика высказываний.
- П.1. Алфавит:
- пропозициональные символы: A1, A2, …, B1, B2, ...
- логические связки: и, или, не, –>, <–>
- запятые и скобки: «“», «”», «,», «(», «)»
- П.2. Правильно построенные выражения рассматриваются как высказывания. Введем определение высказывания:
- 1. Пропозициональные символы являются (атомарными) высказываниями.
- 2. Если p и q – высказывания, то (p и q), (p или q), (не p) – (составные) высказывания.
- 3. Выражения, составленные в соответствии с двумя вышеприведенными пунктами, и только они, являются высказываниями.
- П.3. В качестве аксиом выбираются тавтологии:
- q -> (t -> q)
- ( q -> (t -> q) ) -> ( (q -> t) -> (q -> t) )
- ( не q -> не t ) -> ( t -> q )
- П.4. Правило вывода Modus Ponens (название обязано Диогену Лаэртскому):
- q, q->t |– t
Формула M называется теоремой, если она доказуема (выводима) или является аксиомой. Тогда пишут так: |– M. Если формула M выводима из множества теорем S, то пишут: S |– M.
Множество цепочек символов из алфавита, вообще говоря, бесконечно. Но только некоторые из этих цепочек являются формулами (согласно п.2). И только некоторые из этих формул являются теоремами (согласно п.3 и п.4). И только некоторые из этих теорем являются аксиомами (согласно п.3).
Формальную теорию называют разрешимой, если существует определенный, эффективный способ, чтобы выяснить, является ли некая формула в этой теории теоремой или нет. Такая процедура называется процедурой разрешения. Интересно, что уже такая фундаментальная теория как логика предикатов первого порядка не является разрешимой.
Доказуемость, выводимость формулы – формальный факт. Важно понимать, что доказуемость и истинность – это не одно и то же. В общем виде доказуемое и истинное не совпадают. Трудность состоит как раз в том, чтобы для заданной предметной области построить такую формальную систему, в которой они будут совпадать.
III. Если S = {s1, s2, ..., sn} – множество символов формальной системы, то интерпретация I определяет отображение: S –> R, где R – множество объектов реального мира. Истинностной интерпретацией называется интерпретация R = {true, false}, которая придает каждому символу формальной системы истинностное значение. Существует множество интерпретаций, в которых разным символам приписываются разные истинностные значения.
Лорьер пишет: «Отметим, что речь идет о замыкании или логическом завершении понятия математического подхода. Вначале математик изучает реальность, конструируя некое абстрактное представление о ней, т.е. некую формальную систему. Затем он доказывает теоремы этой формальной системы. <...> Наконец, он возвращается к исходной точке всего построения и дает интерпретацию теорем, полученных при формализации. <...> Вся польза и удобство формальных систем как раз и заключается в их абстрагировании от конкретной реальности. Благодаря этому одна и та же формальная система может служить моделью многочисленных различных конкретных ситуаций». (Можно предположить, что структурализм, возникший в 20-х годах XX века, был естественным продолжением в социальных и гуманитарных науках того формального подхода, который зародился в математике на рубеже XIX-XX веков.)
С практической точки зрения, «необходимо, конечно, чтобы для данной формальной системы всегда существовала по крайней мере одна интерпретация, в которой каждая теорема данной формальной системы была бы истинной» (Лорьер).
Цепочки символов из алфавита образуют выражения. Синтаксически правильные (согласно п.2) цепочки образуют высказывания. Теоремы формальной системы, будучи интерпретированными, становятся утверждениями, и уже можно делать выводы об их истинности или ложности. Однако истинность формулы ничего не говорит о том, доказуема ли она в данной формальной системе!
1. Высказывание q называется логически истинным, или допустимым, или тавтологией, если во всех интерпретациях оно принимает истинное значение. I(q) = true. Пишут: |= q.
2. Высказывание q называется выполнимым, или подтверждаемым, если существует такая интерпретация, в которой оно принимает истинное значение. Ii(q) = true.
3. Высказывание q называется логически ложным, или невыполнимым, или противоречивым, если оно ложное во всех интерпретациях. I(q) = false.
4. Два высказывания q и p логически эквивалентны, если для каждого истинностного означивания I: I(q) = I(p).
5. Множество S (семантически) непротиворечиво, или выполнимо, или подтверждаемо, если существует истинностное означивание, которое подтверждает каждое высказывание из S. Если же каждое истинностное означивание не подтверждает по меньшей мере одно высказывание из S, то S противоречиво.
6. Каждое множество высказываний SV = {q: V(q) = true}, где V – истинностное означивание, составляет возможный мир. Возможные миры – основное понятие семантики Крипке, которая используется при изучении модальной логики, в которой кроме логических связок есть специальные символы – модальные операторы. В модальной логике встречается выражение o А, которое может интерпретироваться как «иногда А истинно» или «А будет истинно в будущем». (Как писал К. Г. Юнг в «Отношениях между Я и бессознательным»: «Есть истины, которые истинны лишь послезавтра, и такие, что были истинны еще вчера, - а некоторые не истинные ни в какое время».)
Аксиоматическая система полна, если каждая тавтология может быть доказана из аксиом последовательным применением правил вывода. Аксиоматическая система корректна, если из неё можно вывести только истинные высказывания. Любую из аксиом формальной системы можно заменить правилом, и наоборот. Выбор между аксиомами и правилами – вопрос субъективной оценки характерных требований теории.
Возможны четыре случая:
1. Формула доказуема и соответствует интерпретации, значение которой истинно. Желательный вариант.
2. Формула недоказуема и соответствует интерпретации, значение которой ложно. Случай корректный, но не представляет интереса.
3. Формула доказуема, но соответствует интерпретации, значение которой ложно. Может использоваться для корректировки формальной системы, таким образом, чтобы с ней остались связанными только те интерпретации, значения которых истинны для всех теорем системы. Убираем неподходящие интерпретации.
4. Формула недоказуема, но соответствует интерпретации, значение которой истинно. Говорит о недостатках формальной системы. Существуют формальные системы, в которых класс недоказуемых и неистинных формул не является пустым при всех интерпретациях!
IV. Метаязык – язык, используемый для рассуждений о формулах некоторого языка и для исследования их свойств. Когда мы говорим, что |= q, т.е. что q – тавтология, мы выражаем суждение о q. Поэтому |= q является метавысказыванием для формальной системы, содержащей высказывание q.
Метаязык может быть формализован. Для избежания чрезмерного педантизма вводят дополнительные символы, чтобы различать метавысказывания от высказываний, например, «–>» в языке высказываний и «=>» в метаязыке. Однако граница между этими двумя уровнями весьма тонка.
V. Формальные грамматики образуют подмножество формальных систем. Все правила формальной грамматики являются правилами переписывания, множество символов делится на множество терминальных и нетерминальных, и единственной аксиомой служит один из нетерминальных символов (начальный символ, главный нетерминал). Множество правил называют схемой грамматики. Цепочка символов, стоящая в левой части правила грамматики, обязательно содержит хотя бы один нетерминальный символ. В правой же части правила в общем случае может стоять произвольная цепочка из терминальных и нетерминальных символов, включая и пустую цепочку.
Языком, порождаемым этой грамматикой, называется множество всех цепочек терминальных символов, выводимых из аксиомы грамматики.
В качестве примера рассмотрим грамматику, порождающую язык булевых формул с переменными a, b и c:
- Символы:
- Терминалы: {a, b, c, и, или, не, (, )}
- Нетерминалы: {I}
- Аксиомы:
- {I}
- Правила вывода:
- { I -> ( I и I )
I -> ( I или I )
I -> ( не I )
I -> a
I -> b
I -> c }
I => ( I или I ) => ( (I и I) или I ) => ( (a и I) или I ) => ( (a и b) или I ) => ( (a и b) или c )
Если дана цепочка символов «( (a и b) или c )», то используя приведенную грамматику, мы можем выяснить, является эта цепочка допустимой или нет. Формальные грамматики широко используются для спецификации языков программирования и при создании трансляторов – например, с помощью грамматик можно определить множество допустимых имен переменных или множество синтаксических конструкций языка.
Существует классическая классификация формальных грамматик (Хомский):
0. Правила вывода грамматики имеют вид q –> w без каких-либо ограничений на q и w. Языки этого класса могут служить моделью естественных языков.
1. Правила имеют вид e1 a e2 –> e1 b e2, где e1, e2 - любые (в том числе и пустые) цепочки символов, a – нетерминальный символ, b – любая непустая цепочка. Это класс контекстно-зависимых языков (НС-грамматик). Каждое правило вывода указывает подстановку непустой цепочки b вместо нетерминала a при условии, что а находится в контексте e1 и e2.
2. Все правила грамматики имеют вид A –> b, где А – нетерминал, а b – непустая цепочка символов. Это класс контекстно-свободных языков (КС-грамматик). В виду их простоты именно их используют для определения синтаксиса (точнее, большей части синтаксиса) языков программирования.
3. Все правила имеют вид A –> bB и A –> b, где A, B – нетерминалы, b – терминал. Это класс языков с конечным числом состояний или регулярных, автоматных языков (А-грамматик). Их используют для определения лексики языков программирования.
Интересно, что каждому классу языков соответствует свой класс абстрактных машин, так, что для определения и реализации языка пригодится автомат соответствующего класса:
| 0. Рекурсивно-перечисляемые множества | Машины Тьюринга |
| 1. НС-языки | Линейно-ограниченные автоматы |
| 2. КС-языки | Автоматы с магазинной памятью |
| 3. Регулярные языки | Конечные автоматы |
VI. Приведу практический пример, где можно использовать формальные системы. Рассмотрим подход В. Проппа, изложенный в его «Морфологии сказки». Пропп интересовался, из каких структурных элементов слагается волшебная сказка, и как эти элементы соотносятся с целым. В качестве структурного элемента он предложил рассматривать функции действующих лиц сказки. Функцией он назвал «поступок действующего лица, определенный с точки зрения его значимости для хода действия». Так, не имеет значения, если «Царь дает удальцу коня» или «Колдун дает Ивану лодочку» - выделяется абстрактная структура дарения. В результате сказка может быть схематически описана в виде последовательности функций (поступков), причем некоторые из функций могут следовать друг за другом, а некоторые – нет, так как некоторые последовательности являются нелогичными. «Так, например, нелогично, если герой, исполнив трудную задачу яги, затем похищает у нее жеребенка. Это не значит, что таких соединений в сказке нет. Они есть, но рассказчик в таких случаях дополнительно должен мотивировать поступки своих героев».
Если определить формальную грамматику, в которой символы – это функции (Пропп называет с 40 штук), а логически корректные последовательности функций – слова, исходные ситуации сказок - аксиомы, то такая грамматика сможет быть использована для автоматической генерации сказок. Воплотив её в программном коде, можно добавить модуль, который будет данные схемы одевать в пышные ризы русских (китайских, клингонских и т.д.) фраз или визуализировать их в виде мультфильмов или компьютерных игр. Своего рода машинка для бесконечной генерации сказочных сюжетов.
Уже есть по крайней мере одна программа, которая использует формальные грамматики для реализации теории Проппа - называется TALE.
Формальные грамматики могут служить для моделирования сложных ветвящихся процессов. Скажем, если вы интересуетесь нелинейной литературой и разрабатываете ветвящийся сюжет, вы можете использовать формальные грамматики.