WikiSort.ru - Не сортированное

ПОИСК ПО САЙТУ | о проекте

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

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

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

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

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

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

Использование изоморфизма Карри — Ховарда позволило создать целый класс функциональных языков программирования, среда выполнения которых одновременно является системой автоматического доказательства, таких как 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.

Литература

Данная страница на сайте WikiSort.ru содержит текст со страницы сайта "Википедия".

Если Вы хотите её отредактировать, то можете сделать это на странице редактирования в Википедии.

Если сделанные Вами правки не будут кем-нибудь удалены, то через несколько дней они появятся на сайте WikiSort.ru .




Текст в блоке "Читать" взят с сайта "Википедия" и доступен по лицензии Creative Commons Attribution-ShareAlike; в отдельных случаях могут действовать дополнительные условия.

Другой контент может иметь иную лицензию. Перед использованием материалов сайта WikiSort.ru внимательно изучите правила лицензирования конкретных элементов наполнения сайта.

2019-2024
WikiSort.ru - проект по пересортировке и дополнению контента Википедии