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

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

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

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

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

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

Найпростішим прикладом відповідності Каррі — Говарда може служити ізоморфізм між простим типізованим -обчисленням і фрагментом інтуіціоністської логіки висловлювань, що включає тільки імплікації. Наприклад, тип в простому типизированному лямбда-численні відповідає вислову логіки висловлювань. Для доказу цього висловлювання необхідно сконструювати терм зазначеного типу (якщо це вдається зробити, то про тип кажуть, що він населений), в даному випадку можна пред'явити потрібний терм:, і це означає, що тавтологія доведена.

Використання ізоморфізму Каррі — Говарда дозволило створити цілий клас функціональних мов програмування, середовище виконання яких одночасно є системою автоматичного доказу, таких як 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(англ.)
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.