Соответствие Карри — Ховарда: различия между версиями

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

 

 

 

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

Простейшим примером соответствия Карри — Ховарда может служить [[изоморфизм]] между простым типизированным λ-исчислением и фрагментом [[Интуиционизм|интуиционистской логики высказываний]], включающим только [[Импликация|импликацию]]. Например, тип <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> доказана.

 

 

== Примечания ==