The Concept of Proof in the Context of a Type-Theoretic Approach, III: Proofs as (Some) Types.pdf Настоящая статья представляет собой третью часть исследования эпистемологических особенностей понятия доказательства в рамках теоретико-типового подхода. Первая статья [1] была посвящена эпистемологии доказательства корректности программного обеспечения, в ней рассматривались проблемы обозримости, вопрос о социальной роли таких доказательств, а также соотношение доказательства с пониманием абстракции в компьютерных науках. Вторая статья [2] касалась вопросов применения компьютерных средств в доказательстве теорем (в смысле математических результатов). В настоящей статье рассматриваются вопросы, связанные с понятием доказательства с точки зрения классического варианта доктрины «пропозиции как типы» (соответствие Кар-ри-Говарда) и современного варианта доктрины «пропозиции как некоторые типы» (вариант соответствия Карри-Говарда с точки зрения гомотопической теории типов). Данная тематика частично затрагивалась и в предыдущих статьях, тем не менее в настоящей работе более подробно освещается ряд важных аспектов и нюансов, рассматривается современное состояние исследований и предлагаются некоторые эпистемологические выводы. Соответствие Карри-Говарда [3] представляет собой нетривиальную связь логики и типизированных вычислений (в частности, типизированного лямбда-исчисления). В наиболее очевидном виде эта связь проявляется между интуиционистской пропозициональной логикой и просто типизированным лямбда-исчислением и позволяет утверждать, что у всякого доказательства соответствующей логической системы имеется некоторое вычислительное содержание, а всякое вычисление, производимое в соответствующем варианте типизированного лямбда-исчисления, имеет некоторое математическое содержание. Необходимо отметить, что благодаря указанному обстоятельству рассматриваемая доктрина является одним из центральных постулатов теории языков программирования, поскольку позволяет удобно и эффективно использовать математические методы при разработке, построении и исследовании различных языков и методов программирования. Хотя различные варианты типизированного лямбда-исчисления соответствуют различным логикам (например, классическая логика описывает вычисления в стиле передачи продолжений, а линейная логика соответствует лямбда-исчислению, моделирующему потребление ресурсов), базовой логикой является интуиционистская логика, так как именно она соответствует наиболее простому варианту типизированного лямбда-исчисления, на основе которого строятся все остальные варианты. Таким образом, в дальнейшем для простоты в качестве логики будет использоваться именно она, а также соответствующая ей семантика. В отличие от классической логики, в которой рассуждения представляются своего рода «с божественной точки зрения» и предполагается, что всякое высказывание является либо истинным, либо ложным вне зависимости от каких-либо связанных с человеческим знанием факторов, интуиционистская логика представляет собой логику «с человеческой точки зрения». Наиболее очевидным это становится при рассмотрении BHK-интерпретации интуиционистской логики, названной так в честь Л.Э.Я. Брауэра, А. Гейтинга и А.Н. Колмогорова. Семантика для интуиционистской логики в соответствии с BHK-интерпретацией [4. P. 161] традиционно дается в терминах доказательств (например, доказательство для конъюнкции дается путем представления доказательств для конъюнков, а доказательство для импликации является построением, позволяющим трансформировать доказательство для антецедента в доказательство для консеквента и т.д.). Хотя вариант, предложенный А.Н. Колмогоровым, формулировался в терминах задач и решений (соответственно, импликация является задачей по сведению решения для консеквента к решению для антецедента; другими словами, требуется решить задачу кон-секвента, имея решение для задачи антецедента), в дальнейшем А. Гейтингом было показано, что для интуиционистского подхода эти варианты аналогичны. Соответственно, высказывание признается истинным, если для него имеется доказательство, и признается ложным, если для него имеется опровержение. В случае же, когда для некоторого высказывания нет ни доказательства, ни опровержения, такое высказывание является неразрешимым (что, конечно, может измениться в процессе накопления знания либо не измениться, если речь идет о принципиально неразрешимых высказываниях). Рассмотрение натурального исчисления для интуиционистской логики позволяет интерпретировать правила введения логических терминов как правила, определяющие «прямые» доказательства, а правила удаления - как «непрямые» доказательства. Причем из «непрямого» доказательства нельзя получить какую-либо дополнительную информацию сверх той, что была заложена в соответствующем «прямом» доказательстве. Такой анализ позволяет явно обсуждать формы доказательств, что в рамках теоретико-типового подхода отражается в синтаксической форме принадлежности (некоторого) терма (некоторому) типу. То есть запись t:T в таком случае означает не просто, что терм t имеет тип T, а что t является доказательством для T (терм t в таком случае может быть назван термом-доказательством или объектом-доказательством). В ряде случаев нам не важно, какую форму имеет доказательство той или иной теоремы, зачастую нам нужно иметь любое доказательство, чтобы иметь тем самым убежденность в рассматриваемом математическом результате, однако в некоторых случаях оказывается важным отличать разные доказательства одной и той же теоремы, что может быть легко выполнено и формально проанализировано при помощи рассматриваемого теоретико-типового подхода. Помимо прочего, BHK-интерпретация позволяет говорить о динамике доказательства, которая наиболее явным образом проявляется при использовании интерпретации интуиционистской логики как исчисления задач по А.Н. Колмогорову, причем динамика в данном случае понимается в соответствии с принципом Г. Генцена (ср.: [5. P. 246-247]), согласно которому правила удаления являются обратными по отношению к правилам введения. В этом смысле (1) доказательство, построенное с помощью правил введения, сохраняет информацию, которая в дальнейшем может быть «восстановлена» с помощью правил удаления, а также (2) доказательство является обратимым и может быть «восстановлено» обратно, используя информацию, полученную с помощью правил удаления. Таким образом, динамика доказательства, связанная с (обратимым) применением правил введения и удаления, оказывается аналогичной соответствующим (типизированным) вычислительным аспектам: например, правило введения конъюнкции соответствует построению пары, а два правила удаления конъюнкции - двум функциям, вычисляющим первую и вторую проекции данной пары; правило введения импликации соответствует лямбда-абстракции (т.е. построению функции), а правило удаления импликации - применению функции к аргументу. В этой связи очевидно, что и статика доказательства, касающаяся форм высказываний, тоже оказывается аналогичной соответствующим (типизированным) термам: конъюнкция соответствует паре, а конъюнкты - соответствующим частям данной пары; импликация соответствует функции, консеквент - аргументу функции, антецедент - значению. Благодаря рассмотренному выше соответствию теоретико-типовой подход является вариантом интерпретации логических понятий и, соответственно, новым взглядом на логику4. Причем следует обратить внимание на то, что этот подход позволяет обнаружить определенного рода «вертикальное единство» логического, которое проявляется в первую очередь с помощью зависимых типов. Дело в том, что выражение с квантором существования, утверждающее существование объекта, для которого выполняется некоторая подформула, в качестве значения предполагает пару, первым элементом которой является этот объект, а вторым - сертификат (или свидетельство), что этот объект выполняет данную подформулу (это функция, возвращающая для данного объекта доказательство того, что этот объект выполняет данную подформулу). Такая пара обычно называется зависимой суммой. В случае же, когда второй элемент пары является константной функцией, мы просто имеем дело с типом произведений, т.е. с обычным декартовым произведением, которое является интерпретацией конъюнкции. Поскольку с теоретико-типовой точки зрения тип произведений является частным случаем типа зависимых сумм, то конъюнкция при таком подходе может пониматься как частный случай выражения с квантором существования. Для выражений с квантором общности имеет место аналогичная ситуация: значением этого выражения является функция, превращающая любой объект в доказательство того, что этот объект выполняет данную подформулу. В случае, когда эта функция не зависит от объекта, мы имеем обычный тип функции. Таким образом, с теоретико-типовой точки зрения импликация является частным случаем выражения с квантором общности. Изложенное выше составляет основу доктрины «высказывания как типы». Получается, каждому высказыванию соответствует некоторый тип, термы которого представляют собой доказательства данного высказывания. Наибольший вклад в изучение рассмотренного соответствия внести Х. Карри [7, 8], У.А. Говард [9], а также Н.Г. де Брёйн [10], использовавший эту идею при построении системы Automath для проверки математических доказательств. Это соответствие может быть дополнено связью теории типов и некоторыми вариантами теории категорий, что может быть названо соответствием Карри-Говарда-Ламбека, или «вычислительным триединством» (термин принадлежит Р. Харперу). В этом отношении [11, 12] теория типов может пониматься как формальный синтаксис для теории категорий, а теория категорий - как семантическая интерпретация теории типов. Следует отметить, что эта связь не настолько очевидна, как в случае с интуиционистской логикой и типизированным лямбда-исчислением, однако она предоставляет возможность построения более выразительных формализмов. Обновленный взгляд на связь логики, типизированного лямбда-исчисления и теории категорий может быть обозначен как доктрина «высказывания как некоторые типы». Уже само это обозначение говорит о том, что при таком подходе не все высказывания соответствуют каким-то типам. Другими словами, высказывания рассматриваются как типы строго определенного вида, другие же типы уже высказываниями напрямую не считаются. Это не связано с какими-либо ограничениями на использование высокопорядковых логик, в теории типов вполне естественным образом можно представить любую формулу логики любого порядка. В случае с формулами логик высоких порядков это может быть достаточно легко сделано с помощью универсумов, которые в любом случае нужны для определения предикатов (как функций из объектов некоторого типа в универсум). Итак, доктрина «высказывания как некоторые типы» может быть проиллюстрирована обращением, например, к внутренней логике топосов или к гомотопической теории типов, в которых высказывания соответствуют типам с не более чем одним термом. Причем в гомотопической теории типов типы могут пониматься как гомотопические типы или как геометрические гомотопические типы. Доктрина «высказывания как типы» предполагает, что всякое высказывание соответствует некоторому типу, а доказательства этого высказывания соответствуют термам данного типа. Другими словами, построение терма некоторого типа является построением доказательства для соответствующего этому типу высказывания. При построении интуиционистской теории типов П. Мартин-Лёф [6. P. 5] выделил четыре формы суждений (которые не следует путать с высказываниями5): (1) A является множеством (= типом); (2) множество (= тип) A равно множеству (= типу) B; (3) a является элементом множества (= типа) A; (4) a и b являются равными элементами множества (= типа) A. Эти формы суждений получают несколько различных прочтений, которые в конечном счете представляют собой разные стороны одного и того же феномена. Например, для П. Мартин-Лёфа первая форма суждения может быть прочитана как утверждение, (1) что A является множеством (= типом); (2) что A является высказыванием; (3) что A является интенцией (ожиданием); (4) что A является проблемой (задачей). Поскольку для П. Мартин-Лёфа эти разные прочтения представляют собой, по сути, одно и то же, постольку особое выделение логического как специально области или формы знания оказывается для него нерелевантным. По-другому обстоят дела с пониманием логического в рамках доктрины «высказывания как некоторые типы». Гомотопическая теория типов не порывает с интуиционистским подходом, однако предлагает некоторое уточнение статуса логического и связанных с ним понятий. Термы, относящиеся к некоторому типу, все еще понимаются как разные доказательства (объекты-доказательства), от различий между которыми мы вполне можем абстрагироваться, применив процедуру -1-обрезания, с помощью которой происходит «усечение» типа любого уровня (начиная с 0) до уровня типов, соответствующих высказываниям. Это вполне согласуется с «чисто» логическим подходом, при котором важным является само наличие доказательства, а не его конкретная форма. Процедура -1-обрезания превращает любой тип в тип-высказывание, имеющий не более одного терма. Все многообразие типов (в смысле числа подпадающих под них термов) сводится к достаточно простой ситуации, когда если тип заселен, то он соответствует истинному высказыванию, а если же тип не заселен, то он соответствует ложному высказыванию. Если некоторый тип с помощью -1-обрезания может быть сведен к типу-высказыванию, имеющему один терм, то это означает, что данное высказывание истинно, и имеется свидетельство в пользу существования доказательства для этого высказывания. Другими словами, тип в доктрине «высказывания как некоторые типы» представляет собой множество доказательств для типа-высказывания, полученного с помощью процедуры -1-обрезания, а доказательства как термы указанного типа отождествляются друг с другом и сводятся к одному единственному терму, выполняющему роль положительного истинностного значения (т.е. истины). Соответственно, уровень «чисто» логического (ср.: [14]) (в его традиционном смысле) в гомотопической иерархии ограничивается -1 уровнем, а логика становится «частным случаем геометрии» [15. P. 329]. Такая ситуация со сведением разных доказательств к одному истинностному значению (их можно понимать как разные компоненты истинностного значения) возможна в гомотопической теории типов благодаря мощному понятию тождества (см.: [16]). Благодаря этому на уровне «чисто» логического мы имеем правила введения и удаления, а на более высоких уровнях, на которых типы понимаются как фундаментальные группоиды, мы имеем правила построения математических структур, лежащих за пределами «чистой» логики. Безусловно, логические структуры сохраняются на более высоких уровнях иерархии и играют нечто вроде формообразующей роли, однако они недостаточны для различения разных форм доказательств одного и того же высказывания и для проведения более тонких различий в рамках уже известных результатов. К примеру, традиционная «чисто» логическая интерпретация теорем К. Гёделя о неполноте не позволяет увидеть возможности построения формализмов, обладающих теми или иными выходящими за границы «чисто» логического подхода формами автореферентности, что демонстрирует как слабость «чисто» логического подхода, так и то, что мы до сих пор не имеем адекватного понимания феномена автореферентности6. При таком подходе «логические операции оказываются специальными случаями математических операций более общего вида» [18]. Теория типов, таким образом, представляет собой более мощный инструмент для анализа понятия доказательства, чем традиционная «чистая» логика, что позволяет строить системы для автоматических и интерактивных доказательств, во многом приближенные к обычным математическим доказательствам и математической интуиции .

Скачать электронную версию публикации