Відповідність Каррі — Говарда

Відповідність Каррі — Говарда (ізоморфізм Каррі — Говарда, англ. Curry-Howard Isomorphism) — теорема, або точніше ряд теорем, що показують структурну еквівалентність між математичними доведеннями та програмами, або обчисленнями англ. computations. Ця еквівалентність може бути формалізована у вигляді ізоморфізму між логічними системами і типізованими лямбда-численнями.

Хаскелл Каррі[1] і Вільям Говард[2] помітили, що конструктивне доведення (тобто, доведення в інтуїціоністській логіці) схожа на програму, яка обчислює висновок, а саме висловлювання конструктивної логіки за своєю структурою схожі з типами виразів лямбда-числення — програм для обчислювальної машини.

Відповідність Каррі — Говарда не обмежується якоюсь однією логікою або системою типів. Наприклад, інтуїционістське числення висловлювань відповідає простому типізованому λ-численню, логіка висловлювань другого порядку — поліморфному λ-численню, числення предикатів — λ-численню з залежними типами.

У рамках ізоморфізму Каррі — Говарда наступні структурні елементи розглядаються як еквівалентні:

Логічні системи	Мови програмування
Висловлювання	Тип
Доказ висловлювання Ρ	Терм (вираз) типу Ρ
Затвердження Ρ можна довести	Тип Ρ населений
Імплікація Ρ ⇒ Q	Функціональний тип Ρ →Q
Кон'юнкція Ρ ∧ Q	Тип множення (пари) Ρ × Q
Диз'юнкція Ρ ∨ Q	Тип суми (розміченого об'єднання) Ρ + Q
Справжня формула	Одиничний тип
Хибна формула	Порожній тип (⊥)
Квантор загальності ∀	Тип залежного добутку (∏-тип)
Квантор існування ∃	Тип залежною суми (∑-тип)

Найпростішим прикладом відповідності Каррі — Говарда може служити ізоморфізм між простим типізованим ${\displaystyle \lambda }$-обчисленням і фрагментом інтуїціоністської логіки висловлювань, що включає тільки імплікації. Наприклад, тип ${\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 і 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(англ.)