Математика, логика и программирование. Часть четвертая, логическое программирование

Предыдущая запись в этой серии была посвящена вопросам, традиционно объединяемым под вывеской «искусственный интеллект». Конечно, вся упомянутая там деятельность может быть довольно полезна в чисто теоретическом плане, но на практике обычно интересны другие вопросы. Я упоминал о программе Eurisko, применявшейся в самых разных областях знаний — это можно было делать, так как Eurisko работала с представленными в некоторой формализованной форме произвольными утверждениями. Система этих утверждений называется «базой знаний», а процесс построения базы знаний и создания запросов к ней — «логическим программированием».

Обычно логическое программирование связывают с языком Prolog — но только потому, что он якобы «специально» для него предназначен. На самом деле тут применяется и Lisp, и «потомки» ML, и «самописные» движки типа Inform 7.

Математическая основа логического программирования — это исчисление предикатов. Предикат — это выражение с параметрами, которое, в зависимости от этих параметров, может быть истинно или ложно. Правила их преобразования — то есть исчисление — возникло, как попытка обоснования математики Фреге и Расселом. Число этих правил, как я говорил в предыдущей части, относительно невелико. Фактически, для построения базы знаний надо представить способ записи предикатов и систему, с этими предикатами работающую. На Lisp ядро такой системы записывается в виде нескольких тысяч строчек, но «стандартом» для построения «коммерческих» баз знаний стал язык Prolog — из-за того, что в него включены некоторые «процедурные» дополнения.

Например, довольно легко записать условие типа «список отсортирован» — но неизвестен (для системы логического вывода) способ, который позволит по этому условию эффективно отсортировать список. «Обычная» система логического вывода для того, чтобы отсортировать список, «имеет право» только перебрать все перестановки его элементов — а это ну очень медленно. В разработанном в начале 70-х Prolog предусматривается возможность задать некоторые действия в «явном» процедурном стиле, что несколько упрощает процедуру вывода (то есть получения ответа на «вопрос» с использованием заданной базы знаний).

Разумеется, при построении системы «простейших» предикатов, то есть базы знаний, программист не может определить, как будут «выводиться» те или иные утверждения. Это свойство «логических» языков программирования называется декларативностью — описывается не последовательность действий для достижения результата, описывается лишь «онтология» и требования к результату. Онтология — это умное слово, обозначающее базу знаний, оно позаимствовано из философии, где означает «всего лишь» систему представлений об окружающем мире. Возвращаясь к «Логико-философскому трактату» — «окружающий мир» есть совокупность утверждений о нем. Экспертная система — еще одно названия для логического «движка» с базой знаний — не может «прыгнуть выше головы», то есть сформулировать утверждение, выходящее за рамки ее онтологии. Считается, что область применения логического программирования этим и ограничена, и сводится фактически к перебору вариантов — а с другой стороны, компьютеры все равно «перебирают варианты» быстрее человека, а главное — не стеснены «лишними знаниями». Игроки в Traveller пытались играть, «отыгрывая роли» великих адмиралов — но все их знания о военно-морской тактике оказались перечеркнуты тем, что программа перебрала все варианты стратегии, включая и самые идиотские.

Эта особенность логического программирования считается «неизбежной». В свое время пользовался известностью японский проект по созданию «компьютера пятого поколения» — фактически, предлагалось сделать машину с огромным количеством независимых процессоров, что — по мнению создателей — должно было ускорить процесс перебора вариантов и сделать «искусственный интеллект» более «доступным». В качестве основного языка для этой системы искусственного интеллекта рассматривался Prolog, но он из-за своих «процедурных» оказался неприспособлен для «параллельной» работы. Этот проект так ничем и не завершился — но многопроцессорные системы уже в ближайшем будущем могут оказаться реальностью, и логическое программирование тоже может стать практически полезным.

Правда, там, где от декларативных языков требуется производительность, и за эту производительность готовы платить — там все обстоит несколько лучше. Например, язык SQL является чисто декларативным — он описывает не процесс поиска данных, а то, какие данные удовлетворяют результату. Но в производительности СУБД заинтересованы люди с большими деньгами — и поэтому ведется постоянная работа по улучшению алгоритмов оптимизации запросов к БД.

Кстати, SQL построен на основе реляционной алгебры — предложенных Коддом в 1970 году операций для работы с «отношениями», то есть таблицами с записями. Тоже математическая теория, только про нее в популярных самоучителях типа «PHP и SQL за два дня» не пишут.

Математика, логика и программирование. Часть третья, доказательство теорем

В предудущей части я упоминал о том, что уже в 50-х появились первые попытки «научить компьютер думать», то есть доказывать математические утверждения. Программа, реализующая «традиционную» логику, получается довольно небольшой — я уже упоминал Logical Theorist — но при этом результат ее работы впечатляет. Например, будучи снабженной списком аксиом из книги Рассела и Уайтхеда «Основания математики», эта программа смогла за разумное время доказать 38 из 52 приведенных во второй главе книги теорем.

Это считалось большим успехом в области «искуственного интеллекта», авторы Logical Theorist давали прогнозы, что в ближайшие десять-пятнадцать (то есть к 1965-1970 году) лет ЭВМ смогут доказывать те же математические утверждения, что и люди.

К сожалению, этого не произошло. Не только из-за сложностей формализации любой более-менее содержательной математической теории, но и из-за связанных с теоремами Геделя трудностей. Например, для любой системы аксиом можно привести пример утверждения, которое нельзя ни доказать, ни опровергнуть. С другой стороны, все утверждения, которые можно доказать, перечислимы, то есть существует алгоритм, который будет последовательно выводить их. В простейшем виде он называется «поиск в ширину» и известен любому программисту.

Правда, сегодня существует несколько смежных с доказательством теорем направлений. Есть несколько систем для автоматической проверки доказательств (например, Mizar), важный «побочный продукт» которых — сборники формализованных определений и доказательств. Другое популярное направление — поиск всех утверждений, которые можно доказать, в надежде на то, что среди них найдется что-то новое. По-английски это называется discovery system, «открывающая» система. Одной из первых таких систем стала Automated Mathematician, о «потомке» которой, программе Eurisko, стоит рассказать подробнее.

Automated Mathematician представлял собой программу на Lisp, умевшую по определенным правилам модифицировать другие программы на том же языке, которые интерпретировались, как определения математических понятий. В 1976 Дуглас Ленат выделил «ядро» этой системы — «язык» RRL-1 (Representation Representation Language) — фактически, набор правил логического вывода. Eurisko — система, применявшая эти правила, — была обобщением Automated Mathematician и могла применяться в различных областях знаний — от проектирования СБИС до… настольных стратегических игр.

Да, не смейтесь, в 1981 году правила настолки Traveller (посвященной сражениям в космосе) были формализованы и внесены в Eurisko, и программа выработала довольно парадоксальную, но стопроцентно выигрышную стратегию — удивившую всех, кто пытался применить там, скажем, «законы» военно-морской тактики. Это считалось очень интересной демонстрацией «искуственного интеллекта» и даже привело к изменению правил игры — правда, в 1982 году Eurisko снова «победила» на соревнованиях, найдя очередную лазейку в новых правилах. После этого, во-первых, применение «сгенерированных компьютером» стратегий на соревнованиях по Traveller было запрещено, а во-вторых — проектом заинтересовалось DARPA, агентство Пентагона по перспективным научным разработкам. Уж что у них там вышло — не знаю.

К вопросу об искуственном интеллекте тесно примыкает построение баз знаний. Можно формализовать правила логического вывода, но очень важными оказываются «аксиомы» — а даже в геометрии их, по Гильберту, насчитывается 20 штук. Все тот же Ленат, обосновывая свой последующий проект Cyc, говорил, что «разум — это десять миллионов правил». Разумеется, что с десятью миллионами правил работать эффективно очень и очень сложно — а если ядро системы написано на пользующемся славой «медленного» Lisp — то вообще невозможно. Правда, есть технологии, позволяющие делать это более эффективно, и о «логическом программировании» речь пойдет в следующей части.

Математика, логика и программирование. Часть вторая, про Lisp и функциональное программирование

В первой части этой серии записей я «объявил» о существовании такой науки, как математическая логика и закончил тем, что «авторы» первых компьютеров — не только инженеры, но и математики. Если продолжать этот «исторический обзор», то необходимо пару-тройку абзацев забыть о математике и перейти к «чистой» вычислительной технике. Кстати, надо разделить понятия Computer science, «информатика» и «вычислительная техника». Под «информатикой» иногда понимается часть математической логики, которую еще называют «математикой текстов» — чисто теоретическая дисциплина, в которой как раз и рассматриваются конструкции типа машины Тьюринга или конечных автоматов. «Железо» и способы работы с ним по-русски называются «вычислительная техника», а по-английски — computer science. Последняя обычно не имеет отношения к матлогике.

Итак, возвращаемся к «историческому обзору». Разумеется, что первые компьютеры могли «программироваться» только в пресловутых «машинных кодах» или на некотором «мнемоническом» языке — подобии ассемблера. Но написавший таким способом уже две-три программы программист может заметить что-то общее и выделить эти «общие» части в подпрограмму. Дальше хочется автоматизировать способы выделения и вызова этих подпрограмм — для чего служили первые «языки программирования» — наверное, стоит упомянуть названия типа Autocode.

Кстати, уже тогда возникло разделение подпрограмм на процедуры и функции. Процедурой называлась выделенная для многократного использования последовательность действий, функцией — подпрограмма, вычисляющая значение какой-то математической функции.

Своего рода «революцией» стал появившийся в 1958 (а разработка началась в 1954) язык FORTRAN, где предусматривалось преобразование чего-то похожего на математические выражения в машинный код. FORTRAN буквально означает FORmula TRANslator. Думаю, преимущества FORTRAN и более позднего ALGOL над ранними «языками программирования» очевидны, а дискуссия о применении оператора goto вместо конструкций ветвления или цикла все еще отражена в школьных учебниках программирования. Я бы не хотел подробно останавливаться на императивных языках, они всем хорошо известны, а хотел бы перейти к более интересным вещам.

В том же «Логико-философском трактате» (да, мне он очень нравится) содержится, видимо, общепринятая сегодня точка зрения о том, что язык ограничивает возможность выражения мыслей, причем очень интересно сформулированная:

Границы моего языка означают границы моего мира.

Витгенштейн сделал из этого вывод, что вместо «естественного» языка необходим какой-то специальный, освобожденный от неоднозначностей — что-то вроде «языка» математической логики Фреге и Рассела. Правда, особых успехов в этом направлении он не достиг и в своих более поздних работах от этой идеи отказался, перейдя от вопросов построения «правильного» языка к вопросам понимания «естественного». Для нас важно то, что утверждение Витгенштейна остается верным и применительно к языкам программирования. В той же книжке Себесты эта мысль вообще считается самоочевидной, и используется для обоснования того тезиса, что «хороший» программист должен знать несколько языков программирования, желательно разных.

В математической логике довольно важную роль играет теория вычислимости, из результатов которой хотелось бы отметить построенное в 1941 году Черчем лямбда-исчисление. В середине 50-х появились первые попытки «научить» ЭВМ доказывать теоремы по геометрии, после работы Гильберта это казалось хорошей демонстрацией способности компьютера «думать», то есть пользоваться формальной логикой. В 1956 году Ньюэлом, Шоу и Саймоном была создана программа Logical Theorist, а в 1958 году МакКарти, работая в IBM над системой символьных вычислений, пришел к выводу, что комбинация FORTRAN c заложенными в Logical Theorist идеями (называлось это FLPL — FORTRAN List Processing Language, язык обработки списков на базе FORTRAN) окажется нежизнеспособна — и сделал лямбда-исчисление «теоретической базой» нового языка программирования, названного Lisp (от LISt Processor).

Программа на Lisp — это не записанная в каком-то порядке последовательность операций, а набор определений функций. Для того, чтобы вычислить функцию, необходимо вычислить сначала ее аргументы — и этот подход оказывается очень удобен. Уже на первых страницах учебников по Lisp объясняется рекурсивная программа вычисления факториала — и там это очень естественно. Кстати, понятие рекурсии происходит из теории вычислимости и лямбда-исчисления и прекрасно там разобрано еще до появления каких-либо компьютеров.

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

Этим список достоинств Lisp не заканчивается. Оказалось, что подобные Lisp функциональные языки программирования допускают очень легкое распараллеливание — так как отдельные функции могут вычисляться независимо. Тогда, в 60-х, это казалось чем-то неважным, но нынешний всплеск интереса к функциональному программированию связывают именно с развитием возможностей для параллельных вычислений.

С другой стороны, Lisp оказался очень далек от реального аппаратного обеспечения. Более того, в 60-х считалось, что языки программирования делятся на две категории — Lisp и «все остальные». Это было правдой, «все остальные» языки программирования придерживались императивного подхода, в той или иной степени обобщавшего реальное устройство компьютера, то есть «машину фон Неймана». Lisp вообще никак не был привязан к свойствам оборудования, и считался очень неэффективным. Правда, в середине 70-х появились так называемые лисп-машины с аппаратной поддержкой некоторых свойств языка, но они были вытеснены быстро развивавшимися компьютерами общего назначения. «Обычным» применением для Lisp и его более современных диалектов (Scheme и Common Lisp) считается «искуственный интеллект» и связанные с ним задачи — например, представление знаний, машинное обучение, обработка естественных языков и тому подобные задачи. Правда, никто не мешает использовать Lisp и в более «стандартных» областях — например, на Lisp написан текстовый редактор Emacs, Scheme используется в некоторых системах информационной безопасности, на Common Lisp была написана одна из первых в мире систем интернет-магазинов.

Среди других функциональных языков стоит назвать РЕФАЛ (РЕкурсивных Функций АЛгоритмический язык), созданный Валентином Турчиным в 1966 году. Кстати, рекурсия впервые появилась именно в Lisp, и является для функциональных языков «естественной» — тогда как в императивных она оказывается чем-то сложным и чужеродным. Из более современных — ML (возникший, как часть системы доказательства теорем LCF), его «потомков» Caml и OСaml, Erlang — интересный тем, что сразу предназначался для «практического» программирования, Haskell — последний является интересным примером реализации «чистого» лямбда-исчисления, не допускающего побочных эффектов. В нем отсутствуют такие привычные «императивным» программистам понятия, как переменные и присваивания — а для «неминуемых» операций с побочными эффектами, вроде ввода-вывода, применяются так называемые «монады».

В следующей части обещаю вернуться к автоматизированному доказательству теорем и прочим развлечениям из области математической логики. Я уже упомянул это «развлечение» в предыдущем абзаце и просто-таки обязан продолжить.

Математика, логика и программирование. Часть первая, про логику

Для начала — как модно говорить, дисклеймер. Я обещал написать некий текст «для чайников», в котором обещал упомянуть такие вещи, как функциональное и логическое программирование. К сожалению, «для чайников» писать я не умею, а умею только прятать в связном тексте ссылки на показавшиеся мне интересными вещи. Получилось на мой взгляд, во-первых, длинновато, а во-вторых — требует от читателя некотого усилия для понимания. Вышла своего рода «компиляция» из книжки Р. Себесты «Основные концепции языков программирования», разнообразных википедий, философии и истории математики.

Думаю, стоит разбить получившийся текст на несколько частей. Для начала я хотел бы рассказать о такой области человеческой деятельности, как математическая логика — это будет полезно для понимания следующих частей. Мне кажется, что очень важно с «теоретической» точки зрения продемонстрировать то, что «нетрадиционные» методы программирования хорошо обоснованы с математической точки зрения — чем и отличаются от чисто «эмпирически» выросшего императивного и объектно-ориентированного подходов.

Начну, как обычно, издалека. В далеком XVII веке Ньютон и Лейбниц независимо друг от друга придумали дифференциальное и интегральное исчисление. Разумеется, они не написали учебник Зорича или Фихтенгольца, а лишь сформулировали некий набор правил работы с «бесконечно малыми величинами» — тем самым создав новое занятие для математиков — поиск обоснования этих правил. Занимались этим все кому не лень, в свое время отметился даже Карл Маркс, причем отметился очень интересно — подойдя к проблеме с точки зрения диалектики. Интересующиеся могут найти в интернете отсканированное издание «Математических рукописей». Впрочем, к концу XIX века сложилась некая более-менее стройная и общепринятая система определений и теорем, «обосновывающая» законность придуманных Ньютоном правил, получившая название «классического анализа».

Любой изучавший матан должен помнить как минимум о существовании двух определений предела функции — «по Коши» и «по Гейне», продвинутые студенты и матшкольники могут назвать несколько конструкций действительных чисел (оказывается, это далеко не «тривиальные» объекты) — в общем, сложилось нечто более-менее логичное и устраивающее почти всех. Все остальные подходы получили название «нестандартного анализа» и были отправлены на свалку истории — в частности, пресловутые «Математические рукописи» Маркса получили некую известность лишь в 1963 году благодаря работе С. А. Яновской. Правда, хотелось бы отметить, что в последнее время к нестандартному анализу возник некий интерес. Говорят, что китайцы очень активно бросились развивать высказанные Марксом идеи — на то они и китайцы.

Вместо неочевидной «системы правил» дифференциального и интегрального исчисления «классическое» обоснование математического анализа опирается на набор «очевидных» фактов теории множеств. С другой стороны, теория множеств в плане неочевидности ничуть «не хуже». Начнем хотя бы с того, что «наивная» теория множеств – пока мы не пытаемся построить ее аксиоматику — допускает большое количество «парадоксов» (к ним относится и известный «парадокс брадобрея»). Попытка ее аксиоматизации порождает неочевидную «аксиому выбора» — а ко времени первых попыток такой аксиоматизации на примере геометрии Лобачевского стало ясно, что отказ от «неочевидной» аксиомы может породить столь же непротиворечивую систему утверждений.

Фактически, возникла проблема обоснования математики — то есть разрешения парадоксов теории множеств. Проблема действительно важная — потому что требовалось объяснить, «а чем это мы все тут занимаемся». Должна ли математика быть связана с реальным миром, или же математические объекты чисто умозрительны? А если они умозрительны — то почему же можно пользоваться математикой в расчетах? Можно ли «доверять» математическим рассуждениям? Эта проблема получила несколько решений, к сожалению, неудовлетворительных.

Первым стоит назвать логицизм, развитый Фреге и Расселом. Основываясь на том, что логика, или исчисление предикатов, «априорна», они попытались построить на ее основе «арифметику», то есть систему объектов, ведущих себя как действительные числа. «Проблемной» оказалась аксиома бесконечности — о существовании хотя бы одного бесконечного множества. Она не присутствует в логике и поэтому математика к «чистой» логике не сводится.

Своеобразным «ответом» на это стал интуиционизм Брауэра. Утверждалось, что математика должна быть «конструктивной». Можно рассматривать данные в интуиции объекты (конечные) и явным образом построенные из них — без снятия двойного отрицания и закона исключенного третьего. Правда, оказалось, что фундаментальные утверждения математического анализа неконструктивны.

Очень важной попыткой обосновать математику стал формализм, построенный Гильбертом. Для доказательства непротиворечивости теории, согласно Гильберту, необходимо «всего лишь» построить полностью описывающую ее систему аксиом, с которыми разрешается работать только по «правилам» логики. В 1899 году Гильберт в «Основаниях геометрии» построил полную аксиоматику евклидовой геометрии — и если в дальнейшем строго следовать его подходу, то получится, что все утверждения геометрии — это конечные комбинации этих аксиом, построенные по определенным правилам.

Правда, в 1931 году Гедель доказал, что с помощью конечных систем аксиом и конечных же доказательств нельзя обосновать арифметику — а это означало несостоятельность формализма как обоснования математики. Но очень важным результатом всех этих «обоснований» стало то, что логика из части философии превратилась в часть математики. В 1921 году Витгенштейн в «Логико-философском трактате» цитирует Фреге и Рассела и утверждает, что философия должна заниматься исключительно вопросами понимания естественного языка (потому что больше от нее ничего не осталось):

Цель философии — логическое прояснение мыслей. Философия не теория, а деятельность. Философская работа состоит по существу из разъяснений. Результат философии — не некоторое количество «философских предложений», но прояснение предложений. Философия должна прояснять и строго разграничивать мысли, которые без этого являются как бы темными и расплывчатыми.

Логика, превратившись из «общей» науки о рассуждениях в математическую теорию в первой половине XX достигла больших успехов, пытаясь объяснить методы рассуждений в математике. Теоретические работы по теории вычислимости, выросшие из упомянутых выше теорем Геделя, оказались очень «к месту», когда в середине 40-х годов появились первые программируемые электронно-вычислительные машины. Создавались они не только инженерами, но и математиками (Джон фон Нейман, в честь которого названа «стандартная» архитектура ЭВМ, известен своими работами по функциональному анализу, Алан Тьюринг занимался как раз вопросами вычислимости) и очень быстро превратились из инструмента для расчетов в нечто более сложное.