Interested Article - Соответствие Карри — Ховарда

Соответствие Карри — Ховарда ( изоморфизм Карри — Ховарда , англ. formulæ-as-types interpretation ) — наблюдаемая структурная эквивалентность между математическими доказательствами и программами , которая может быть формализована в виде изоморфизма между логическими системами и типизированными исчислениями.

Хаскелл Карри и заметили, что построение конструктивного доказательства похоже на описание вычислений, а высказывания конструктивной логики по своей структуре схожи с типами вычисляемых выражений — программ для вычислительной машины . Ранние проявления этой связи — (1925), задающая семантику интуиционистской логики через вычисления доказательств, и теория Клини (1945).

Соответствие Карри — Ховарда в современном представлении не ограничивается какой-то одной логикой или системой типов. Например, логика высказываний соответствует простому типизированному λ-исчислению , полиморфному λ-исчислению , исчисление предикатов λ-исчислению с зависимыми типами .

В рамках изоморфизма Карри — Ховарда следующие структурные элементы рассматриваются как эквивалентные:

Логические системы Языки программирования
Высказывание Тип
Доказательство высказывания Терм (выражение) типа
Утверждение доказуемо Тип обитаем
Импликация Функциональный тип
Конъюнкция Тип произведения (пары)
Дизъюнкция Тип суммы (размеченного объединения)
Истинная формула Единичный тип
Ложная формула Пустой тип ( )
Квантор всеобщности Тип зависимого произведения ( -тип)
Квантор существования Тип зависимой суммы ( -тип)

Простейшим примером соответствия Карри — Ховарда может служить изоморфизм между простым типизированным λ-исчислением и фрагментом интуиционистской логики высказываний , включающим только импликацию . Например, тип в простом типизированном лямбда-исчислении соответствует высказыванию логики высказываний. Для доказательства этого высказывания необходимо сконструировать терм указанного типа (если это удаётся сделать, то про тип говорят, что он обитаем или населён ), в данном случае можно предъявить нужный терм: , и это значит, что тавтология доказана.

Использование изоморфизма Карри — Ховарда позволило создать целый класс функциональных языков программирования , среда выполнения которых одновременно является системой автоматического доказательства , таких как Coq , Agda и .

Примечания

  1. Curry, H. B., Feys, R. Combinatory Logic Vol. I. — Amsterdam : , 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 .

Литература

  • Pierce, Benjamin C. Types and Programming Languages. — MIT Press , 2002. — ISBN 0-262-16209-1 .
    • Перевод на русский язык: Пирс Б. Типы в языках программирования. — , 2012. — 680 с. — ISBN 978-5-7913-0082-9 .
Источник —

Same as Соответствие Карри — Ховарда