Википедия

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

Интерактивная навигация по истории
[отпатрулированная версия][отпатрулированная версия]
← Предыдущая правкаСледующая правка →
Содержимое удалено Содержимое добавлено
ВизуальныйВики-текст
поддержка переименования и замечаний на моей СО
Нет описания правки
Строка 1:
'''Соответствие Карри — Ховарда''' (''изоморфизм Карри — Ховарда'', {{lang-en|formulae-as-types interpretation}}) — соотношение,наблюдаемая устанавливающееструктурная структурное соответствиеэквивалентность между [[Математическое доказательство|математическими доказательствами]] и [[Компьютерная программа|программами]]. ПроявляетсяЭта наэквивалентность различныхможет уровнях:быть [[логикаформализована высказываний]]в соотноситсявиде сизоморфизма {{Немежду переведено|есть=:en:Simplyлогическими typedсистемами lambdaи calculus|Простоетипизированными типизированноеисчислениями. лямбда-исчисление|простым типизированным λ-исчислением}}, [[исчисление предикатов]] с [[Зависимые типы|зависимыми типами]], [[пропозициональная логика второго порядка]] — с [[Полиморфизм (программирование)|полиморфными типами]].
 
[[Хаскелл Карри]]<ref name="CurryFeys58" /> и {{Не переведено|есть=:en:William Alvin Howard|надо=Ховард, Уильям|текст=Уильям Ховард}}<ref name="Howard69" /> заметили, что построение [[Конструктивная математика|конструктивного доказательства]] похоже на описание вычислений, а высказывания конструктивной логики по своей структуре схожи с типами вычисляемых выражений — программ для [[Вычислительная машина|вычислительной машины]].
 
Соответствие Карри — Ховарда не ограничивается какой-то одной логикой или системой типов. Например, [[логика высказываний]] соответствует {{Не переведено|есть=:en:Simply typed lambda calculus|Простое типизированное лямбда-исчисление|простому типизированному λ-исчислению}}, [[пропозициональная логика второго порядка]] — [[Полиморфизм (программирование)|полиморфному λ-исчислению]], [[исчисление предикатов]] — [[Зависимые типы| λ-исчислению с зависимыми типами]].
Изоморфизм Карри — Ховарда на уровне соответствия между исчислением предикатов и зависимыми типами:
 
В рамках изоморфизма Карри — Ховарда следующие структурные элементы рассматриваются как эквивалентные
{| class="wikitable"
|-
Строка 29 ⟶ 31 :
|}
 
Простейшим примером изоморфизма Карри — Ховарда может служить [[изоморфизм]] между простым типизированным лямбда-исчислением и фрагментом [[Интуиционизм|интуиционистской логики высказываний]], включающим только [[Импликация|импликацию]],. например,Рассмотрим наличие терма типатип (P → Q → R) → (P → Q) → P → R (λв простом типизированном лямбда-термаисчислении. Он соответствует высказыванию (P ⇒ (Q ⇒ R)) ⇒ ((P ⇒ Q) ⇒ (P ⇒ R)) логики высказываний. Для доказательства этого высказывания мы должны сконструировать терм указанного типа (если это удаётся сделать, то про тип говорят, что он обитаем или населён). В нашем случае мы можем предъявить нужный терм: λ f g x → f x (g x)). можноЭто интерпретировать какзначит, доказательствочто [[Тавтология (логика)|тавтологиитавтология]] (P ⇒ (Q ⇒ R)) ⇒ ((P ⇒ Q) ⇒ (P ⇒ R)) доказана.
 
 
Использование изоморфизма Карри — Ховарда позволило создать целый класс [[Язык функционального программирования|функциональных языков программирования]], среда выполнения которых одновременно является системой [[Автоматическое доказательство|автоматического доказательства]], таких как [[Coq]], [[Agda]] и {{Не переведено|есть=:en:Epigram (programming language)|надо=Epigram}}.
Источник — https://ru.wikipedia.org/wiki/Соответствие_Карри_—_Ховарда