Соответствие Карри — Ховарда
Соответствие Карри — Ховарда (изоморфизм Карри — Ховарда, англ. formulæ-as-types interpretation) — наблюдаемая структурная эквивалентность между математическими доказательствами и программами, которая может быть формализована в виде изоморфизма между логическими системами и типизированными исчислениями.
Хаскелл Карри[1] и Уильям Ховард[2] заметили, что построение конструктивного доказательства похоже на описание вычислений, а высказывания конструктивной логики по своей структуре схожи с типами вычисляемых выражений — программ для вычислительной машины. Ранние проявления этой связи — интерпретация Брауэра — Гейтинга — Колмогорова (1925), задающая семантику интуиционистской логики через вычисления доказательств, и теория реализуемости Клини (1945).
Соответствие Карри — Ховарда в современном представлении не ограничивается какой-то одной логикой или системой типов. Например, логика высказываний соответствует простому типизированному λ-исчислению, логика высказываний второго порядка — полиморфному λ-исчислению, исчисление предикатов — λ-исчислению с зависимыми типами.
В рамках изоморфизма Карри — Ховарда следующие структурные элементы рассматриваются как эквивалентные:
Логические системы | Языки программирования |
---|---|
Высказывание | Тип |
Доказательство высказывания | Терм (выражение) типа |
Утверждение доказуемо | Тип обитаем |
Импликация | Функциональный тип |
Конъюнкция | Тип произведения (пары) |
Дизъюнкция | Тип суммы (размеченного объединения) |
Истинная формула | Единичный тип |
Ложная формула | Пустой тип () |
Квантор всеобщности | Тип зависимого произведения (-тип) |
Квантор существования | Тип зависимой суммы (-тип) |
Простейшим примером соответствия Карри — Ховарда может служить изоморфизм между простым типизированным λ-исчислением и фрагментом интуиционистской логики высказываний, включающим только импликацию. Например, тип в простом типизированном лямбда-исчислении соответствует высказыванию логики высказываний. Для доказательства этого высказывания необходимо сконструировать терм указанного типа (если это удаётся сделать, то про тип говорят, что он обитаем или населён), в данном случае можно предъявить нужный терм: , и это значит, что тавтология доказана.
Использование изоморфизма Карри — Ховарда позволило создать целый класс функциональных языков программирования, среда выполнения которых одновременно является системой автоматического доказательства, таких как 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.
Литература
- Pierce, Benjamin C. Types and Programming Languages. — MIT Press, 2002. — ISBN 0-262-16209-1.
- Перевод на русский язык: Пирс Б. Типы в языках программирования. — Добросвет, 2012. — 680 с. — ISBN 978-5-7913-0082-9.