Написание кода как математическое доказательство

Споры о том, нужна программисту математика или нет, вероятно, не утихнут никогда. Существует миллион мнений за и против, но сегодня речь пойдет вовсе не об этом. Предлагаем вашему вниманию адаптированный перевод материала Спиро Сидериса (Spiro Sideris) в котором он рассуждает, как можно написать код программы, следуя логике математических доказательств. Когда я начинал программировать, мне всегда было интересно рассмотреть связь формальной математики и процесса написания кода. Из математики мы узнали, как нужно строить доказательства, то есть как, исходя из набора аксиом и определений, можно логически построить истинные утверждения, чтобы доказать некую гипотезу. После доказательства гипотеза становится теоремой и ее можно использовать для доказательства других гипотез. Такая цепочка доказательств и превращений из гипотез в теоремы чем-то похожа на последовательность шагов при разработке программного обеспечения. Мы начинаем с множества определений (условные операторы, циклы и так далее), а также ранее доказанных теорем (стандартные библиотеки, сторонние библиотеки и так далее). Затем пытаемся объединить эти элементы для решения своих задач. Сочетание утверждений в программном обеспечении выполняется буквально. Каждая строка компьютерного кода оценивается как логическая последовательность инструкций во время работы программы. Следующая цитата из учебника по основам математического анализа описывает сравнение между написанием доказательств и эссе. Стивен Эббот, автор книги «Понимание анализа» пишет: Именно это сравнение построения доказательств и написания эссе лежит в основе моего представления об аналогии между написанием доказательств и написанием кода. Прежде, чем мы начнем, хочу пояснить, что я не пытаюсь убедить читателя «математизировать» код в духе Дональда Кнута. Я просто хочу использовать концепции построения хороших доказательств для написания качественного кода. В этом материале я опишу несколько полезных примеров доказательств, разбор которых, возможно, поможет улучшить код программы. Рассмотрим один из них. Предположим, нам необходимо доказать, что сумма двух последовательных целых чисел всегда нечётна. Как было указано раннее, мы будем стремиться комбинировать последовательность логических утверждений, начиная с определений или ранее доказанных теорем, для получения нашего доказательства. Рассмотрим пример. Теорема Если a и b — последовательные целые числа, то их сумма (a + b) — всегда является нечётным целым числом. Доказательство Допустим, a и b — последовательные целые числа. По определению нечетное число записывается как 2k+1, где k – любое целое число. Поскольку a и b являются последовательными числами, мы можем записать: b=a+1. Таким образом, их сумма (a + b) может быть записана как:

a+b = a+(a+1) = a+a+1 = 2a+1

Так как a — целое число, следовательно, 2a+1 — нечетное число. Таким образом, и сумма (a + b) = 2a+1 — нечетное число. Что и требовалось доказать.

Знай свою целевую аудиторию

Разберем некоторые важные части нашего доказательства и некоторые предположения относительно вас, читателей этого материала. Во-первых, я предположил, что читатели этой статьи понимают, что такое целые числа (из-за того, что речь идет о программировании). Во-вторых, я предположил, что читателям будет удобно работать с алгеброй целых чисел (поскольку операции с целыми числами зачастую интуитивно понятны). Но, вместо того, чтобы предположить, что читатель знает формальное определение нечетных целых чисел, я ввел его определение вместе с доказательством, чтобы обеспечить согласованный набор понятий между автором и читателями. С каждым следующим предположением и определением я создавал доказательство с использованием строго истинных утверждений и успешно доказал теорему. Создание необходимых предположений об уровне аудитории всегда будет необходимым шагом при написании формального доказательства, поскольку это можно сделать по-разному. Например, если предположить, что читатели изначально знали формальные определения четных и нечетных чисел, я мог бы их не приводить в тексте, и тогда доказательство выглядело бы очень коротким. Вместо этого, я предположил, что кто-то из моих читателей не посещал занятий по математике, или это было так давно, что он уже забыл все определения. Хороший автор, неважно идет речь о написании математического доказательства или остросюжетного романа, всегда должен понимать, для кого он пишет, какие люди станут его целевой аудиторией. Если речь идёт об учебнике по основам математики для младшей школы, то материал будет восприниматься легче, если указать в нем основные определения. Если же речь идет о статье в специализированный математический журнал, автор, разумеется, может опустить элементарные определения, по праву полагая, что его целевой аудиторией являются специалисты в данной области. Понимание целевой аудитории поможет правильно сформулировать доказательство и донести его читателям. Мы можем построить похожую схему не только при составлении доказательств, но также при написании программного обеспечения. Когда большинство разработчиков пишет программу, в основном они стараются написать исполняемый код. Однако если код выполняется, это не гарантирует его читабельности и понятности. Скорее всего, вы прекрасно разберётесь в своей (или чужой) небольшой программке. Но что, если вам придётся разбираться в тоннах чужого кода в миллион строк? Чтобы написать понятный код, всегда задавайте вопрос о том, кто ваша целевая аудитория. Каков их уровень подготовки? Какими базовыми знаниями они должны обладать, чтобы прочитать написанную вами функцию. Кроме того, существуют различия в семантике между языками программирования, поэтому знание лучших практик и стилей языков программирования, гарантируют, что ваш код получится легко читаемым для разработчиков, специализирующихся в этом языке программирования. Когда вы собираетесь писать следующую функцию, помните о словах, которые вы используете для описания ваших переменных и методов. Например, если вы назовёте переменную minimum для обозначения минимальной границы некоего множества, большинство поймёт, что вы имеете в виду. А вот при использовании для той же переменной более специфическое, хоть и правильное, infimum, вас поймут либо математики, либо те, кто недавно изучал начала анализа. Обратите внимание на то, как вы структурируете свои комментарии и код. Создание руководства по стилю проекта или соблюдение уже существующего руководства, также поможет облегчить понимание вашего кода и «джунам», и опытным разработчикам. Если вы будет следовать этому принципу, ваш код будет легко читаться и уменьшит усилия ваших последователей, которые будут также разбираться в вашем коде.

Пишите четко и кратко

Сегодня во время написания кода мы имеем возможность проверять код с помощью встроенных в IDE и текстовые редакторы инструментов. В случае нарушения валидности, хорошая IDE выдаст нам ошибку компиляции или исключение во время выполнения (runtime exception). Конструирование доказательств, увы, не предполагают таких проверок. Проверять доказательство математика на валидность будет читатель или студент. Чтобы убедить читателя в верности полученного результата, автор доказательства должен его сформулировать наиболее понятным и кратким образом. Долгие и бессвязные размышления о сущности бытия не смогут донести до читателя смысл доказательства. Я предлагаю писать код так, чтоб он не просто был исполнимым, но также был прозрачным — убеждал читателя в истинности утверждений. Как и хорошее доказательство, код должен быть написан внимательно и тщательно. Мы должны обязательно сократить избыточные данные, которые не дают читателю дополнительную выгоду, а только запутывают его. Зачем писать сто строк кода, если для выполнения задачи достаточно восемьдесят, шестьдесят или еще меньше? Мертвый код, как и мертвые фразы, чрезмерно напрягают читателя. Чаще всего решение проблемы займет много времени и сил. Вернитесь и попытайтесь отредактировать написанное вами, упростив его для понимания. При этом я не призываю вас «уменьшить количество кода» во всем проекте. Крайности не уместны, и в этом случае они также принесут больше вреда, чем пользы. Иногда создание новой, потенциально избыточной переменной, может, наоборот, упростить код для понимания.

Проверьте все варианты

Очень часто доказательство гипотез начинается с использования частного примера, а затем происходит перенос на общий случай. В приведённой выше теореме о последовательных числах мы можем взять для проверки два целых последовательных числа 2 и 3, действительно, их сумма 5 нечетное число. Используя этот пример, мы можем экстраполировать и посмотреть, как данный шаблон применяется далее. Конечно, мы ищем общее решение, но это не означает, что мы не можем использовать практические примеры для получения необходимого результата. Однако, сосредоточив свое внимание только на практических примерах, мы можем допустить ошибку. Иногда мы можем забыть проверить конкретный случай, который нарушает общее решение. В нашем примере мы рассмотрели два положительных целых числа. А как же отрицательные числа? Что будет если мы используем нейтральный элемент (в случае с integer, это 0)? К счастью, в данном конкретном примере доказательство останется верным и для отрицательных чисел, и для нейтрального элемента. К сожалению, это не всегда так. Простой школьный пример. Предположим, нам необходимо доказать, что каждый квадратный корень целого числа существует в действительных числах. Если вы пробовали взять для примера √2, √4 или даже √0, то считаете, что результат верен. Однако, что же будет если мы попробуем найти квадратный корень любого отрицательного числа? Фактически, математикам пришлось создать целый новый набор чисел — комплексных чисел — чтобы найти квадратные корни отрицательных целых чисел. Включив в рассмотрение, казалось бы, простой вариант отрицательных чисел, история математики изменилась. И это далеко не единственный случай, когда математика расширялась, дабы соответствовать новым требованиям. В программном обеспечении варианты, при которых программа работает иначе, мы выделяем в группу частных случаев и называем их edge case (краевые случаи). Разработчики программного обеспечения регулярно сталкиваются с такими краевыми случаями, особенно при написании функции, которая вводит пользовательский ввод: необходимо обеспечить её работоспособность, если пользователь не ввёл данных, или ввёл их слишком много, или эти данные не такие, как ожидалось… Фантазия иных пользователей безгранична. Инженеры-программисты регулярно жалуются на краевые случаи и многие из них ими пренебрегают, что приводит к сбоям в работе программы. Хотя при именовании краевых случаев, мы пытаемся обозначить их как «редкие», на практике они встречаются не так уж и редко, и их обязательно нужно учитывать. Разработчики не всегда обрабатывают краевые случаи в своих предложениях, и вот почему:

1. Они не учли краевой случай, поскольку не знают, что такой вариант возможен;
2. Они знают, что такой вариант возможен, но не пишут код, который с ним взаимодействует.

Первый пункт относится к ряду трудноразрешимых задач. Тем не менее, как у математиков есть рецензенты доказательств, у разработчиков есть code review (обзор кода, в русскоязычных странах обычно так и говорят — код ревью) для проверки тестовых примеров. Существуют способы тестирования кода с помощью модульных тестов, интеграционных тестов или проверки модели, например, TLA+. Кроме того, нам часто помогает личный опыт, чтобы заранее узнать дополнительную информацию о вариантах потенциальных тестов. Чем больше программ вы пишете, тем чаще вам придется сталкиваться с такими случаями, и ваши знания могут быть использованы в более поздних разработках. Возвращаясь к нашим двум причинам, замечу, что если первый пункт — это проблема незнания, то второй — куда более коварен. Это происходит, если разработчик знает о возможности возникновения краевого случая, но не пытается разобраться с вариантами защиты от него. Это может быть связано либо с ограничением сроков проекта, спешкой или обычной ленью. Каждая попытка рационализации связана с необходимостью увеличить количество времени для работы над проектом или куском кода с ошибкой. Чего в принципе не должно быть в других случаях. Мало того, что это плохо отражается на программном обеспечении, которое вы создаете, логически неверно игнорировать такие случаи. И хотя я понимаю чувства разработчика, которому необходимо затратить дополнительное время для поиска новой проблемы, я считаю, что нельзя сидеть сложа руки пока проблема не будет решена. Если разработчик создаст тесты, которые учтут краевые случаи, он получит сильный код, который будет работать чётко, как верное доказательство математической теоремы.

Подведем итоги

В данном материале я постарался найти три наиболее подходящих соответствия между написанием математических доказательств и написанием программного кода. Конечно, эти три варианта не единственны, но мне кажется они наиболее полезны для написания программы. Мир математики и мир программирования находятся куда ближе друг от друга, чем кажется большинству людей. И изучение математики может вам помочь в будущем программировать лучше. Если тема этой статьи показалась вам интересной, возможно, стоит попробовать открыть простейшую книгу о доказательствах и прошерстить её. Надеюсь, что удовольствие от доказанной с нуля теоремы, для вас, как и для меня, будет сравнимо с удовольствием от написания хорошей программы.