Применение информационных технологий в математике

БЕЛОРУССКИЙ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ

 

 

 

 

 

 

 

 

 

 

 

Выпускная работа по 
«Основам информационных технологий»

 

 

 

 

 

 

 

Аспирант кафедры дифференциальных уравнений Зорин Евгений Владимирович

Руководители:

Член-корреспондент  НАН Б, профессор Берник Василий Иванович,

ст. преподаватель  Кожич Павел Павлович

 

 

 

Минск – 2007 г.

Оглавление

 

 

  БЕЛОРУССКИЙ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ

 

 

 

 

 

 

 

 

 

Реферат

по теме 
«Применение информационных технологий в математике»

 

 

 

 

 

 

 

Аспирант кафедры дифференциальных уравнений

Зорин Евгений  Владимирович

Руководители:

Член-корреспондент  НАН Б, профессор Берник Василий Иванович,

ст. преподаватель  Кожич Павел Павлович

 

 

Минск – 2007 г

 

Введение

 

Тест  Тьюринга — тест, предложенный Аланом Тьюрингом в 1950 г. в статье «Вычислительные машины и разум» (Computing machinery and intelligence) для проверки, является ли компьютер разумным в человеческом смысле слова. Тьюринг предложил тест, чтобы заменить бессмысленный, по его мнению, вопрос «может ли машина мыслить?» на более определенный.

Тест должен проводиться следующим образом. Судья (человек) переписывается на естественном языке с двумя собеседниками, один из которых — человек, другой — компьютер. Если судья не может надежно определить, кто есть кто, считается, что компьютер прошел тест. Предполагается, что каждый из собеседников стремится, чтобы человеком признали его. Чтобы сделать тест простым и универсальным, переписка сводится к обмену текстовыми сообщениями.

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

(материал из Wikipedia)

 

В программу  научной конференции по кибернетике и информатике, которая пройдет в июле этого года во Флориде, включили бессмысленный доклад, состоящий из случайно подобранного текста, таблиц и диаграмм, сообщает BBC News. Эта работа, озаглавленная "Рутер: Методология типичной унификации точек доступа и резервирования", была написана компьютерной программой-генератором случайных текстов.

(новостная лента, апрель 2005 года, http://www.lenta.ru/news/2005/04/16/hoax/)

 

Компьютеры  играют все большую роль в современном  мире. Они заменяют человека повсюду, где требуется методичное, кропотливое, четкое и быстрое руководство происходящими процессами и молниеносное реагирование на происходящие события. Вместе с тем до сих пор остается нерешенной проблема алгоритмизации творческих процессов. Да, компьютеры пишут стихи (одну из программ для этого можно скачать вот здесь: http://lleo.aha.ru/soft/lleo_dip.htm), рисуют абстрактные картины, но люди по прежнему интересуются такими произведениями только исходя из того, что они созданы необычным автором. Процесс «инсайта», творческого создания чего-либо нового, до сих пор не удается по-настоящему алгоритмизировать, несмотря на огромный интерес который вызывает этот вопрос для людей и (как следствие) огромные усилия прикладываемые в этой области.

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

 

Часть 1. Доказательство теорем при помощи коспьютеров.

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

 

Как известно, оказалось  что существуют естественные ограничения для реализации такой программы наиболее известным из которых является теорема Геделя о неполноте (если формальная система включает в себя аксиомы Пеано, то есть аксиоматику натуральных чисел, то в такой системе либо можно для какого-то утверждения P доказать как P, так и отрицание P, либо существует какое-то утверждение Q, которое можно сформулировать в этой системе, которое нельзя ни доказать, ни опровергнуть (то есть доказать обратное) в рамках этой системы).

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

Как было доказано в 1936-ом году Черчем, натуральные числа (с аксиоматикой Пеано) являются неразрешимой формальной системой. На первый взгляд несколько удивительно, но, как было показано Тарским (в начале 30-х годов, хотя из-за войны работы вышла только в 1948-м), действительная арифметика является разрешимой. Создав свою аксиоматику Евклидовой геометрии (которая, конечно же, соответствует естественному пониманию об этом объекте) Тарский доказал что и эта формальная система является разрешимой. В то же время уже проективная геометрия оказалась неразрешимой.

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

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

Здесь стоит  отметить, что многие задачи математики на том или ином этапе (возможно, после долгой творческой работы над ними людей) сводятся к утверждениям в действительной арифметике, даже если изначально они возникли в алгебре или теории чисел. В то же время, статья Тарского «A Decision Method for Elementary Algebra and Geometry» дает хороший алгоритм сведения любой задачи в действительной арифметике к вычислению конкретной формулы (может быть довольно сложной, но более чем посильной для современных компьютеров). Собственно, там приводится алгоритм того как преобразовать утверждение в действительной арифметики начинающееся с квантора существования к другому утверждению, уже не содержащему такового, и как несложно видеть такими преобразованиями можно свести любое утверждение содержащее много кванторов существования и всеобщности (и любые логические операции) к логической формуле без кванторов, которую потом можно проверить при всех значениях логических переменных.

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

К сожалению, никакая  из известных автору программ «автоматического доказательства теорем», включая и те что носят имя Тарского (например, вот этот пакет для Mathematica http://www.di.unito.it/~stefano/Mathematica-TarskiGames.nb), не выполняет большего чем преобразования логических выражений (точнее говоря, все что умеет делать автор с логическими выражениями посредством известных ему программ, это вычислять их значения, проверять всегда ли они истинны и т. пр.), процесс «сокращения кванторов» если где-то он и реализован, автором не обнаружен (поиск проводился достаточно долгий и интерес к объекту поиска наличествовал).

 

Часть 2. Доказательство теорем при помощи компьютеров.

Хотя автоматическое доказательство теорем пока имеет весьма ограниченное применение в «чистой» математике, компьютеры оказывают неоценимую помощь человеку в другом ее аспекте, в конкретных вычислениях. Собственно говоря, это и являлось основной мотивацией при их создании, можно сказать что «это их основное предназначение». Для математиков докомпьютерной эры вычисления являлись обычно тяжелой необходимостью, которая редко кому доставляла удовольствие. Широко известен следующий отрывок из письма  (20 января 1903 года) Альберта Эйнштейна его будущей жене, тогда Милеве Марич

..Если  хочешь замужества, ты должна  будешь согласиться на мои  условия, вот они:      

 Во-первых, ты  будешь заботиться о моей одежде  и постели.      

 Во- вторых, будешь  приносить мне трижды в день  еду в мой кабинет,      

 В-третьих,  ты откажешься от всех личных контактов со мной, за исключением тех, которые необходимы для соблюдения приличий в обществе,      

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

 В-пятых, без  слов протеста ты будешь выполнять для меня научные расчеты,      

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

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

 

В наши дни существует большое  количество программ для проведения научных расчетов (возможно, это внесло некий вклад в снижение популярности института брака). Существуют как мультифункциональные пакеты, например Mathematica, Maple, MathLab, MathCad так и весьма специализированные, например Macaulay (в настоящее время Macaulay 2, применяется для расчетов в коммутативной алгебре), Statistica и GAP (Groups, Algorithms and Programming).

Часть 2. Некоторые программные пакеты предназначенные для математических расчетов

Mathematica

Минимальные требования к системе (для версии Mathematica 5):

• процессор Pentium II или выше;
• 128 Мбайт оперативной памяти (рекомендуется 256 Мбайт или больше);
• 400-550 Мбайт дискового пространства;
• операционные системы: Windows 98/Me/ NT 4.0/2000/2003 Server/2003x64/XP/XP x64.

 

Пакет Mathematica, разработанный компанией Wolfram Reseach Inc., объединяет возможности аналитических и численных вычислений, визуализации и документирования в единой среде. Mathematica позволяет производить существенные расширения в системе и имеет развитые возможности связи с Java и XML. Система предлагает средства для линейного программирования, статистики, решения задач оптимизации, комбинаторики и теории графов.

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

Пакет состоит  из двух частей – ядра, которое производит вычисления, выполняя заданные команды, и интерфейсного процессора, который определяет внешнее оформление и характер взаимодействия с пользователем и системой. В системах класса Mathematica ядро математических операций машинно-независимое. Поэтому оно позволяет переносить систему на различные компьютерные платформы.

Ядро сделано  достаточно компактным для того, чтобы можно было очень быстро вызвать из него любую функцию. Для расширения набора функций служат библиотека (Library) и набор пакетов расширения (Add-on Packages). Пакеты расширений готовятся на собственном языке программирования систем Mathematica и являются главным средством для развития возможностей системы и их адаптации к решению конкретных классов задач пользователя.

Интерфейс пакета строится из нескольких базовых понятий: тетрадь (Notebooks), ячейка (Cell) и палитра (Palletes). Тетрадью называется файл, с которым работает пользователь. В нем создаются и вычисляются формулы, строятся графики и таблицы. При желании, в тетради можно даже проиграть звуковой файл или фильм. Тетрадь состоит из ячеек. Все информация, которая есть в тетради, хранится в его ячейках. Как только в пустом новом файле набирается хотя бы один символ, Mathematica создаст для него ячейку. Все ячейки можно разделить на три типа: ячейки ввода – в них задаются команды (формулы), которые будут вычислены; ячейки результата, в которых выводятся результаты вычислений; другие ячейки – ячейки с текстом, заголовки и все остальное, что вводит пользователь и вычислять не надо. Необходимые числа, буквы, символы можно вводить как с клавиатуры с помощью комбинаций клавиш, так и с помощью многочисленных палитр. Палитры содержат окна с кнопками, которые выполняют различные действия: от добавления греческой буквы, до раскрытия скобок в алгебраическом выражение. Если возникают какие - то вопросы, то можно обратиться к встроенной электронной справочной системе Help, которая содержит очень качественное описание функций с примерами, а также учебник.