С давних пор я искал простое средство доказательства теорем: небольшой (скажем, ~ 1000 LOC) язык программирования, способный выражать и доказывать математические теоремы о собственных программах. Если бы у нас была такая вещь, разработчики по всему миру могли бы доказывать утверждения о коде, который они создают, и пользователи могли бы доверять этим утверждениям, не доверяя разработчикам. Этот поиск привел меня к множеству озарений и разочарований. Я пишу этот пост, чтобы подвести итоги своего пути. В конце я приведу ссылки на возможные реализации.

Что такое средство доказательства теорем и почему оно важно?

Предположим, мы пишем смарт-контракт, содержащий криптоактивы, и хотим убедить людей, что фактический баланс этого контракта всегда соответствует сумме балансов, хранящихся во внутреннем состоянии. С обычными языками это нужно делать либо с помощью тестов, которые не на 100% уверены, либо с помощью аудитов. К сожалению, вручную проанализировать все возможные состояния большой программы невозможно.

Вместо этого с помощью средства доказательства теорем мы могли бы просто опубликовать доказательство следующего утверждения: sum(state.user_balances) == state.balance. Поскольку это логическое доказательство, мы охватываем все возможные состояния. После того, как пользователь проверит это доказательство на своем компьютере, он будет уверен, что учет баланса смарт-контракта никогда не пойдет неправильно, независимо от того, насколько он сложен, без необходимости читать ни одной строчки его кода. Средства доказательства теорем существенно сокращают объем работы по аудиту с O(N) до O(1), где N представляет размер кода / сложность программы, и именно поэтому они имеют значение.

В чем проблема с существующими средствами доказательства теорем?

На рынке есть много устройств для доказательства теорем: Coq, Agda, Idris, Isabelle и многие другие. Но у большинства из них есть кое-что общее: они большие. Например, ядро ​​Coq содержит около 30 000 строк кода. Это проблема по двум основным причинам.

Во-первых, языковая реализация сама по себе не может проверить свою непротиворечивость, а это значит, что пользователи должны либо доверять ей, либо реализовывать другой язык для ее проверки; но тогда пользователи должны доверять этому. В конце концов, следует доверять коду хотя бы одного средства доказательства теорем. Любая незначительная ошибка в нем все сломает, позволив людям доказать ложные утверждения, что станет катастрофой для безопасности. На данный момент Coq очень стабилен, но мы никогда не можем быть уверены на 100%. Другие языки, такие как Agda и Idris, находятся в худшей ситуации, поскольку они по-прежнему часто обнаруживают ошибки, нарушающие их логическую последовательность; ищите ярлык false на их проблемах Github.

Во-вторых, большой размер означает, что их нелегко перенести или адаптировать под разные платформы или сценарии использования. Например, Coq несовместим с абстрактным алгоритмом, очень быстрым вычислителем функциональных сокращений. Чтобы сделать это так, нужно было бы изменить внутреннюю логику системы типов, но внести такие фундаментальные изменения в такую ​​огромную кодовую базу было бы практически невозможно. Точно так же Coq, Agda, Idris не будут работать изначально в браузере или на мобильном устройстве. Что, если мы хотим проверить доказательства на iPad? Конечно, его можно скомпилировать, но тогда нам нужно также убедиться, что компилятор не содержит ошибок (а это не так).

Ищете более простой инструмент доказательства теорем

Принимая во внимание эти проблемы, кажется естественным искать средство доказательства теорем как можно меньшего размера. Если бы у нас был, например, один с

Первый кандидат: Исчисление конструкций (CoC)

Первый кандидат - это Строительное исчисление (CoC). CoC - действительно очень простой инструмент для доказательства теорем; например, 400-JS-LOC-simple. Он чистый, элегантный и не похож на что-то придуманное человеком, как Agda, но вместо этого выглядит чем-то действительно естественным, например, константой Эйлера или лямбда-исчислением. Тем не менее, несмотря на свою простоту, он действует как средство доказательства теорем благодаря одной мощной функции: зависимым функциям. С их помощью CoC может реализовать абсолютно любой тип данных, о котором вы только можете подумать, и может подтвердить такие утверждения, как 2 + 2 == 4 или not(not(bool)) == id(bool). Самым популярным его воплощением, я считаю, является Morte Габриэля Гонсалеса. Если вам интересно, он написал несколько статей об этом, хотя в Википедии тоже есть хорошая рецензия. CoC сам по себе является частью семейства других простых языков, систем чистых типов.

В чем проблема с CoC?

Приведенные выше характеристики делают CoC идеальным кандидатом на то, что я искал. К сожалению, с этим связана огромная небольшая проблема: он не может доказать принцип индукции. Принцип индукции (по числам) гласит, что если у нас есть числовое свойство, которое мы хотим доказать, то, если мы докажем, 1. что это свойство выполняется для n = 0, 2. что, учитывая предположение, что это свойство выполняется для число k, оно также выполняется для k + 1, то мы можем заключить, что это свойство сохраняется для каждого числа n.

Например, предположим, что наше свойство - forall n: IsEven(n * 2) (или «двойное число любого числа четное»). Держится ли n = 0? Конечно, потому что 0 * 2 == 0, а это даже. Более того, учитывая предположение, что оно справедливо для k, верно ли оно для k + 1? Конечно, потому что 1. (k + 1) * 2 == 2k + 2, 2. 2k четно (в силу нашего предположения), 3. любое четное число плюс 2 четно. Таким образом, по принципу индукции мы можем заключить, что двойник каждого числа четный.

Невозможность вывести принцип индукции - огромная проблема, потому что индуктивные доказательства подобны циклам for в математике, без них далеко не уйти. Например, хотя CoC может доказать 2 + 2 == 4, он не может доказать 2 + 3 != 4. На самом деле ничего более сложного сделать нельзя. Он не может доказать коммутативность (a + b = b + a), ассоциативность (a + (b + c) == (a + b) + c), он даже не может доказать, что id(x) == x. Учитывая, что CoC не может доказать эти простые математические утверждения, очевидно, что он не может доказать сложные программные инварианты.

Решение: «заплатка» CoC.

Из-за этой проблемы люди начали исправлять CoC, расширяя его новыми примитивами, которые позволяли бы проводить индуктивные рассуждения. Так, например, родился Coq: он взял за основу CoC и добавил собственную систему для индуктивных типов данных. Получившаяся система CoIC (исчисление индуктивных построений) - это то, что реализует ядро ​​Coq. Однако есть проблема: индуктивные типы данных сложны. Если CoC может быть реализован в ~ 400 LOC, я был бы удивлен, если бы CoIC могло быть менее чем в 2000. Например, ядро ​​Coq имеет ›30 000 LOC. Таким образом, этот подход сложен, подвержен ошибкам и непереносим. Более того, это привело к более высоким проблемам, таким как несовместимость HoTT. Лично мне ясно, что жесткое кодирование такой системы типов данных - не лучший подход, когда мы заботимся о простоте и переносимости.

Не все на поле согласны с этим утверждением, но некоторые явно согласны. Один особенно вызвал у меня интерес. В прошлом году вышла статья Синтаксис и семантика седиллы. В нем представлена ​​теория типов, называемая исчислением зависимых исключений лямбда (CDLE), которая, как и CoIC, расширяет CoC новыми конструкциями, но, в отличие от него, вместо прямого добавления индуктивных типов данных добавляет всего несколько простых и естественных конструкций, которые могут , затем можно использовать для реализации индуктивных типов данных. Около года назад мне удалось реализовать его ядро ​​Cedille-Core чуть менее чем за 1000 мест. Это в 30 раз меньше по сравнению с Coq! Это впервые дало мне ощущение прогресса в моих давних поисках. Но это еще не конец.

Проблема с Cedille

Как только я закончил реализацию Cedille-Core, я осознал его проблему: хотя сам базовый язык прост, код, написанный на нем, - нет. В качестве примера ниже представлена ​​реализация натуральных чисел и доказательство принципа индукции на Cedille-Core. Вам не нужно разбираться в этом коде, просто обратите внимание на его размер. Однако полная проверка типов доступна в Gist, если хотите.

Это огромный. Для сравнения, это эквивалентное доказательство индукции на Agda:

От 7 до 67 строк кода, это немалая разница. Основная проблема Cedille заключается в том, что, хотя сам язык чрезвычайно прост из-за отсутствия собственных индуктивных типов данных, эта сложность проявляется, когда вам нужно использовать их в своем коде. Учитывая, что типы данных являются основой функционального программирования, работать напрямую с Cedille-Core гораздо менее практично, чем с Agda, Idris и им подобными. Представьте, что вам нужно написать 70 строк кода всякий раз, когда вы хотите определить небольшую структуру C?

На первый взгляд я предположил, что эту проблему можно решить, расширив язык с помощью синтаксических сахаров для собственных типов данных. То есть пользователь набирает что-то похожее на версию Agda, которая затем расширяется до версии Cedille-Core. Это сделало бы язык более практичным для работы. Но возникает вопрос: являются ли эти синтаксические сахара частью языка? Если да, то размер языка соответственно увеличивается. Если нет, то что делать тем, кому нужно прочитать доказательства? В конце концов, синтаксические сахара теряются после расширения. Распространяемым кодом по-прежнему будет Cedille-Core, поэтому люди, проверяющие его доказательства, увидят более длинную версию. Хотя средства доказательства теорем позволяют отказаться от чтения доказательств, вам все равно нужно прочитать доказанное утверждение. Если это нецелесообразно из-за чрезмерной многословности, то это решение не является удовлетворительным.

Из-за этих проблем я не хотел останавливаться на Cedille-Core как на ответе на мои поиски. В какой-то момент это стало похоже на проблему без решения. Типы данных по своей природе сложны. Индуктивные - тем более. Либо эта сложность должна быть связана с реализацией языка, либо с кодом, написанным на нем. Верно? Но все же у Cedille-Core другая проблема: она не просто сложная, а напрасно! Чтобы реализовать на нем тип данных, вам нужно объявить два эквивалентных, но немного разных его представления, а затем пересечь их как третий тип, который является «официальным». Этот подход также делает доказательство обходным путем, поскольку вам нужно, во-первых, доказать отражение. После долгих экспериментов я понял, что это слишком ошеломляюще. Но почему они присутствуют? Почему нельзя упростить?

Примечание: я также заметил другую проблему с Cedille-Core, которая может сделать его несовместимым с абстрактным алгоритмом, о котором я упоминал ранее. Я не буду здесь вдаваться в подробности, но есть дополнительная информация об этом коммите.

Упрощение Cedille

На самом деле Cedille можно чрезвычайно упростить с помощью одного изменения: замены зависимых пересечений и примитивов равенства собственными типами и взаимной рекурсией. Оба подхода на самом деле очень похожи, но последний позволяет достичь двух очень важных результатов:

  1. Из-за взаимной рекурсии объявление типа типа данных может ссылаться на его конструкторы до того, как они были определены. Таким образом, нам больше не нужны два разных объявления одного и того же типа плюс третье для их объединения. Мы можем объявить тип данных за один раз.
  2. Поскольку сейчас задействован только один тип, нам не нужно доказывать отражение, чтобы доказать индукцию. Это позволяет нам избавиться от всех примитивов равенства языка, которые составляют примерно половину его сложности.

Таким образом, это небольшое изменение, в свою очередь, делает базовый язык примерно на 40% меньше, а реализацию индуктивных типов данных внутри него примерно на 60% меньше. Вот чем становится доказательство индукции (проверка типов включена в Gist):

Это не только намного меньше; с 67 до 26 строк; но, что самое главное, больше нет избыточности. Объявление индуктивного типа данных, такого как Nat, включает в себя именно ту информацию, которая необходима для определения его принципа индукции. Конечно, это не так лаконично, как, например, Агда; но на этот раз дополнительная информация присутствует, потому что это действительно необходимо. Agda просто скрывает это при реализации. Например, Eq читается почти как аксиома J, и вывести ее несложно:

Этот язык также решает многие проблемы, с которыми сталкивается Cedille, например, невозможность доказать 1 != 0 без дополнительной аксиомы или возможная несовместимость с абстрактным алгоритмом. Излишне говорить, что мне это очень нравится. К сожалению, хорошие вещи не даются бесплатно. Исследователь, который сам ввел самотипы, утверждал, что они слишком сложны для обеспечения семантики, поэтому он отошел от них и построил Cedille вокруг зависимых пересечений. Другими словами, велика вероятность того, что такой язык будет противоречивым.

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

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