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

Материал из Википедии — свободной энциклопедии
Перейти к: навигация, поиск

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

Хаскелл Карри[1] и Уильям Ховард (англ.)[2] заметили, что построение конструктивного доказательства похоже на описание вычислений, а высказывания конструктивной логики по своей структуре схожи с типами вычисляемых выражений — программ для вычислительной машины.

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

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

Логические системы Языки программирования
Высказывание Тип
Доказательство высказывания P Терм (выражение) типа P
Утверждение P доказуемо Тип P обитаем
Импликация P \Rightarrow Q Функциональный тип P \rightarrow Q
Конъюнкция P \and Q Тип произведения (пары) P \times Q
Дизъюнкция P \or Q Тип суммы (размеченного объединения) P + Q
Истинная формула Единичный тип
Ложная формула Пустой тип (\bot)
Квантор всеобщности \forall Тип зависимого произведения (\Pi-тип)
Квантор существования \exists Тип зависимой суммы (\Sigma-тип)

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

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

Литература[править | править исходный текст]