Глибоке посилання, що прирівнює математичні докази та комп’ютерні програми | Журнал Quanta

Деякі наукові відкриття мають значення, оскільки вони відкривають щось нове — наприклад, подвійну спіральну структуру ДНК або існування чорних дір. Однак деякі відкриття є глибокими, оскільки вони показують, що дві старі концепції, які колись вважалися різними, насправді є однаковими. Візьмемо рівняння Джеймса Клерка Максвелла, які показують, що електрика та магнетизм є двома аспектами одного явища, або зв’язок загальної теорії відносності гравітації з викривленим простором-часом.

Листування Каррі-Говарда робить те саме, але в більшому масштабі, пов’язуючи не просто окремі поняття в одній галузі, а цілі дисципліни: Інформатика та математична логіка. Також відомий як ізоморфізм Каррі-Говарда (термін, що означає існування певної однозначної відповідності між двома речами), він встановлює зв’язок між математичними доказами та комп’ютерними програмами.

Простіше кажучи, листування Каррі-Говарда стверджує, що два поняття з інформатики (типи та програми) еквівалентні, відповідно, пропозиціям і доказам — поняттям з логіки.

Одним із розгалужень цього листування є те, що програмування — яке часто розглядається як особисте ремесло — підноситься до ідеалізованого рівня математики. Написання програми — це не просто «кодування», це стає актом доведення теореми. Це формалізує процес програмування та надає способи математичних міркувань щодо правильності програм.

Листування названо на честь двох дослідників, які незалежно один від одного виявили його. У 1934 році математик і логік Хаскелл Каррі помітив подібність між функціями в математиці та зв’язком імплікації в логіці, який приймає форму висловлювань «якщо-тоді» між двома пропозиціями.

Натхненний спостереженням Каррі, математичний логік Вільям Елвін Говард у 1969 році виявив більш глибокий зв’язок між обчисленнями та логікою, показавши, що запуск комп’ютерної програми дуже схожий на спрощення логічного доказу. Під час виконання комп’ютерної програми кожен рядок «оцінюється» для отримання єдиного результату. Подібним чином у доказі ви починаєте зі складних тверджень, які можна спростити (усунувши зайві кроки, наприклад, або замінивши складні вирази простішими), доки не прийдете до висновку — більш стислого та стислого твердження, отриманого з багатьох проміжних тверджень. .

Хоча цей опис передає загальний зміст відповідності, щоб повністю зрозуміти його, нам потрібно дізнатися трохи більше про те, що інформатики називають «теорією типів».

Почнемо з відомого парадоксу: в одному селі живе перукар, який голить усіх чоловіків, які не голяться самі, і тільки їх. Перукар голиться сам? Якщо відповідь ствердна, то він не повинен голитися сам (оскільки він голить лише тих чоловіків, які не голяться самі). Якщо відповідь ні, то він повинен поголитися сам (тому що він голить усіх чоловіків, які не голяться самі). Це неофіційна версія парадоксу, який відкрив Бертран Рассел, намагаючись встановити основи математики за допомогою концепції під назвою множини. Тобто неможливо визначити множину, яка містить усі множини, які не містять самих себе, не зіткнувшись із протиріччями.

Щоб уникнути цього парадоксу, як показав Рассел, ми можемо використовувати «типи». Грубо кажучи, це категорії, конкретні значення яких називають об'єктами. Наприклад, якщо існує тип під назвою “Nat”, що означає натуральні числа, його об’єктами є 1, 2, 3 і так далі. Дослідники зазвичай використовують двокрапку для позначення типу об’єкта. Число 7 цілого типу можна записати як «7: ціле». У вас може бути функція, яка бере об’єкт типу A та викидає об’єкт типу B, або функція, яка об’єднує пару об’єктів типу A та B у новий тип, який називається «A × B».

Таким чином, один із способів вирішення парадоксу полягає в тому, щоб помістити ці типи в ієрархію, щоб вони могли містити лише елементи «нижчого рівня», ніж вони самі. Тоді тип не може містити сам себе, що дозволяє уникнути самопосилання, яке створює парадокс.

У світі теорії типів доказ істинності твердження може виглядати інакше, ніж ми звикли. Якщо ми хочемо довести, що ціле число 8 є парним, тоді потрібно показати, що 8 справді є об’єктом певного типу, який називається «парним», де правило приналежності ділиться на 2. Після перевірки того, що 8 ділиться 2, ми можемо зробити висновок, що 8 дійсно є «мешканцем» типу Even.

Каррі та Говард показали, що типи принципово еквівалентні логічним пропозиціям. Коли функція «населяє» тип — тобто, коли ви можете успішно визначити функцію, яка є об’єктом цього типу — ви фактично показуєте, що відповідна пропозиція істинна. Таким чином, функції, які приймають вхід типу A і дають вихід типу B, позначаються як тип A → B, повинні відповідати імплікації: «Якщо A, то B». Наприклад, візьмемо вислів «Якщо йде дощ, значить земля мокра». У теорії типів ця пропозиція буде змодельована функцією з типом «Дощ → GroundIsWet». Формулювання, що виглядають по-різному, фактично математично однакові.

Як би абстрактно не звучав цей зв’язок, він не лише змінив уявлення практикуючих математиків та інформатики про свою роботу, але й призвів до кількох практичних застосувань в обох сферах. Для інформатики вона забезпечує теоретичну основу верифікації програмного забезпечення, процесу забезпечення коректності програмного забезпечення. Формуючи бажану поведінку в термінах логічних пропозицій, програмісти можуть математично довести, що програма поводиться, як очікувалося. Він також забезпечує міцну теоретичну основу для розробки потужніших функціональних мов програмування.

А для математики листування призвело до народження доведення помічників, які також називаються інтерактивними засобами доказування теорем. Це програмні інструменти, які допомагають у побудові формальних доказів, наприклад Coq і Lean. У Coq кожен крок доказу є, по суті, програмою, а достовірність доказу перевіряється за допомогою алгоритмів перевірки типу. Математики також використовували помічники з доведення — зокрема, Лін теорема доказ — формалізувати математику, яка передбачає представлення математичних концепцій, теорем і доказів у строгому форматі, який можна перевірити комп’ютером. Це дозволяє інколи неформальну мову математики перевіряти комп’ютерами.

Дослідники все ще досліджують наслідки цього зв’язку між математикою та програмуванням. Оригінальне листування Каррі-Говарда об’єднує програмування з різновидом логіки, яка називається інтуїціоністською логікою, але виявилося, що інші типи логіки також можуть піддаватися такому об’єднанню.

«Протягом сторіччя, що минуло після відкриття Каррі, ми виявляємо все більше і більше випадків, коли «логічна система X відповідає обчислювальній системі Y», — сказав він. Майкл Кларксон, комп’ютерний науковець Корнельського університету. Дослідники вже пов’язали програмування з іншими типами логіки, такими як лінійна логіка, яка включає поняття «ресурси», і модальна логіка, яка має справу з поняттями можливості та необхідності.

І хоча це листування носить імена Каррі та Говарда, вони аж ніяк не єдині, хто її знайшов. Це свідчить про фундаментальний характер листування: люди помічають його знову і знову. «Здається, невипадково існує глибокий зв’язок між обчисленням і логікою», — сказав Кларксон.