Відповідність Каррі — Говарда (ізоморфізм Каррі — Говарда, англ. Curry-Howard Isomorphism) — теорема, або точніше ряд теорем, що показують структурну еквівалентність між математичними доведеннями та програмами, або обчисленнями англ. computations. Ця еквівалентність може бути формалізована у вигляді ізоморфізму між логічними системами і типізованими лямбда-численнями.
Хаскелл Каррі і Вільям Говард помітили, що конструктивне доведення (тобто, доведення в інтуїціоністській логіці) схожа на програму, яка обчислює висновок, а саме висловлювання конструктивної логіки за своєю структурою схожі з типами виразів лямбда-числення — програм для обчислювальної машини.
Відповідність Каррі — Говарда не обмежується якоюсь однією логікою або системою типів. Наприклад, інтуїционістське числення висловлювань відповідає простому типізованому λ-численню, логіка висловлювань другого порядку — (поліморфному λ-численню), числення предикатів — λ-численню з (залежними типами).
У рамках ізоморфізму Каррі — Говарда наступні структурні елементи розглядаються як еквівалентні:
Логічні системи | Мови програмування |
---|---|
Висловлювання | Тип |
Доказ висловлювання Ρ | Терм (вираз) типу Ρ |
Затвердження Ρ можна довести | Тип Ρ населений |
Імплікація Ρ ⇒ Q | Функціональний тип Ρ →Q |
Кон'юнкція Ρ ∧ Q | Тип множення (пари) Ρ × Q |
Диз'юнкція Ρ ∨ Q | Тип суми (розміченого об'єднання) Ρ + Q |
Справжня формула | Одиничний тип |
Хибна формула | Порожній тип (⊥) |
Квантор загальності ∀ | Тип залежного добутку (∏-тип) |
Квантор існування ∃ | Тип залежною суми (∑-тип) |
Найпростішим прикладом відповідності Каррі — Говарда може служити ізоморфізм між простим типізованим -обчисленням і фрагментом інтуїціоністської логіки висловлювань, що включає тільки імплікації. Наприклад, тип в простому типізованому лямбда-численні відповідає вислову логіки висловлювань. Для доказу цього висловлювання необхідно сконструювати терм зазначеного типу (якщо це вдається зробити, то про тип кажуть, що він населений), в даному випадку можна пред'явити потрібний терм:, і це означає, що тавтологія доведена.
Використання ізоморфізму Каррі — Говарда дозволило створити цілий клас функціональних мов програмування, середовище виконання яких одночасно є системою автоматичного доказу, таких як Coq, Agda і Epigram (англ.).
Примітки
- 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(англ.)
Вікіпедія, Українська, Україна, книга, книги, бібліотека, стаття, читати, завантажити, безкоштовно, безкоштовно завантажити, mp3, відео, mp4, 3gp, jpg, jpeg, gif, png, малюнок, музика, пісня, фільм, книга, гра, ігри, мобільний, телефон, android, ios, apple, мобільний телефон, samsung, iphone, xiomi, xiaomi, redmi, honor, oppo, nokia, sonya, mi, ПК, web, Інтернет