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

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

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

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

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

Найпростішим прикладом відповідності Каррі — Говарда може служити ізоморфізм між простим типізованим ${\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 (англ.).