Изоморфизм Карри-Говарда

Изоморфизм Карри-Говарда является отношением между компьютерными программами и математическими доказательствами. Это понятие известно также под названиями «Соотношение Карри-Говарда» и «Соотношение формул и типов». Для его выражения используется несколько различных формулировок. Открыт независимо американским математиком Х. Б. Карри и логиком В. Э. Говардом.

Соотношение может быть распознано на двух уровнях. Во-первых, по аналогии того, что тип функции аналогичен логическим теоремам, при этом тип результата функции (т. е. тип значения, которое возвращается функцией) соответствует заключению теоремы, а типы аргументов функции соответствуют гипотезам теоремы. Поэтому программа, вычисляющая такую функцию, аналогична процессу доказательства теоремы. В теории информатики это является важнейшим базовым принципом, соединяющим смежные области λ-исчисления и теории типов. Обычно этот уровень соотношения формулируется в виде «Доказательства есть программы». Другой формулировкой является «высказывания есть типы».

Второй и более формальный уровень соотношения заключается в том, что оно специфицирует формальный изоморфизм между двумя областями математики: между формализованной особым образов дедукцией и типизированным λ-исчислением. Между этими областями имеется биекция: в первой используются доказательства и термы, во второй — теорема об уничтожении разрезов и β-редукция.

Существует несколько способов осмыслить изоморфизм Карри-Говарда. С одной стороны он действует на уровне преобразования доказательств в программы. Здесь доказательство в оригинале было ограничено понятием доказательства в конструктивной логике — типичной в системе интуиционистской логики. А программы рассматриваются в смысле функционального программирования, при этом с точки зрения синтаксиса такие программы выражаются при помощи некоторой формы λ-исчисления. Поэтому одна из конкретных реализаций изоморфизма Карри-Говарда заключается в детальном изучении того, как доказательства из интуиционистской логики могут быть записаны в виде λ-термов (это вклад Говарда, Карри остановился на комбинаторах, которые более приспособлены для записи программ на машинных языках, для которых λ-исчисление является языком более высокого уровня). Ранее расширение изоморфизма Карри-Говарда было сформулировано таким образом, чтобы охватить и классическую логику, внося соответствия для классических правил вроде закона отрицания отрицания и закона Пирса типам, в терминах которых производится работа с континуациями.

Существует направление преобразования (т. е. преобразование доказательства в программу или использование программы для генерации доказательства), которое соответствует возможности создания доказательства при наличии корректности программы. Это осуществимо только в совершенно богатом окружении теории типов. Фактически разработка очень богатых типизированных языков программирования теоретиками была мотивирована желанием проявить изоморфизм Карри-Говарда более наглядно.

Типы

Используя нотацию λ-исчисления, функция с параметром x и телом E записывается как λx.E. Когда к этой функции прикладывается аргумент a (термин «прикладывается» также взят из λ-исчисления), в теле функции E на a заменяется каждое свободное вхождение x. Правильные λ-термы выглядят следующим образом:

1. v (где v — переменная)
2. λv.E (где v — переменная и E — λ-выражение)
3. (EF) (где E и F — λ-выражения)

Вторая форма определяет абстракцию функции. Эта абстракция создаёт функцию с аргументом v и телом E, в котором аргумент v может участвовать ноль или более раз.

Третья форма называется аппликацией (или применением). Она определяет попытку приложить терм E (как будто бы это аргумент функции) к терму F (как будто бы это функция).

Также для удобства обычно используются сокращения, при использовании которых аппликация ((AB)C) сокращается до (ABC), а абстракция λa.λb.E сокращается до λab.E. Говорят, что λ-выражение замкнуто, если оно не содержит свободных переменных.

Типы зависят от переменных типа, которые обозначаются стрчными буквами греческого алфавита: α, β и т. д. Для уменьшения записей все переменные типа предполагаются квантифицированными квантором всеобщности, то есть если в выражении типа имеется переменная типа, она должна быть согласующейся с любым типом, который может быть подставлен вместо неё. Тип произвольного выражения определяется следующим образом. Если переменная v имеет тип α, а выражение E имеет тип β, то абстракция λx.E имеет тип, обозначаемый как α → β; это тип функции, принимающей аргумент типа α и возвращающая результат типа β. В выражении (EF) если F имеет тип α, то функция E должна иметь тип α → β, а результат применения функции имеет тип β (и, соответственно, само выражение имеет этот тип).

Например, пусть имеется функция K = λab.a. Пусть также переменная a имеет тип α и переменная b имеет тип β. В этом случае λ-терм λb.a имеет тип β → α, а сама функция K имеет тип α → (β → α). Принимая во внимание то, что стрелка (→) ассоциативна вправо, этот тип можно записать как α → β → α. А это, в свою очередь, значит, что функция K принимает на вход один аргумент типа α и возвращает функцию типа β → α, которая получает на вход аргумент типа β, и возвращает результат типа α.

Абсолютно также пусть имеется функция B = λabc.(a(bc)). Пусть переменная c имеет тип γ. В этом случае переменная b должна иметь тип навроде γ → β, а λ-выражение (bc) имеет тип β. Абсолютно также переменная a должна иметь тип навроде β → α, а λ-выражение (a(bc)) имеет тип α. Это всё подводит к мысли о том, что λ-выражение λc.(a(bc)) имеет тип γ → α; λ-выражение λbc.(a(bc)) имеет тип (γ → β) → γ → α; а λ-выражение λabc.(a(bc)) имеет тип (β → α) → (γ → β) → γ → α. Этот результат можно интерпретировать так, что функция B принимает на вход аргумент типа (β → α) и аргумент типа (γ → β), а в качестве результата возвращает функцию, которая, принимая на вход аргумент типа γ, возвращает результат типа α.

Проблема полноты системы типов

Вполне понятно, что λ-выражение может иметь совершенно сложный тип. Можно спросить, существует ли λ-выражение с заданным типом. Проблема поиска такого λ-выражения называется проблемой наполненности типов.

Ответ весьма примечателен: существует закрытое λ-выражение с заданным типом тогда и только тогда, когда тип соответствует теореме в логике, если символы (→) интерпретировать в качестве операции логической импликации.

Например, если представить функцию тождества λx.x, которая получает на вход аргумент типа α и возвращает его же с типом α, а потому её тип: α → α. Это выражение определённо является теоремой в логике: из заданной формулу α может следовать только α.

Тип функции K :: α → β → α, и это тоже теорема. Если α истинно, то можно заключить, что если β истинно, из этого можно заключить истинность α. Это выражение иногда упоминают под наименованим «правило реитерации». Тип функции B :: (β → α) → (γ → β) → γ → α. Это выражение можно рассматривать как тавтологию: если (β → α) истинно, то если (γ → β) истинно, то можно заключить, что из γ следует α.

С другой стороны можно рассмотреть выражение α → β, которое не является теоремой. Ясно, что не существует λ-терма с таким типом. Если бы он существовал, это была бы функция, которая принимает на вход один аргумент типа α и возвращает результат типа β — типа, совершенно не связанного с типов входного аргумента, ничем не ограниченного. Это невозможно, поскольку нельзя получить что-то из ничего.

Однако существует функция с типом β → (α → α) (например, функция λb.λa.a, которая получает на вход аргумент b, игнорирует его и возвращает функцию тождества в качестве результата), но не существует функции с типом (α → α) → β, которая, если бы существовала, преобразовывала бы некоторую функцию в значение произвольного типа (что невозможно).

Интуиционистская логика

Хотя верно то, что все типы существующих объектов соответствуют теоремам логики, обратное утверждение не верно. Даже если ограничить внимание логическими формулами, которые содержат только импликацию (→), — то есть ограничить внимание только так называемой импликативной частью логики, не каждая правильная логическая формула соответствует некоторому типу объектов. Например, тип ((α → β) → α) → α не содержит ни одного объекта, в то время как соответствующая логическая формула, известная как закон Пирса, является тавтологией.

Интуиционистская логика является более слабой системой, чем классическая логика. Тогда как классическая логика содержит формулы, которые абстрактно истинны (в смысле мира идей Платона), формула в интуиционистской логике полагается истинной только тогда, когда из неё можно создать доказательство. Формула α ∨ ¬α служит поясняющим это положение примером — она является теоремой в классической логике, но не является таковой в логике интуиционистской. Хотя она истинна в классической логике, в интуиционистской логике эта формула утверждает, что можно доказать либо утверждение α, либо можно доказать утверждение ¬α. Поскольку не всегда можно доказать либо то, либо другое утверждение (см. также теорему Гёделя о неполноте), эта формула не является теоремой в интуиционистской логике.

Взаимное соответствие между типами, в которых имеются объекты, и правильными логическими формулами (при ограничении рассмотрения теорем только с операцией импликацией) существует в интуиционистской логике. Это соответствие называется алгеброй Гильберта.

Простая система аксиом в стиле Гильберта

Следуя некоторым основным идеям дедукционной системы в стиле Гильберта, можно формально охарактеризовать импликационный фрагмент интуиционистской логики примерно следующим образом. Все формулы вида

α → β → α

являются аксиомами, равно как и все формулы вида

(α → β → γ) → (α → β) → α → γ

Единственным правилом вывода является правило Modus Ponens, которое говорит о том, что если доказаны две теоремы α → β и α, предполагается доказанным, что β — тоже доказанная теорема. Множество формул, которые могут быть выведены при помощи этого правила, в точности является множеством формул с импликациями из интуиционистской логики. В частности, закон Пирса не выводится при помощи этого правила из двух упомянутых аксиом.

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

Функции являются доказательствами

Второй аспект изоморфизма Карри-Говарда заключается в том, что функции, чей тип соответствует логической формуле, сами по сеье являются аналогом доказательства такой формулы.

Например, пусть имеются две функции λ-исчисления: $$K \equiv \lambda xy.x$$ $$S \equiv \lambda xyz.xz(yz)$$

Можно показать, что любая функция может быть создана при помощи определённой комбинации этих двух функций (см. Базис S, K, а также статью «Комбинаторная логика», в которой приведено доказательство). Например, функция B может быть определена как (S(KS)K). Если функция, такая как B, может быть определена как композиция функция K и S, то такое выражение может быть напрямую сконвертировано в доказательство теоремы интуиционистской логики, соответствующей типу функции B. Важно отметить то, что проявления функции K соответствуют использованию первой аксиомы, а проявления функции S соответствуют применению второй аксиомы, а применение функций соответствует использованию правила вывода Modus Ponens.

Первая аксиома выглядит как α → β → α, и это в точности тип функции K, В точности также вторая аксиома выглядит как (α → β → γ) → (α → β) → α → γ, и это — тип функции S. Правило Modus Ponens говорит о том, что если имеются два выражения, первое типа α → β (то есть это — тип функции, которая принимает значение типа α и возвращает результат типа β), а второе типа α, то применение первого выражения ко второму даст значение типа β. Другими словами, фактическая передача параметра типа α в функцию типа α → β даст значение типа β.

Доказательство теоремы α → α

В качестве простого примера можно рассмотреть доказательство теоремы α → α. Это — тип комбинатора тождества $I \equiv \lambda x.x$. Функция ((SK)K) также эквивалентна тождеству. Для начала доказательства необходимо применить S к K. Это происходит следующим образом:

α → β → α

(α → β → γ) → (α → β) → α → γ

Если предположить, что γ = α в выражении типа S (см. «Унификация типов»), то получится:

(α → β → α) → (α → β) → α → α

Поскольку антецедент этой формулы — (α → β → α) — первая аксиома, применяя Modus Ponens, можно вывести консеквент:

(α → β) → α → α

Это выражение является типом применения (SK). Теперь эту функцию необходимо применить к K. Опять же необходимо манипулировать формулами таким образом, чтобы антецедент был похож на аксиому K, в рассматриваемом случае унификация типов даст соответствие (β → α) к β:

(α → β → α) → α → α

Опять же, используя правило вывода, получается консеквент:

α → α

Что и требовалось доказать.

В общем виде процедура доказательства выглядит просто. Если где-либо в программе имеется применение (PQ), то для начала необходимо доказать теоремы, соответствующие типам термов P и Q. Далее, поскольку терм P применяется к Q, тип этого терма должен иметь форму α → β, а тип терма Q должен иметь форму α (для некоторых α и β, принимая во внимание унификацию типов). При помощи правила вывода Modus Ponens можно заключить истинным следствие β.

Доказательство теоремы (β → α) → (γ → β) → γ → α

В качетсве более сложного примера можно рассмотреть теорему, которая соответствует функции B. Тип этой функции — (β → α) → (γ → β) → γ → α, а её выражение через комбинаторы K и S выглядит так: (S(KS)K). Ниже приводится последовательность шагов при доказательстве теоремы (β → α) → (γ → β) → γ → α.

Прежде всего необходимо сконструировать применение (KS). Для этого необходимо сопоставить антецедент функции K и тип функции S, а это делается приравниванием α к (α → β → γ) → (α → β) → α → γ и β к δ:

α → β → α

((α → β → γ) → (α → β) → α → γ) → δ → (α → β → γ) → (α → β) → α → γ

Поскольку антецедентом здесь является тип функции S, можно выделить консеквент:

δ → (α → β → γ) → (α → β) → α → γ

Это — теорема, которая соответствует типу применения (KS). Теперь необходимо применить функцию S к этому выражению. Принимая во внимание аксиому для этой функции

(α → β → γ) → (α → β) → α → γ

необходимо сопоставить α = δ, β = (α → β → γ) и γ = ((α → β) → α → γ), что даёт

(δ → (α → β → γ) → (α → β) → α → γ) → (δ → (α → β → γ)) → δ → (α → β) → α → γ

откуда следует истинность консеквента:

(δ → α → β → γ) → δ → (α → β) → α → γ

Эта формула является типом выражения (S(KS)). Особым видом этой теоремы является случай, когда δ = (β → γ):

((β → γ) → α → β → γ) → (β → γ) → (α → β) → α → γ

Теперь эта последняя формула должна быть применена к функции K. Опять же, производится унификация типов в аксиоме для K, на этот раз при помощи замены α на (β → γ) и β на α:

α → β → α

(β → γ) → α → (β → γ)

Это выражение тождественно антецеденту предшествующей формулы, так что можно выделить консеквент:

(β → γ) → (α → β) → α → γ

Меняя наименования переменных α и γ местами, можно получить:

(β → α) → (γ → β) → γ → α

Это выражение является искомой теоремой. Что и требовалось доказать.

Исчисление следствий

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

Правила вывода исчисления следствий для импликационного фрагмента интуиционистской логики выглядят следующим образом:

1. ${{} \over \Gamma, \alpha \vdash\alpha } \qquad {\rm (Axiom)}$
2. ${\Gamma, \alpha\vdash\beta \over \Gamma\vdash\alpha\rightarrow\beta}\qquad ({\rm Right}\rightarrow)$
3. ${\Gamma\vdash\alpha\qquad\qquad\Sigma, \beta\vdash\gamma \over \Gamma, \Sigma, \alpha\rightarrow\beta \vdash \gamma}\qquad({\rm Left}\rightarrow)$

Символ $\Gamma$ представляет контекст, который является набором гипотез. Запись «$\Gamma\vdash a$» показывает, что можно доказать $a$ при помощи предположения истинности контекста $\Gamma$. Логические теоремы в точности состоят из тех формул $t$, для доказательства которых не требуются гипотезы. Другими словами терм $t$ является теоремой тогда и только тогда, когда можно показать «$\vdash t$».

Доказательством в исчислении следствий является дерево, в корне которого находится теорема, которую необходимо доказать; в листовых вершинах же находятся аксиомы. Каждый промежуточный узел дерева должен быть помечен либо «Right →» or «Left →» и должен содержать формулу, выведенную из дочерних элементов в соответствии с указанным правилом вывода. Например, доказательство теоремы (β → α) → (γ → β) → γ → α в исчислении следствий выглядит следующим образом: $$\cfrac { \gamma \vdash \gamma \qquad \cfrac { \beta \vdash \beta \qquad \alpha \vdash \alpha} {\beta,\beta \rightarrow \alpha \vdash \alpha} Left \rightarrow }{\qquad \cfrac {\gamma, \beta \rightarrow \alpha, \gamma \rightarrow \beta \vdash \alpha } { \qquad \cfrac {\beta \rightarrow \alpha, \gamma \rightarrow \beta \vdash \gamma \rightarrow \alpha } { \qquad \cfrac { \beta \rightarrow \alpha \vdash (\gamma \rightarrow \beta) \rightarrow \gamma \rightarrow \alpha } { \vdash (\beta \rightarrow \alpha) \rightarrow (\gamma \rightarrow \beta) \rightarrow \gamma \rightarrow \alpha } Right \rightarrow } Right \rightarrow } Right \rightarrow } Left \rightarrow$$

Доказательства в исчислении следствий близко соответствуют λ-выражениям. Запись «$\Gamma\vdash a$» может быть проинтерпретирована таким образом, что для заданных значений с типами, перечисленными в $\Gamma$, можно создать значение с типом $a$. Аксиома соответствует вводу новой переменной с новым неограниченным типом. Правило «Right →» соответствует абстракции функции: $${ \Gamma, \alpha\vdash\beta \over \Gamma\vdash\alpha\rightarrow\beta}\qquad ({\rm Right}\rightarrow)$$

Когда можно заключить, что некоторая программа $\Gamma$ содержит функцию с типом α → β? Тогда, когда $\Gamma$ и значение типа α содержат достаточно для того, чтобы создать значенеи типа β.

Правило вывода «Left →» соответствует аппликации функций: $${ \Gamma \vdash \alpha \qquad \Sigma, \beta \vdash \gamma \over \Gamma, \Sigma, \alpha\rightarrow\beta \vdash\gamma} \qquad ({\rm Left} \rightarrow)$$

Если имеется значение типа α и при наличии значения типа β можно сконструировать значение типа γ, то функция типа α → β также позволит сконструировать значение типа γ. Это делается следующим образом: сначала необходимо сконструировать значение типа α, затем применить к нему функцию и получить результат типа β, после чего сконструировать значение типа γ.

Доказательство теоремы (β → α) → (γ → β) → γ → α, приведённое выше, показывает способ создания λ-выражения этого типа. Для начала пусть имеются переменные a и b с типами α и β соответственно. Правило «Left →» предписывает сконструировать функцию (λb.ab), которая вызвращает значение типа α. Далее опять используется правило вывода «Left →», на основании которого создаётся функция (λb.a(λg.bg)), которая всё также возвращает значение типа α.

Точка зрения теории категорий

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

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

Далее предполагается, что доказательства рассматриваются как некоторые функции высшего порядка, а указанный функтор действует как компилятор. Если задать вопрос «доказательство чего?», ответом будет «некоторого выражения». Поскольку доказательства проецируются на программы, их типы становятся соответствующими выражениям. Говоря, что имеется функтор, утверждается, что правило вывода Modus Ponens в некоторой своей форме становится композицией функциональных программ, то есть явный применений.

Приведённое рассуждение является полезной схемой, которая применима в широком диапазоне ситауций. Это значит, что не имеет смысла искать некоторых канонических формулировок. Традиционным взглядом на изоморфизм является ожидание квантифицированного существования выражений, которые ведут (в интуиционистской логике) к конструктивным решениям проблем. Этот взгляд восходит к Колмогорову и полностью соответствует точке зрения теории категорий. С акцентом на то, что на уровне морфизмов пропозиция «из A следует B» интерпретируется как функциональный тип: если A утверждает, что существует нечто, удовлетворяющее P; и B утверждает, что существует нечто, удовлетворяющее Q, тогда имеется интерес в методах, которые позволяют сконструировать нечто типа Q из нечто типа P (интерпретация Колмогорова). Это полностью соответствует точке зрения на функциональные программы, которые являются базовыми интерпретациями декартово-замкнутых категорий как моделей типизированного λ-исчисления.

Это позволяет использовать изоморфизм Карри-Говарда для интеграции в категориальную логику в качестве практического инструмента для фундаментального объяснения моделирования. Теории типов становятся категориями, категории поддерживают интерпретации на уровне λ-исчисления. Эта точка зрения иногда называется «соответствием Карри-Говарда-Ламбека» в честь Иоахима Ламбека, который впервые рассмотрел категориальную логику под этим углом. Коды программ скрываются при помощи компилирования λ-исчислений в нечто более низкого уровня (например, в термы комбинаторной логики Х. Карри).

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

См. также

• Интуиционистская теория типов
• Haskell

Ссылки

• Thompson, Simon (1991). Type Theory and Functional Programming Addison-Wesley. ISBN 0-201-41667-0.