Соответствие Карри — Ховарда

Соответствие Карри — Ховарда (изоморфизм Карри — Ховарда, англ. formulæ-as-types interpretation) — наблюдаемая структурная эквивалентность между математическими доказательствами и программами, которая может быть формализована в виде изоморфизма между логическими системами и типизированными исчислениями.

Хаскелл Карри и Уильям Ховард (англ.) заметили, что построение конструктивного доказательства похоже на описание вычислений, а высказывания конструктивной логики по своей структуре схожи с типами вычисляемых выражений — программ для вычислительной машины. Ранние проявления этой связи — интерпретация Брауэра — Гейтинга — Колмогорова^[en] (1925), задающая семантику интуиционистской логики через вычисления доказательств, и теория реализуемости^[en] Клини (1945).

Соответствие Карри — Ховарда в современном представлении не ограничивается какой-то одной логикой или системой типов. Например, логика высказываний соответствует простому типизированному λ-исчислению, логика высказываний второго порядка (англ.) — полиморфному λ-исчислению, исчисление предикатов — λ-исчислению с зависимыми типами.

В рамках изоморфизма Карри — Ховарда следующие структурные элементы рассматриваются как эквивалентные:

Логические системы	Языки программирования
Высказывание	Тип
Доказательство высказывания $P$$P$	Терм (выражение) типа $P$$P$
Утверждение $P$$P$ доказуемо	Тип $P$$P$ обитаем
Импликация $P\Rightarrow <!--\; \Rightarrow \; -->Q$$P\Rightarrow Q$	Функциональный тип $P\to <!--\; \to \; -->Q$$P\rightarrow Q$
Конъюнкция $P\wedge <!--\; \wedge \; -->Q$$P\land Q$	Тип произведения (пары) $P\times <!--\; \times \; -->Q$$P\times Q$
Дизъюнкция $P\vee <!--\; \vee \; -->Q$$P\lor Q$	Тип суммы (размеченного объединения) $P+Q$$P+Q$
Истинная формула	Единичный тип
Ложная формула	Пустой тип ($\mathrm{\perp <!--\; \perp \; -->}$$\bot$)
Квантор всеобщности $\mathrm{\forall <!--\; \forall \; -->}$$\forall$	Тип зависимого произведения ($\mathrm{\Pi <!--\; \Pi \; -->}$$\Pi$-тип)
Квантор существования $\mathrm{\exists <!--\; \exists \; -->}$$\exists$	Тип зависимой суммы ($\mathrm{\Sigma <!--\; \Sigma \; -->}$$\Sigma$-тип)

Простейшим примером соответствия Карри — Ховарда может служить изоморфизм между простым типизированным λ-исчислением и фрагментом интуиционистской логики высказываний, включающим только импликацию. Например, тип $(P\to <!--\; \to \; -->Q\to <!--\; \to \; -->R)\to <!--\; \to \; -->(P\to <!--\; \to \; -->Q)\to <!--\; \to \; -->P\to <!--\; \to \; -->R$$(P\rightarrow Q\rightarrow R)\rightarrow (P\rightarrow Q)\rightarrow P\rightarrow R$ в простом типизированном лямбда-исчислении соответствует высказыванию $(P\Rightarrow <!--\; \Rightarrow \; -->(Q\Rightarrow <!--\; \Rightarrow \; -->R))\Rightarrow <!--\; \Rightarrow \; -->((P\Rightarrow <!--\; \Rightarrow \; -->Q)\Rightarrow <!--\; \Rightarrow \; -->(P\Rightarrow <!--\; \Rightarrow \; -->R))$$(P\Rightarrow (Q\Rightarrow R))\Rightarrow ((P\Rightarrow Q)\Rightarrow (P\Rightarrow R))$ логики высказываний. Для доказательства этого высказывания необходимо сконструировать терм указанного типа (если это удаётся сделать, то про тип говорят, что он обитаем или населён), в данном случае можно предъявить нужный терм: $\mathrm{\lambda <!--\; \lambda \; -->}fgx\to <!--\; \to \; -->fx(gx)$$\lambda fgx\rightarrow fx(gx)$, и это значит, что тавтология $(P\Rightarrow <!--\; \Rightarrow \; -->(Q\Rightarrow <!--\; \Rightarrow \; -->R))\Rightarrow <!--\; \Rightarrow \; -->((P\Rightarrow <!--\; \Rightarrow \; -->Q)\Rightarrow <!--\; \Rightarrow \; -->(P\Rightarrow <!--\; \Rightarrow \; -->R))$$(P\Rightarrow (Q\Rightarrow R))\Rightarrow ((P\Rightarrow Q)\Rightarrow (P\Rightarrow R))$ доказана.

Использование изоморфизма Карри — Ховарда позволило создать целый класс функциональных языков программирования, среда выполнения которых одновременно является системой автоматического доказательства, таких как Coq, Agda и Epigram (англ.).

ЛитератураПравить

• Pierce, Benjamin C. Types and Programming Languages. — MIT Press, 2002. — ISBN 0-262-16209-1.
  • Перевод на русский язык: Пирс Б. Типы в языках программирования. — Добросвет, 2012. — 680 с. — ISBN 978-5-7913-0082-9.