Соответствие Карри

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

Хаскелл Карри^[1] и Уильям Ховард (англ.)^[2] заметили, что построение конструктивного доказательства похоже на описание вычислений, а высказывания конструктивной логики по своей структуре схожи с типами вычисляемых выражений — программ для вычислительной машины.

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

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

Логические системы	Языки программирования
Высказывание	Тип
Доказательство высказывания $P$	Терм (выражение) типа $P$
Утверждение $P$ доказуемо	Тип $P$ обитаем
Импликация $P \Rightarrow Q$	Функциональный тип $P \rightarrow Q$
Конъюнкция $P \and Q$	Тип произведения (пары) $P \times Q$
Дизъюнкция $P \or Q$	Тип суммы (размеченного объединения) $P + Q$
Истинная формула	Единичный тип
Ложная формула	Пустой тип ($\bot$)
Квантор всеобщности $\forall$	Тип зависимого произведения ($\Pi$-тип)
Квантор существования $\exists$	Тип зависимой суммы ($\Sigma$-тип)

Простейшим примером соответствия Карри — Ховарда может служить изоморфизм между простым типизированным λ-исчислением и фрагментом интуиционистской логики высказываний, включающим только импликацию. Например, тип $(P \rightarrow Q \rightarrow R) \rightarrow (P \rightarrow Q) \rightarrow P \rightarrow R$ в простом типизированном лямбда-исчислении соответствует высказыванию $(P \Rightarrow (Q \Rightarrow R)) \Rightarrow ((P \Rightarrow Q) \Rightarrow (P \Rightarrow R))$ логики высказываний. Для доказательства этого высказывания необходимо сконструировать терм указанного типа (если это удаётся сделать, то про тип говорят, что он обитаем или населён), в данном случае можно предъявить нужный терм: $\lambda f g x \rightarrow f x (g x)$, и это значит, что тавтология $(P \Rightarrow (Q \Rightarrow R)) \Rightarrow ((P \Rightarrow Q) \Rightarrow (P \Rightarrow R))$ доказана.

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

Примечания

1. ↑ Curry, H. B., Feys, R. Combinatory Logic Vol. I. — Amsterdam: North-Holland, 1958.
2. ↑ Howard, W. A. The formulae-as-types notion of construction // To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. — Boston: Academic Press, 1980. — С. 479–490.

Литература

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