Соответствие Карри — Ховарда: различия между версиями
| [отпатрулированная версия] | [непроверенная версия] |
Содержимое удалено Содержимое добавлено
Bezik (обсуждение | вклад) одел в латекс, оформление |
Deniok (обсуждение | вклад) Нет описания правки |
||
Строка 3:
[[Хаскелл Карри]]<ref name="CurryFeys58" /> и {{Не переведено|есть=:en:William Alvin Howard|надо=Ховард, Уильям|текст=Уильям Ховард}}<ref name="Howard69" /> заметили, что построение [[Конструктивная математика|конструктивного доказательства]] похоже на описание вычислений, а высказывания конструктивной логики по своей структуре схожи с типами вычисляемых выражений — программ для [[Вычислительная машина|вычислительной машины]].
Соответствие Карри — Ховарда не ограничивается какой-то одной логикой или системой типов. Например, [[логика высказываний]] соответствует
В рамках изоморфизма Карри — Ховарда следующие структурные элементы рассматриваются как эквивалентные:
| |||