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

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

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

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

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

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

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