Глубокая ссылка, уравнивающая математические доказательства и компьютерные программы | Журнал Кванта

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

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

Проще говоря, переписка Карри-Ховарда утверждает, что два понятия из информатики (типы и программы) эквивалентны соответственно утверждениям и доказательствам — понятиям из логики.

Одним из последствий этого соответствия является то, что программирование — часто рассматриваемое как личное ремесло — возводится до идеализированного уровня математики. Написание программы — это не просто «кодирование», это становится актом доказательства теоремы. Это формализует процесс программирования и дает возможность математически рассуждать о правильности программ.

Переписка названа в честь двух исследователей, которые независимо друг от друга ее обнаружили. В 1934 году математик и логик Хаскелл Карри заметил сходство между функциями в математике и отношением импликации в логике, которое принимает форму утверждений «если-то» между двумя предложениями.

Вдохновленный наблюдением Карри, математический логик Уильям Элвин Ховард в 1969 году обнаружил более глубокую связь между вычислениями и логикой, показав, что выполнение компьютерной программы во многом похоже на упрощение логического доказательства. Когда компьютерная программа запускается, каждая строка «оценивается» для получения единственного результата. Точно так же в доказательстве вы начинаете со сложных утверждений, которые можно упростить (например, устраняя лишние шаги или заменяя сложные выражения более простыми), пока не придете к выводу — более сжатому и лаконичному утверждению, полученному из множества промежуточных утверждений. .

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

Начнем с известного парадокса: В деревне живет цирюльник, который бреет всех мужчин, которые не бреются сами, и только их. Парикмахер бреется сам? Если ответ «да», то ему нельзя бриться самому (потому что он бреет только мужчин, которые сами не бреются). Если ответ отрицательный, то он должен побриться сам (потому что он бреет всех мужчин, которые не бреются). Это неформальная версия парадокса, открытого Бертраном Расселом, когда он пытался обосновать основы математики с помощью понятия, называемого множествами. То есть невозможно определить множество, содержащее все множества, не содержащие самих себя, не столкнувшись с противоречиями.

Чтобы избежать этого парадокса, как показал Рассел, мы можем использовать «типы». Грубо говоря, это категории, конкретные значения которых называются объектами. Например, если существует тип под названием «Nat», означающий натуральные числа, его объектами будут 1, 2, 3 и т. д. Исследователи обычно используют двоеточие для обозначения типа объекта. Число 7 целочисленного типа можно записать как «7: целое число». У вас может быть функция, которая принимает объект типа A и выдает объект типа B, или функцию, которая объединяет пару объектов типа A и типа B в новый тип, называемый «A × B».

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

В мире теории типов доказательство истинности утверждения может выглядеть иначе, чем мы привыкли. Если мы хотим доказать, что целое число 8 четное, тогда нам нужно показать, что 8 действительно является объектом определенного типа, называемого «Четный», где правило членства делится на 2. После проверки того, что 8 делится по 2 можно сделать вывод, что 8 действительно является «жителем» типа Эвен.

Карри и Ховард показали, что типы по своей сути эквивалентны логическим предложениям. Когда функция «населяет» тип — то есть когда вы можете успешно определить функцию, которая является объектом этого типа — вы эффективно показываете, что соответствующее предложение истинно. Таким образом, функции, которые принимают входные данные типа A и дают выходные данные типа B, обозначаемые как тип A → B, должны соответствовать импликации: «Если A, то B». Например, возьмем предложение «Если идет дождь, то земля мокрая». В теории типов это предложение будет моделироваться функцией типа «Дождь → GroundIsWet». Различные на вид формулы на самом деле математически одинаковы.

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

А для математики переписка привела к рождению корректоры, также называемые интерактивными средствами доказательства теорем. Это программные инструменты, которые помогают в построении формальных доказательств, такие как Coq и Lean. В Coq каждый шаг доказательства по существу представляет собой программу, а достоверность доказательства проверяется с помощью алгоритмов проверки типов. Математики также использовали помощники для доказательства, в частности, Средство доказательства теорем бережливого производства — формализовать математику, что предполагает представление математических концепций, теорем и доказательств в строгом, проверяемом компьютером формате. Это позволяет компьютерам проверять иногда неформальный язык математики.

Исследователи все еще изучают последствия этой связи между математикой и программированием. Исходное соответствие Карри-Ховарда объединяет программирование с разновидностью логики, называемой интуиционистской логикой, но оказывается, что таким объединениям могут быть подвержены и другие типы логики.

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

И хотя эта переписка носит имена Карри и Говарда, они ни в коем случае не единственные, кто ее обнаружил. Это свидетельствует о фундаментальном характере переписки: люди замечают ее снова и снова. «Похоже, не случайно существует глубокая связь между вычислениями и логикой», — сказал Кларксон.