Эти записи посвящены старой аналогии между доказыванием теорем и программированием: доказательство похоже на программу, программа похожа на доказательство. Возможно, причиной того, что эта аналогия, известная как доказательства-как-программы, утверждения-как-типы или соответствие Карри–Ховарда, всё еще кажется новой, хотя ей уже несколько десятилетий, кроется в том, что она вдохновляет и математиков и программистов. Программист может сказать себе: "Я не только трачу время, программируя целый день – я доказываю теоремы". Математик в свою очередь может сказать себе: "Я не только трачу время, доказывая теоремы целый день – я программирую".
«Logical basis of evaluation order and pattern matching», Ноам Зайлбергер
Утверждение о доказательствах как программах носит название соответствие Карри–Ховарда. Впрочем, это уже не одно утверждение, а парадигма, взгляд на логические теории как языки программирования и на языки программирования как на логические теории. Этот взгляд можно сформулировать так:
Утверждение в формальной логической системе можно сопоставить с типом в языке программирования, а доказательство утверждения со значением такого типа.
Меньше всего трудностей у такой интерпретации вычисления возникает, когда мы говорим о языках, специально созданных для интерактивных систем доказательств, (таких как Agda) или функциональных языках, разрабатываемых академическим сообществом, (таких как Haskell) при приближении же к промышленным языкам программирования соответствие становится всё более и более призрачным. Так что, это соответствие не означает, что, создавая класс на вашем любимом языке программирования, вы что-то утверждаете.
Строгое соответствие есть между формальными логическими теориями и системами типов для лямбда исчисления. Здесь имеет смысл остановиться на том, что понимается под типом в математике. Идея типа возникла в математике где-то в конце XIX века. Первая система типов была описана Расселом и Уайтхедом для их логической теории, в попытке избежать замкнутого круга в определениях¹. Такая система типов была довольно сложной, о чём говорило само название разветвлённая теория типов. Она не получила серьёзного развития. Но сама идея, что с математическим объектом можно связать некий атрибут, и комбинировать объекты только так, как это позволяют их атрибуты, оказалась плодотворной. Её использовал Чёрч, когда понял, что разработанный им язык для формального описания математических функций ‒ лямбда исчисление, описывает и те функции, которые не возвращают значение, входя в бесконечную рекурсию. Для исправления ситуации Чёрч придумал простую теорию типов, в которой функциям, произвольно использующим рекурсию, нельзя было приписать тип. То есть, в математике система типов задаёт ограничения, которые гарантируют корректность формальной теории. В программировании это не совсем так.
Но вернёмся к соответствию Карри–Ховарда. У него достаточно интересная судьба. Хаскелл Карри занимался комбинаторным исчислением, языком описания функций без переменных. В нём функции задаются с помощью нескольких базовых, называемых комбинаторами. Как и для лямбда исчисления в комбинаторном исчислении, для того чтоб показать, что функции всегда возвращают результат, используется система типов. Карри обратил внимание, что типы базовых комбинаторов S и K напоминают аксиомы формальной логики²:
K: A ⇒ (B ⇒ A)
S: (A ⇒ (B ⇒ C)) ⇒ ((A ⇒ B) ⇒ (A ⇒ C))
Комбинаторное исчисление было реализовано в виде языка программирования Unlambda. Желающие могут пробовать на нём что-нибудь написать.
Вильям Ховард впервые чётко описал соответствие, но большой своей заслуги в этом не видел. Он не стал публиковать свою статью formulae-as-types notion of construction ‒ его записи распространялись частным образом, только через одиннадцать лет после написания, в 1980 году, статья увидела свет. В чём-то он прав, достаточно окинуть свежим взглядом интерпретацию BHK, чтоб увидеть за ней язык программирования³:
высказыванию A ⋀ B соответствует тип-произведение или пара - любая структура, содержащая два поля с типами A и B. Каноническим представлением будет:
в Haskell —(A, B)
в С# — Tuple<A, B>
в С++ — pair<A, B>
в Haskell — Either A B
в С# — нет стандартного, в сторонних библиотеках встречается Either<A, B>
в С++ — нет стандартного, в сторонних библиотеках встречается variant<A, B>
в Haskell — A -> B
в С# — Func<A, B>
в С++ — function<B(A)>
Осталось рассмотреть вопрос, что есть вычисление с точки зрения логики. В чисто функциональном языке вычисление ‒ это вызов функции. Вызову функции в логике соответствует modus ponens:
A A ⇒ B
B
Это становится очевидно, если мы укажем свидетельства рядом с высказываниями:
a : A f : A ⇒ B
f(a) : B
Как же формируется f(a) c логической точки зрения? Свидетельство в каком-то смысле является доказательством, по крайней мере, из него должно быть возможно доказательство восстановить. Но из восстановленного доказательства уже не видно, что оно получено из f и a. Такое доказательство не будет включать в себя каких-либо промежуточных лемм, а будет представлять собой вывод напрямую из аксиом. То есть, с точки зрения логики вычисление есть процесс упрощения структуры доказательства для конкретных условий путём подстановки доказательств лемм и выбрасывания случаев, неприменимых к заданным условиям. Аналогичная трактовка вычисления свойственна и функциональным языкам программирования.
В computer science существует взгляд на программирование, формальные логические системы и теоркатегорные структуры, которые им соответствуют (об этом когда-нибудь потом), как разные стороны одного и того же явления ‒ так называемый вычислительный тринитаризм, вера в вычислительную Троицу. Не знаю насколько он оправдан, но всё же примечательно, что процесс вычисления и процесс мышления можно структуировать с помощью одних и тех же формальных систем.
Впрочем, задачи у языков программирования и логических систем разные, корректность во всех случаях для программирования редко бывает важна. Потому, несмотря на наличие сходства, программирование к математике не сводится. Даже общая рекурсия, столь пугавшая Чёрча и Карри, ради избавления от которой, типы, собственно, и вводились, является важным инструментом в программировании. Её аналогом в более привычных для всех императивных языках программирования является цикл. Попробуйте что-нибудь серьёзное написать, не используя цикл⁴. И если цикл, который не завершается, в программировании имеет смысл, то доказательство, которое зацикливается и не может достичь аксиом смысла не несёт. Правда, логику можно расширить разными модальностями, с помощью которых возможно трактовать и такие вычисления. Но о модальной логике будет дальше.
Возможно ли распространить соответствие Карри‒Ховарда на классическую логику, можно ли приписать классической логике конструктивный смысл? Ответ ‒ в некотором смысле да. Об этом в следующий раз.
¹ То есть, явное или неявное использование определяемого объекта в самом определении.
² Этих двух комбинаторов достаточно, для того чтоб описать все функции, которое можно задать алгоритмически. Две аксиомы же описывают импликационный фрагмент (т.е. фрагмент, основанный на операции следования) интуиционистской логики высказываний. Надо сказать, что "и" и "или" можно определять через "следует", так что к импликационному фрагменту можно свести всю остальную часть.
³ В момент, когда появилась интерпретация BHK (в начале 1930-х), ещё уточнялось само понятие алгоритма, и концепции типизированного функционального языка программирования просто не было. В том, что она появилась, большая заслуга Чёрча и Карри. Собственно, лямбда-исчисление и оказалось первым функциональным языком программирования.
² Этих двух комбинаторов достаточно, для того чтоб описать все функции, которое можно задать алгоритмически. Две аксиомы же описывают импликационный фрагмент (т.е. фрагмент, основанный на операции следования) интуиционистской логики высказываний. Надо сказать, что "и" и "или" можно определять через "следует", так что к импликационному фрагменту можно свести всю остальную часть.
³ В момент, когда появилась интерпретация BHK (в начале 1930-х), ещё уточнялось само понятие алгоритма, и концепции типизированного функционального языка программирования просто не было. В том, что она появилась, большая заслуга Чёрча и Карри. Собственно, лямбда-исчисление и оказалось первым функциональным языком программирования.
⁴ Это, на самом деле, интересная задача ‒ программирование с помощью урезанных форм рекурсии/специальных форм циклов (например, только проход по элементам коллекции), как правило, даёт более качественный код.
Комментариев нет:
Отправить комментарий