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

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

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

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

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

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

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

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

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

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

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

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

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