Написання коду як математичний доказ

Суперечки про те, чи потрібна програмісту математика чи ні, ймовірно, не вщухнуть ніколи. Існує мільйон думок за і проти, але сьогодні йтиметься зовсім не про це. Пропонуємо до вашої уваги адаптований переклад матеріалу Спіро Сідеріса (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+. Крім того, нам часто допомагає особистий досвід, щоб заздалегідь дізнатися про додаткову інформацію про варіанти потенційних тестів. Чим більше програм ви пишете, тим частіше вам доведеться стикатися з такими випадками, і ваші знання можуть бути використані у пізніших розробках. Повертаючись до наших двох причин, зауважу, що якщо перший пункт — це проблема незнання, то другий — значно підступніший. Це відбувається, якщо розробник знає про можливість виникнення крайового випадку, але не намагається розібратися з варіантами захисту від нього. Це може бути пов'язане або з обмеженням термінів проекту, поспіхом або звичайною лінню. Кожна спроба раціоналізації пов'язана з необхідністю збільшити кількість часу для роботи над проектом або шматком коду з помилкою. Чого, в принципі, не повинно бути в інших випадках. Мало того, що це погано впливає на програмне забезпечення, яке ви створюєте, логічно неправильно ігнорувати такі випадки. І хоча я розумію почуття розробника, якому необхідно витратити додатковий час для пошуку нової проблеми, я вважаю, що не можна сидіти склавши руки, поки проблема не буде вирішена. Якщо розробник створить тести, які врахують крайові випадки, він отримає сильний код, який працюватиме чітко як вірний доказ математичної теореми.

Підведемо підсумки

У цьому матеріалі я постарався знайти три найбільш відповідні відповідності між написанням математичних доказів та написанням програмного коду. Звичайно, ці три варіанти не єдині, але мені здається, вони найбільш корисні для написання програми. Світ математики і світ програмування знаходяться набагато ближче один від одного, ніж здається більшості людей. І вивчення математики може допомогти вам у майбутньому програмувати краще. Якщо тема цієї статті здалася вам цікавою, можливо, варто спробувати відкрити найпростішу книгу про докази та прошерстити її. Сподіваюся, що задоволення від доведеної з нуля теореми для вас, як і для мене, буде порівняно із задоволенням від написання гарної програми.