Русская Википедия:Соответствие Карри — Ховарда
Соответствие Карри — Ховарда (изоморфизм Карри — Ховарда, Шаблон:Lang-en) — наблюдаемая структурная эквивалентность между математическими доказательствами и программами, которая может быть формализована в виде изоморфизма между логическими системами и типизированными исчислениями.
Хаскелл Карри[1] и en (William Alvin Howard)[2] заметили, что построение конструктивного доказательства похоже на описание вычислений, а высказывания конструктивной логики по своей структуре схожи с типами вычисляемых выражений — программ для вычислительной машины. Ранние проявления этой связи — Шаблон:Iw (1925), задающая семантику интуиционистской логики через вычисления доказательств, и теория Шаблон:Iw Клини (1945).
Соответствие Карри — Ховарда в современном представлении не ограничивается какой-то одной логикой или системой типов. Например, логика высказываний соответствует простому типизированному λ-исчислению, en (Second-order propositional logic) — полиморфному λ-исчислению, исчисление предикатов — λ-исчислению с зависимыми типами.
В рамках изоморфизма Карри — Ховарда следующие структурные элементы рассматриваются как эквивалентные:
| Логические системы | Языки программирования |
|---|---|
| Высказывание | Тип |
| Доказательство высказывания <math>P</math> | Терм (выражение) типа <math>P</math> |
| Утверждение <math>P</math> доказуемо | Тип <math>P</math> обитаем |
| Импликация <math>P \Rightarrow Q</math> | Функциональный тип <math>P \rightarrow Q</math> |
| Конъюнкция <math>P \land Q</math> | Тип произведения (пары) <math>P \times Q</math> |
| Дизъюнкция <math>P \lor Q</math> | Тип суммы (размеченного объединения) <math>P + Q</math> |
| Истинная формула | Единичный тип |
| Ложная формула | Пустой тип (<math>\bot</math>) |
| Квантор всеобщности <math>\forall</math> | Тип зависимого произведения (<math>\Pi</math>-тип) |
| Квантор существования <math>\exists</math> | Тип зависимой суммы (<math>\Sigma</math>-тип) |
Простейшим примером соответствия Карри — Ховарда может служить изоморфизм между простым типизированным λ-исчислением и фрагментом интуиционистской логики высказываний, включающим только импликацию. Например, тип <math>(P \rightarrow Q \rightarrow R) \rightarrow (P \rightarrow Q) \rightarrow P \rightarrow R</math> в простом типизированном лямбда-исчислении соответствует высказыванию <math>(P \Rightarrow (Q \Rightarrow R)) \Rightarrow ((P \Rightarrow Q) \Rightarrow (P \Rightarrow R))</math> логики высказываний. Для доказательства этого высказывания необходимо сконструировать терм указанного типа (если это удаётся сделать, то про тип говорят, что он обитаем или населён), в данном случае можно предъявить нужный терм: <math>\lambda f g x \rightarrow f x (g x)</math>, и это значит, что тавтология <math>(P \Rightarrow (Q \Rightarrow R)) \Rightarrow ((P \Rightarrow Q) \Rightarrow (P \Rightarrow R))</math> доказана.
Использование изоморфизма Карри — Ховарда позволило создать целый класс функциональных языков программирования, среда выполнения которых одновременно является системой автоматического доказательства, таких как Coq, Agda и [[|en]] (Epigram (programming language)).
Примечания
Литература
- Шаблон:Книга
- Перевод на русский язык: Шаблон:Книга
