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