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

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

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

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

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

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

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

Примечания

Литература

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