Відповідність Каррі — Говарда (ізоморфізм Каррі — Говарда, ) — теорема, або точніше ряд теорем, що показують структурну еквівалентність між математичними доведеннями та програмами, або обчисленнями . Ця еквівалентність може бути формалізована у вигляді ізоморфізму між логічними системами і типізованими лямбда-численнями.
Хаскелл КарріCurry, H. B., Feys, R. Combinatory Logic Vol. I. — Amsterdam: North-Holland, 1958 і Вільям Говард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 помітили, що конструктивне доведення (тобто, доведення в інтуїціоністській логіці) схожа на програму, яка обчислює висновок, а саме висловлювання конструктивної логіки за своєю структурою схожі з типами виразів лямбда-числення — програм для обчислювальної машини.
Відповідність Каррі — Говарда не обмежується якоюсь однією логікою або системою типів. Наприклад, інтуїционістське числення висловлювань відповідає простому типізованому λ-численню, логіка висловлювань другого порядку — поліморфному λ-численню, числення предикатів — λ-численню з залежними типами.
У рамках ізоморфізму Каррі — Говарда наступні структурні елементи розглядаються як еквівалентні:
Логічні системи Мови програмування Висловлювання Тип Доказ висловлювання Ρ Терм (вираз) типу Ρ Затвердження Ρ можна довести Тип Ρ населений Імплікація Ρ ⇒ Q Функціональний тип Ρ →Q Кон'юнкція Ρ ∧ Q Тип множення (пари) Ρ × Q Диз'юнкція Ρ ∨ Q Тип суми (розміченого об'єднання) Ρ + Q Справжня формула Одиничний тип Хибна формула Порожній тип (⊥) Квантор загальності ∀ Тип залежного добутку (∏-тип) Квантор існування ∃ Тип залежною суми (∑-тип)
Найпростішим прикладом відповідності Каррі — Говарда може служити ізоморфізм між простим типізованим -обчисленням і фрагментом інтуїціоністської логіки висловлювань, що включає тільки імплікації. Наприклад, тип в простому типізованому лямбда-численні відповідає вислову логіки висловлювань. Для доказу цього висловлювання необхідно сконструювати терм зазначеного типу (якщо це вдається зробити, то про тип кажуть, що він населений), в даному випадку можна пред'явити потрібний терм:, і це означає, що тавтологія доведена.
Використання ізоморфізму Каррі — Говарда дозволило створити цілий клас функціональних мов програмування, середовище виконання яких одночасно є системою автоматичного доказу, таких як Coq, Agda і Epigram (англ.).
Примітки