Переписка Карри–Говарда

Изоморфизм между компьютерными программами и конструктивными математическими доказательствами

В теории языков программирования и теории доказательств соответствие Карри–Ховарда — это прямая связь между компьютерными программами и математическими доказательствами . Оно также известно как изоморфизм или эквивалентность Карри–Ховарда , или интерпретация доказательств-как-программ и предложений -или формул-как-типов .

Это обобщение синтаксической аналогии между системами формальной логики и вычислительными исчислениями, впервые обнаруженной американским математиком Хаскеллом Карри и логиком Уильямом Элвином Говардом . ^[1] Именно связь между логикой и вычислениями обычно приписывается Карри и Говарду, хотя эта идея связана с операционной интерпретацией интуиционистской логики, данной в различных формулировках Л. Э. Дж. Брауэром , Арендом Гейтингом и Андреем Колмогоровым (см. Интерпретация Брауэра–Гейтинга–Колмогорова ) ^[2] и Стивеном Клини (см. Реализуемость ). Связь была расширена и теперь включает теорию категорий как трехстороннее соответствие Карри–Говарда–Ламбека . ^{[3] [4] [5]}

Происхождение, сфера применения и последствия

Начало переписки Карри и Ховарда кроется в нескольких наблюдениях:

1. В 1934 году Карри заметил, что типы комбинаторов можно рассматривать как аксиоматические схемы для интуиционистской импликационной логики. ^[6]
2. В 1958 году он заметил, что определенный вид системы доказательства , называемый системой вывода в стиле Гильберта , совпадает в некотором фрагменте с типизированным фрагментом стандартной модели вычисления, известной как комбинаторная логика . ^[7]
3. В 1969 году Говард заметил, что другая, более «высокоуровневая» система доказательств , называемая естественной дедукцией , может быть непосредственно интерпретирована в ее интуиционистской версии как типизированный вариант модели вычислений, известной как лямбда-исчисление . ^[8]

Соответствие Карри–Ховарда — это наблюдение, что существует изоморфизм между системами доказательств и моделями вычислений. Это утверждение, что эти два семейства формализмов можно считать идентичными.

Если абстрагироваться от особенностей любого формализма, то возникает следующее обобщение: доказательство — это программа, а доказываемая ею формула — это тип программы . Более неформально это можно рассматривать как аналогию , которая утверждает, что возвращаемый тип функции (т. е. тип значений, возвращаемых функцией) аналогичен логической теореме, при условии, что гипотезы соответствуют типам значений аргументов, переданных функции; и что программа для вычисления этой функции аналогична доказательству этой теоремы. Это устанавливает форму логического программирования на строгом фундаменте: доказательства могут быть представлены как программы, и особенно как лямбда-термы , или доказательства могут быть запущены .

Соответствие стало отправной точкой большого спектра новых исследований после его открытия, что привело, в частности, к новому классу формальных систем, разработанных для работы как в качестве системы доказательств , так и в качестве типизированного функционального языка программирования . Сюда входят интуиционистская теория типов Мартина-Лёфа и исчисление конструкций Коканда , два исчисления, в которых доказательства являются обычными объектами дискурса и в которых можно устанавливать свойства доказательств так же, как и свойств любой программы. Эту область исследований обычно называют современной теорией типов .

Такие типизированные лямбда-исчисления, полученные из парадигмы Карри–Ховарда, привели к появлению программного обеспечения, такого как Coq , в котором доказательства, рассматриваемые как программы, могут быть формализованы, проверены и запущены.

Обратное направление — использовать программу для извлечения доказательства , учитывая его правильность — область исследований, тесно связанная с кодом, содержащим доказательство . Это осуществимо только в том случае, если язык программирования , на котором написана программа, очень богато типизирован: разработка таких систем типов была частично мотивирована желанием сделать соответствие Карри–Ховарда практически значимым.

Переписка Карри–Ховарда также подняла новые вопросы относительно вычислительного содержания концепций доказательства, которые не были охвачены оригинальными работами Карри и Ховарда. В частности, было показано, что классическая логика соответствует способности манипулировать продолжением программ и симметрией секвенциального исчисления для выражения дуальности между двумя стратегиями оценки, известными как вызов по имени и вызов по значению.

Из-за возможности написания незавершающихся программ, Тьюринг-полные модели вычислений (такие как языки с произвольными рекурсивными функциями ) должны интерпретироваться с осторожностью, поскольку наивное применение соответствия приводит к непоследовательной логике. Лучший способ работы с произвольными вычислениями с логической точки зрения все еще является активно обсуждаемым исследовательским вопросом, но один популярный подход основан на использовании монад для разделения доказуемо завершающегося от потенциально незавершающегося кода (подход, который также обобщается на гораздо более богатые модели вычислений, ^[9] и сам по себе связан с модальной логикой естественным расширением изоморфизма Карри-Ховарда ^{[ext 1]} ). Более радикальный подход, пропагандируемый полным функциональным программированием , заключается в устранении неограниченной рекурсии (и отказе от полноты по Тьюрингу , хотя все еще сохраняя высокую вычислительную сложность), используя более контролируемую корекурсию везде, где на самом деле желательно незавершающееся поведение.

Общая формулировка

В более общей формулировке соответствие Карри–Ховарда — это соответствие между формальными исчислениями доказательств и системами типов для моделей вычислений . В частности, оно распадается на два соответствия. Одно на уровне формул и типов , которое не зависит от того, какая конкретная система доказательств или модель вычислений рассматривается, и одно на уровне доказательств и программ , которое на этот раз специфично для конкретного выбора рассматриваемой системы доказательств и модели вычислений.

На уровне формул и типов соответствие говорит, что импликация ведет себя так же, как тип функции, конъюнкция — как тип «произведения» (это может называться кортежем, структурой, списком или каким-либо другим термином в зависимости от языка), дизъюнкция — как тип суммы (этот тип может называться объединением), ложная формула — как пустой тип, а истинная формула — как тип единицы (единственным членом которого является нулевой объект). Квантификаторы соответствуют зависимому функциональному пространству или произведениям (в зависимости от ситуации). Это суммировано в следующей таблице:

На уровне систем доказательств и моделей вычислений соответствие в основном показывает идентичность структуры, во-первых, между некоторыми частными формулировками систем, известных как система вывода в стиле Гильберта и комбинаторная логика , и, во-вторых, между некоторыми частными формулировками систем, известных как естественная дедукция и лямбда-исчисление .

Между системой натурального вывода и лямбда-исчислением существуют следующие соответствия:

Соответствующие системы

Интуиционистские системы вывода в стиле Гильберта и типизированная комбинаторная логика

В начале это было простое замечание в книге Карри и Фейса 1958 года по комбинаторной логике: простейшие типы для основных комбинаторов K и S комбинаторной логики удивительным образом соответствовали соответствующим схемам аксиом α → ( β → α ) и ( α → ( β → γ )) → (( α → β ) → ( α → γ )), используемым в системах вывода в стиле Гильберта . По этой причине эти схемы теперь часто называют аксиомами K и S. Примеры программ, рассматриваемых как доказательства в логике в стиле Гильберта, приведены ниже.

Если ограничиться импликационным интуиционистским фрагментом, то простой способ формализовать логику в стиле Гильберта заключается в следующем. Пусть Γ — конечный набор формул, рассматриваемых как гипотезы. Тогда δ выводима из Γ, обозначаемая Γ ⊢ δ, в следующих случаях:

• δ — гипотеза, т.е. это формула Γ,
• δ является примером схемы аксиом, т.е. в рамках наиболее распространенной системы аксиом:
  • δ имеет вид α → ( β → α ), или
  • δ имеет вид ( α → ( β → γ )) → (( α → β ) → ( α → γ )),
• δ следует из дедукции, т.е. для некоторого α , как α → δ , так и α уже выводимы из Γ (это правило modus ponens )

Это можно формализовать с помощью правил вывода , как в левом столбце следующей таблицы.

Типизированную комбинаторную логику можно сформулировать с использованием похожего синтаксиса: пусть Γ будет конечным набором переменных, аннотированных их типами. Термин T (также аннотированный своим типом) будет зависеть от этих переменных [Γ ⊢ T: δ ], когда:

• T — одна из переменных в Γ,
• T — базовый комбинатор, т.е. в соответствии с наиболее распространенным базисом комбинатора:
  • T есть K: α → ( β → α ) [где α и β обозначают типы его аргументов], или
  • T есть S:( α → ( β → γ )) → (( α → β ) → ( α → γ )),
• T — это композиция двух подтермов, которые зависят от переменных в Γ.

Определенные здесь правила генерации приведены в правом столбце ниже. Замечание Карри просто утверждает, что оба столбца находятся во взаимно-однозначном соответствии. Ограничение соответствия интуиционистской логикой означает, что некоторые классические тавтологии , такие как закон Пирса (( α → β ) → α ) → α , исключаются из соответствия.

Рассматривая это на более абстрактном уровне, соответствие можно переформулировать так, как показано в следующей таблице. В частности, теорема о дедукции, характерная для логики в стиле Гильберта, соответствует процессу устранения абстракции комбинаторной логики.

Благодаря соответствию результаты комбинаторной логики могут быть перенесены в логику Гильберта и наоборот. Например, понятие сокращения терминов в комбинаторной логике может быть перенесено в логику Гильберта, и это дает способ канонического преобразования доказательств в другие доказательства того же утверждения. Можно также перенести понятие нормальных терминов в понятие нормальных доказательств, выражая, что гипотезы аксиом никогда не должны быть полностью отделены (поскольку в противном случае может произойти упрощение).

Наоборот, недоказуемость закона Пирса в интуиционистской логике может быть перенесена обратно в комбинаторную логику: не существует типизированного термина комбинаторной логики, который типизируется с помощью типа

(( α → β ) → α ) → α .

Результаты о полноте некоторых наборов комбинаторов или аксиом также могут быть переданы. Например, тот факт, что комбинатор X составляет одноточечную основу (экстенсиональной) комбинаторной логики, подразумевает, что схема с одной аксиомой

((( α → ( β → γ )) → (( α → β ) → ( α → γ ))) → (( δ → ( ε → δ )) → ζ )) → ζ ,

который является основным типом X , является адекватной заменой комбинации схем аксиом

α → ( β → α ) и

( α → ( β → γ )) → (( α → β ) → ( α → γ )).

Интуиционистская естественная дедукция и типизированное лямбда-исчисление

После того, как Карри подчеркнул синтаксическое соответствие между интуиционистским выводом в стиле Гильберта и типизированной комбинаторной логикой , Говард в 1969 году явно сформулировал синтаксическую аналогию между программами просто типизированного лямбда-исчисления и доказательствами естественной дедукции . Ниже левая часть формализует интуиционистский импликативный естественный вывод как исчисление секвенций (использование секвенций является стандартным при обсуждении изоморфизма Карри–Говарда, поскольку позволяет более четко сформулировать правила вывода) с неявным ослаблением, а правая часть показывает правила типизации лямбда-исчисления . В левой части Γ, Γ ₁ и Γ ₂ обозначают упорядоченные последовательности формул, тогда как в правой части они обозначают последовательности именованных (т. е. типизированных) формул со всеми разными именами.

Перефразируя соответствие, доказательство Γ ⊢ α означает наличие программы, которая, учитывая значения с типами, перечисленными в Γ, производит объект типа α . Аксиома/гипотеза соответствует введению новой переменной с новым, неограниченным типом, правило →  I соответствует абстракции функции, а правило →  E соответствует применению функции. Обратите внимание, что соответствие не является точным, если контекст Γ рассматривается как набор формул, например, λ-термы λ x .λ y . x и λ x .λ y . y типа α → α → α не будут различаться в соответствии. Примеры приведены ниже.

Говард показал, что соответствие распространяется на другие связки логики и другие конструкции просто типизированного лямбда-исчисления. Рассматриваемое на абстрактном уровне соответствие может быть суммировано, как показано в следующей таблице. В частности, оно также показывает, что понятие нормальных форм в лямбда-исчислении соответствует понятию Правитца о нормальной дедукции в естественной дедукции , из чего следует, что алгоритмы для проблемы заселения типов могут быть превращены в алгоритмы для решения интуиционистской доказуемости.

Соответствие Говарда естественным образом распространяется на другие расширения естественной дедукции и простого типизированного лямбда-исчисления . Вот неполный список:

• Система Жирара-Рейнольдса F как общий язык для логики высказываний второго порядка и полиморфного лямбда-исчисления,
• логика высшего порядка и система Жирара F ω
• индуктивные типы как алгебраические типы данных
• необходимость в модальной логике и поэтапном вычислении ^{[ext 2]} ${\displaystyle \Box }$
• возможность в модальной логике и монадических типах для эффектов ^{[ext 1]} ${\displaystyle \Diamond }$
• Исчисление λ _I (где абстракция ограничена λx . E , где x имеет по крайней мере одно свободное вхождение в E) и исчисление CL _I соответствуют соответствующей логике . ^[10]
• Модальность локальной истинности (∇) в топологии Гротендика или эквивалентная ей «слабая» модальность (◯) Бентона, Бирмана и де Пайвы (1998) соответствуют CL-логике, описывающей «типы вычислений». ^[11]

Классическая логика и операторы управления

Во времена Карри, а также во времена Говарда соответствие доказательств-как-программ касалось только интуиционистской логики , т. е. логики, в которой, в частности, закон Пирса не был выводим. Расширение соответствия до закона Пирса и, следовательно, до классической логики стало ясно из работы Гриффина по типизации операторов, которые захватывают контекст оценки выполнения данной программы, так что этот контекст оценки может быть позже переустановлен. Базовое соответствие в стиле Карри–Говарда для классической логики приведено ниже. Обратите внимание на соответствие между трансляцией двойного отрицания, используемой для отображения классических доказательств в интуиционистскую логику, и трансляцией в стиле продолжения-передачи, используемой для отображения лямбда-терминов, включающих управление, в чистые лямбда-термины. Более конкретно, трансляции в стиле продолжения-передачи вызова по имени относятся к трансляции двойного отрицания Колмогорова , а трансляции в стиле продолжения-передачи вызова по значению относятся к своего рода трансляции двойного отрицания, предложенной Куродой.

Более тонкое соответствие Карри–Ховарда существует для классической логики, если определить классическую логику не добавлением аксиомы, такой как закон Пирса , а допущением нескольких заключений в секвенциях. В случае классической естественной дедукции существует соответствие доказательства-как-программы с типизированными программами λμ-исчисления Париго .

Последовательное исчисление

Соответствие доказательств как программ может быть установлено для формализма, известного как секвенциальное исчисление Генцена , но это не соответствие с четко определенной ранее существовавшей моделью вычислений, как это было для выводов в стиле Гильберта и естественных выводов.

Последовательное исчисление характеризуется наличием левых правил введения, правых правил введения и правила сечения, которое может быть устранено. Структура последовательного исчисления относится к исчислению, структура которого близка к структуре некоторых абстрактных машин . Неформальное соответствие следующее:

Связанные соответствия доказательств-как-программ

Роль де Брейна

NG de Bruijn использовал лямбда-нотацию для представления доказательств программы проверки теорем Automath и представлял предложения как «категории» их доказательств. Это было в конце 1960-х годов, в то же время, когда Говард написал свою рукопись; де Брейн, вероятно, не знал о работе Говарда и установил соответствие независимо (Sørensen & Urzyczyn [1998] 2006, стр. 98–99). Некоторые исследователи склонны использовать термин соответствие Карри–Говарда–де Брейна вместо соответствия Карри–Говарда.

интерпретация BHK

Интерпретация BHK интерпретирует интуиционистские доказательства как функции, но не определяет класс функций, релевантных для интерпретации. Если взять лямбда-исчисление для этого класса функций, то интерпретация BHK говорит то же самое, что и соответствие Говарда между естественной дедукцией и лямбда-исчислением.

Реализуемость

Рекурсивная реализуемость Клини разбивает доказательства интуиционистской арифметики на пару рекурсивной функции и доказательства формулы, выражающей, что рекурсивная функция «реализует», т.е. правильно реализует дизъюнкции и кванторы существования исходной формулы, так что формула становится истинной.

Модифицированная реализуемость Крейзеля применяется к интуиционистской логике предикатов высшего порядка и показывает, что просто типизированный лямбда-терм, индуктивно извлеченный из доказательства, реализует исходную формулу. В случае пропозициональной логики это совпадает с утверждением Говарда: извлеченный лямбда-терм является самим доказательством (рассматриваемым как нетипизированный лямбда-терм), а утверждение реализуемости является парафразом того факта, что извлеченный лямбда-терм имеет тип, который означает формула (рассматриваемый как тип).

Интерпретация диалектики Гёделя реализует (расширение) интуиционистской арифметики с вычислимыми функциями. Связь с лямбда-исчислением неясна, даже в случае естественной дедукции.

Соответствие Карри–Ховарда–Ламбека

Иоахим Ламбек показал в начале 1970-х годов, что доказательства интуиционистской пропозициональной логики и комбинаторы типизированной комбинаторной логики имеют общую эквациональную теорию, теорию декартовых замкнутых категорий . Выражение соответствие Карри–Ховарда–Ламбека теперь используется некоторыми людьми ^{[ кем? ]} для обозначения отношений между интуиционистской логикой, типизированным лямбда-исчислением и декартовыми замкнутыми категориями. При этом соответствии объекты декартово-замкнутой категории могут интерпретироваться как предложения (типы), а морфизмы — как выводы, отображающие набор предположений ( контекст типизации ) в допустимый консеквент (хорошо типизированный термин). ^[12]

Соответствие Ламбека является соответствием эквациональных теорий, абстрагируясь от динамики вычислений, таких как бета-редукция и нормализация терминов, и не является выражением синтаксической идентичности структур, как это имеет место для каждого из соответствий Карри и Говарда: т. е. структура хорошо определенного морфизма в декартово-замкнутой категории не сопоставима со структурой доказательства соответствующего суждения ни в логике Гильберта, ни в естественной дедукции. Например, невозможно утверждать или доказать, что морфизм является нормализующим, установить теорему типа Чёрча-Россера или говорить о "сильно нормализующей" декартово-замкнутой категории. Чтобы прояснить это различие, ниже перефразируется базовая синтаксическая структура декартово-замкнутых категорий.

Объекты (предложения/типы) включают

• ${\displaystyle \top }$как объект
• дано и как объекты, то и как объекты. ${\displaystyle \alpha }$ ${\displaystyle \beta }$ ${\displaystyle \alpha \times \beta }$ ${\displaystyle \alpha \rightarrow \beta }$

Морфизмы (выводы/термины) включают

• идентичности: ${\displaystyle {\text{id}}_{\alpha }:\alpha \to \alpha }$
• композиция: если и являются морфизмами, то является морфизмом ${\displaystyle t:\alpha \to \beta }$ ${\displaystyle u:\beta \to \gamma }$ ${\displaystyle u\circ t:\alpha \to \gamma }$
• Конечные морфизмы : ${\displaystyle \star _{\alpha }:\alpha \to \top }$
• продукты: если и являются морфизмами, является морфизмом ${\displaystyle t:\alpha \to \beta }$ ${\displaystyle u:\alpha \to \gamma }$ ${\displaystyle (t,u):\alpha \to \beta \times \gamma }$
• прогнозы: и ${\displaystyle \pi _{\alpha ,\beta ,1}:\alpha \times \beta \to \alpha }$ ${\displaystyle \pi _{\alpha ,\beta ,2}:\alpha \times \beta \to \beta }$
• оценка: ${\displaystyle {\text{eval}}_{\alpha ,\beta }:(\alpha \to \beta )\times \alpha \to \beta }$
• каррирование: если — морфизм, то — морфизм. ${\displaystyle t:\alpha \times \beta \to \gamma }$ ${\displaystyle \lambda t:\alpha \to \beta \to \gamma }$

Эквивалентно аннотациям выше, хорошо определенные морфизмы (типизированные термины) в любой декартово-замкнутой категории могут быть построены в соответствии со следующими правилами типизации . Обычная нотация категориального морфизма заменяется нотацией контекста типизации . ${\displaystyle f:\alpha \to \beta }$ ${\displaystyle \alpha \vdash f:\beta }$

Личность:

${\displaystyle {\frac {}{\alpha \vdash {\text{id}}:\alpha }}}$

Состав:

${\displaystyle {\frac {\alpha \vdash t:\beta \qquad \beta \vdash u:\gamma }{\alpha \vdash u\circ t:\gamma }}}$

Тип объекта ( конечный объект ):

${\displaystyle {\frac {}{\alpha \vdash \star :\top }}}$

Декартово произведение:

${\displaystyle {\frac {\alpha \vdash t:\beta \qquad \alpha \vdash u:\gamma }{\alpha \vdash (t,u):\beta \times \gamma }}}$

Левая и правая проекция:

${\displaystyle {\frac {}{\alpha \times \beta ~\vdash ~\pi _{1}:\alpha }}\qquad {\frac {}{\alpha \times \beta ~\vdash ~\pi _{2}:\beta }}}$

Каррирование :

${\displaystyle {\frac {\alpha \times \beta ~\vdash ~t:\gamma }{\alpha \vdash \lambda t:\beta \to \gamma }}}$

Приложение :

${\displaystyle {\frac {}{(\alpha \rightarrow \beta )\times \alpha \vdash {\text{eval}}:\beta }}}$

Наконец, уравнения категории имеют вид

• ${\displaystyle {\text{id}}\circ t=t}$
• ${\displaystyle t\circ {\text{id}}=t}$
• ${\displaystyle (v\circ u)\circ t=v\circ (u\circ t)}$
• ${\displaystyle \star ={\text{id}}}$ (если правильно напечатано)
• ${\displaystyle \star \circ u=\star }$
• ${\displaystyle \pi _{1}\circ (t,u)=t}$
• ${\displaystyle \pi _{2}\circ (t,u)=u}$
• ${\displaystyle (\pi _{1},\pi _{2})=id}$
• ${\displaystyle (t_{1},t_{2})\circ u=(t_{1}\circ u,t_{2}\circ u)}$
• ${\displaystyle {\text{eval}}\circ (\lambda t\circ \pi _{1},\pi _{2})=t}$
• ${\displaystyle \lambda {\text{eval}}={\text{id}}}$
• ${\displaystyle \lambda t\circ u=\lambda (t\circ (u\circ \pi _{1},\pi _{2}))}$

Из этих уравнений следуют следующие законы: ${\displaystyle \eta }$

• ${\displaystyle (\pi _{1}\circ t,\pi _{2}\circ t)=t}$
• ${\displaystyle \lambda ({\text{eval}}\circ (t\circ \pi _{1},\pi _{2}))=t}$

Теперь существует t такое, что тогда и только тогда доказуемо в импликационной интуиционистской логике. ${\displaystyle \alpha _{1}\times \ldots \times \alpha _{n}\vdash t:\beta }$ ${\displaystyle \alpha _{1},\ldots ,\alpha _{n}\vdash \beta }$

Примеры

Благодаря соответствию Карри–Ховарда типизированное выражение, тип которого соответствует логической формуле, аналогично доказательству этой формулы. Вот примеры.

Комбинатор идентичности рассматривается как доказательствоα→αв логике Гильберта

В качестве примера рассмотрим доказательство теоремы α → α . В лямбда-исчислении это тип функции тождества I = λ x . x , а в комбинаторной логике функция тождества получается путем применения S = λ fgx . fx ( gx ) дважды к K = λ xy . x . То есть, I = (( S K ) K ) . В качестве описания доказательства это говорит о том, что для доказательства α → α можно использовать следующие шаги :

• реализуем вторую схему аксиом с формулами α , β → α и α , чтобы получить доказательство ( α → (( β → α ) → α )) → (( α → ( β → α )) → ( α → α ) ) ,
• реализуем первую схему аксиом один раз с α и β → α, чтобы получить доказательство α → (( β → α ) → α ) ,
• реализуем первую схему аксиом второй раз с α и β, чтобы получить доказательство α → ( β → α ) ,
• примените modus ponens дважды, чтобы получить доказательство α → α

В целом процедура заключается в том, что всякий раз, когда программа содержит приложение формы ( P Q ), необходимо выполнить следующие шаги:

1. Сначала докажите теоремы , соответствующие типам P и Q.
2. Поскольку P применяется к Q , тип P должен иметь форму α → β , а тип Q должен иметь форму α для некоторых α и β . Следовательно, можно отделить заключение β с помощью правила modus ponens.

Композиционный комбинатор рассматривается как доказательство (β→α) → (γ→β) →γ→αв логике Гильберта

В качестве более сложного примера рассмотрим теорему, соответствующую функции B. Тип B — ( β → α ) → ( γ → β ) → γ → α . B эквивалентно ( S ( K S ) K ). Это наша дорожная карта для доказательства теоремы ( β → α ) → ( γ → β ) → γ → α .

Первый шаг — построить ( K S ). Чтобы сделать антецедент аксиомы K похожим на аксиому S , положим α равным ( α → β → γ ) → ( α → β ) → α → γ , а β равным δ (чтобы избежать столкновений переменных):

К  : α → β → α

K [ α знак равно ( α → β → γ ) → ( α → β ) → α → γ , β знак равно δ] : (( α → β → γ ) → ( α → β ) → α → γ ) → δ → ( α → β → γ ) → ( α → β ) → α → γ

Поскольку антецедент здесь — просто S , консеквент можно отделить с помощью Modus Ponens:

KS  : δ → ( α → β → γ ) → ( α → β ) → α → γ

Это теорема, которая соответствует типу ( K S ). Теперь применим S к этому выражению. Взяв S следующим образом

S  : ( α → β → γ ) → ( α → β ) → α → γ ,

положим α = δ , β = α → β → γ и γ = ( α → β ) → α → γ , что даст

S [ α знак равно δ , β знак равно α → β → γ , γ знак равно ( α → β ) → α → γ ] : ( δ → ( α → β → γ ) → ( α → β ) → α → γ ) → ( δ → ( α → β → γ )) → δ → ( α → β ) → α → γ

и затем отделить следствие:

S (KS)  : ( δ → α → β → γ ) → δ → ( α → β ) → α → γ

Это формула для типа ( S ( K S )). Частный случай этой теоремы имеет δ = ( β → γ ) :

S (KS) [ δ знак равно β → γ ] : (( β → γ ) → α → β → γ ) → ( β → γ ) → ( α → β ) → α → γ

Эту последнюю формулу необходимо применить к K. Специализируем K снова, на этот раз заменив α на ( β → γ ) и β на α :

К  : α → β → α

K [ α знак равно β → γ , β знак равно α ] : ( β → γ ) → α → ( β → γ )

Это то же самое, что и антецедент предыдущей формулы, поэтому, отсоединяя консеквент:

S (KS) K  : ( β → γ ) → ( α → β ) → α → γ

Поменяв местами имена переменных α и γ, мы получаем

( β → α ) → ( γ → β ) → γ → α

что и оставалось доказать.

Нормальное доказательство (β→α) → (γ→β) →γ→αв естественной дедукции рассматривается как λ-терм

Диаграмма ниже дает доказательство ( β → α ) → ( γ → β ) → γ → α естественным выводом и показывает, как его можно интерпретировать как λ-выражение λ a .λ b .λ g .( a ( b g )) типа ( β → α ) → ( γ → β ) → γ → α .

 a:β → α, b:γ → β, g:γ ⊢ b : γ → β a:β → α, b:γ → β, g:γ ⊢ g : γ—————————————————————————————————————————————————— ————————————————————————————————————————————————— ———a:β → α, b:γ → β, g:γ ⊢ a: β → α a:β → α, b:γ → β, g:γ ⊢ bg : β————————————————————————————————————————————————— —————————————————————— a:β → α, b:γ → β, g:γ ⊢ a (bg) : α ———————————————————————————————————— a:β → α, b:γ → β ⊢ λ g. а (бг) : γ → α ———————————————————————————————————————— а:β → α ⊢ λ б. λ г. а (бг) : (γ → β) → γ → α ———————————————————————————————————— ⊢ λ а. λ б. λ г. a (bg) : (β → α) → (γ → β) → γ → α

Другие приложения

Недавно изоморфизм был предложен как способ определения разбиения пространства поиска в генетическом программировании . ^[13] Метод индексирует наборы генотипов (деревья программ, созданные системой GP) с помощью их изоморфного доказательства Карри-Ховарда (называемого видом).

Как отметил директор по исследованиям INRIA Бернард Ланг, ^[14] переписка Карри-Ховарда представляет собой аргумент против патентоспособности программного обеспечения: поскольку алгоритмы являются математическими доказательствами, патентоспособность первых подразумевала бы патентоспособность вторых. Теорема может быть частной собственностью; математик должен был бы платить за ее использование и доверять компании, которая ее продает, но держит свое доказательство в секрете и отказывается от ответственности за любые ошибки.

Обобщения

Перечисленные здесь соответствия идут гораздо дальше и глубже. Например, декартовы замкнутые категории обобщаются замкнутыми моноидальными категориями . Внутренний язык этих категорий — это линейная система типов (соответствующая линейной логике ), которая обобщает просто типизированное лямбда-исчисление как внутренний язык декартовых замкнутых категорий. Более того, можно показать, что они соответствуют кобордизмам , ^[15] которые играют важную роль в теории струн .

Расширенный набор эквивалентностей также исследуется в теории гомотопических типов . Здесь теория типов расширяется аксиомой унивалентности («эквивалентность эквивалентна равенству»), которая позволяет использовать теорию гомотопических типов в качестве основы для всей математики (включая теорию множеств и классическую логику, предоставляя новые способы обсуждения аксиомы выбора и многого другого). То есть, соответствие Карри–Ховарда, что доказательства являются элементами обитаемых типов, обобщается до понятия гомотопической эквивалентности доказательств (как путей в пространстве, причем тип тождества или тип равенства теории типов интерпретируется как путь). ^[16]

Ссылки

1. Соответствие было впервые явно указано в Howard 1980. См., например, раздел 4.6, стр. 53 Gert Smolka и Jan Schwinghammer (2007-8), Lecture Notes in Semantics
2. Интерпретация Брауэра–Гейтинга–Колмогорова также называется «интерпретацией доказательства»: стр. 161 из Juliette Kennedy, Roman Kossak, eds. 2011. Теория множеств, арифметика и основы математики: теоремы, философии ISBN  978-1-107-00804-5
3. Касадио, Клаудия; Скотт, Филип Дж. (2021). Иоахим Ламбек: Взаимодействие математики, логики и лингвистики. Springer. стр. 184. ISBN 978-3-030-66545-6.
4. Коек, Боб; Киссинджер, Алекс (2017). Изображение квантовых процессов. Cambridge University Press. стр. 82. ISBN 978-1-107-10422-8.
5. "Вычислительная трилогия". nLab . Получено 29 октября 2023 г.
6. Карри 1934.
7. Карри и Фейс 1958.
8. Говард 1980.
9. Moggi, Eugenio (1991), «Понятия вычисления и монады» (PDF) , Информация и вычисления , 93 (1): 55–92, doi : 10.1016/0890-5401(91)90052-4
10. Сёренсон, Мортен; Ужичин, Павел (1998), Лекции об изоморфизме Карри-Ховарда , CiteSeerX 10.1.1.17.7385 
11. Голдблатт, «7.6 Топология Гротендика как интуиционистская модальность» (PDF) , Математическая модальная логика: модель ее эволюции , стр. 76–81. Упомянутая «слабая» модальность взята из Benton; Bierman; de Paiva (1998), «Вычислительные типы с логической точки зрения», Journal of Functional Programming , 8 (2): 177–193, CiteSeerX 10.1.1.258.6004 , doi :10.1017/s0956796898002998, S2CID  6149614 
12. Ламбек, Иоахим; Скотт, П.Дж. (1989). Введение в категориальную логику высшего порядка . Кембридж, Нью-Йорк, Порт-Честер [и т.д.]: Издательство Кембриджского университета. ISBN 0521356539.
13. Ф. Бинард и А. Фелти, «Генетическое программирование с полиморфными типами и функциями высшего порядка». В трудах 10-й ежегодной конференции по генетическим и эволюционным вычислениям, страницы 1187–1194, 2008.[1]
14. "Статья". bat8.inria.fr . Архивировано из оригинала 2013-11-17 . Получено 2020-01-31 .
15. Джон С. Баез и Майк Стэй, «Физика, топология, логика и вычисления: Розеттский камень», (2009) ArXiv 0903.0340 в New Structures for Physics , под ред. Боба Коке, Lecture Notes in Physics , т. 813 , Springer, Берлин, 2011, стр. 95–174.
16. Теория гомотопических типов: унифицированные основания математики. (2013) Программа унифицированных оснований. Институт перспективных исследований .

Основополагающие ссылки

• Карри, Х. Б. (1934-09-20). «Функциональность в комбинаторной логике». Труды Национальной академии наук Соединенных Штатов Америки . 20 (11): 584–90. Bibcode :1934PNAS...20..584C. doi : 10.1073/pnas.20.11.584 . ISSN  0027-8424. PMC  1076489 . PMID  16577644.
• Curry, Haskell B; Feys, Robert (1958). Craig, William (ред.). Комбинаторная логика . Исследования по логике и основаниям математики. Том 1. North-Holland Publishing Company. LCCN  a59001593; с двумя разделами Craig, William; см. параграф 9E{{cite book}}: CS1 maint: postscript (link)
• Де Брейн, Николас (1968), Automath, язык для математики , Кафедра математики, Технический университет Эйндховена, TH-report 68-WSK-05. Перепечатано в исправленном виде с двухстраничным комментарием в: Automation and Reasoning, т. 2, Классические статьи по вычислительной логике 1967–1970 , Springer Verlag, 1983, стр. 159–200.
• Howard, William A. (сентябрь 1980 г.) [оригинальная рукопись статьи от 1969 г.], «Понятие формул как типов в конструкции» (PDF) , в Seldin, Jonathan P.; Hindley, J. Roger (ред.), To HB Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism , Academic Press , стр. 479–490, ISBN 978-0-12-349050-6.

Продление переписки

1. Pfenning, Frank; Davies, Rowan (2001), "A Judgmental Reconstruction of Modal Logic" (PDF) , Математические структуры в информатике , 11 (4): 511–540, CiteSeerX 10.1.1.43.1611 , doi :10.1017/S0960129501003322, S2CID  16467268 
2. Дэвис, Роуэн; Пфеннинг, Франк (2001), «Модальный анализ поэтапных вычислений» (PDF) , Журнал ACM , 48 (3): 555–604, CiteSeerX 10.1.1.3.5442 , doi :10.1145/382780.382785, S2CID  52148006 

• Гриффин, Тимоти Г. (1990), «Понятие управления как формул», Отчет конференции 17-го ежегодного симпозиума ACM по принципам языков программирования, POPL '90, Сан-Франциско, Калифорния, США, 17–19 января 1990 г. , стр. 47–57, doi :10.1145/96709.96714, ISBN 978-0-89791-343-0, S2CID  3005134.
• Париго, Мишель (1992), «Лямбда-мю-исчисление: алгоритмическая интерпретация классического естественного вывода», Международная конференция по логическому программированию и автоматизированному рассуждению: Труды LPAR '92, Санкт-Петербург, Россия , Lecture Notes in Computer Science, т. 624, Springer-Verlag , стр. 190–201, ISBN 978-3-540-55727-2.
• Herbelin, Hugo (1995), "Структура лямбда-исчисления, изоморфная структуре секвенциального исчисления в стиле Генцена", в Pacholski, Leszek; Tiuryn, Jerzy (ред.), Computer Science Logic, 8th International Workshop, CSL '94, Kazimierz, Poland, September 25–30, 1994, Selected Papers , Lecture Notes in Computer Science, vol. 933, Springer-Verlag , pp. 61–75, ISBN 978-3-540-60017-6.
• Габбай, Дов; де Кейрос, Руй (1992). «Расширение интерпретации Карри–Ховарда на линейную, релевантную и другие ресурсные логики». Журнал символической логики . Том 57. Ассоциация символической логики. С. 1319–1365. doi :10.2307/2275370. JSTOR  2275370. S2CID  7159005.. (Полная версия статьи, представленной на Logic Colloquium '90 , Хельсинки. Аннотация в JSL 56(3):1139–1140, 1991.)
• де Кейрос, Руй; Габбай, Дов (1994), «Равенство в маркированных дедуктивных системах и функциональная интерпретация пропозиционального равенства», в Деккер, Пол; Стохоф, Мартин (ред.), Труды Девятого Амстердамского коллоквиума , ILLC/Философский факультет, Амстердамский университет, стр. 547–565, ISBN 978-90-74795-07-4.
• де Кейрос, Рюй; Габбай, Дов (1995), «Функциональная интерпретация квантификатора существования», Бюллетень Группы по интересам в области чистой и прикладной логики , т. 3, стр. 243–290. (Полная версия статьи, представленной на Logic Colloquium '91 , Уппсала. Аннотация в JSL 58(2):753–754, 1993.)
• де Кейрос, Руй; Габбай, Дов (1997), «Функциональная интерпретация модальной необходимости», в де Рийке, Маартен (ред.), Достижения в интенсиональной логике , Серия прикладной логики, т. 7, Springer-Verlag , стр. 61–91, ISBN 978-0-7923-4711-8.
• de Queiroz, Ruy; Gabbay, Dov (1999), "Labelled Natural Deduction", в Ohlbach, Hans-Juergen; Reyle, Uwe (ред.), Logic, Language and Reasoning. Эссе в честь Дова Габбея , Trends in Logic, т. 7, Kluwer, стр. 173–250, ISBN 978-0-7923-5687-5.
• де Оливейра, Аньолина; де Кейрос, Руй (1999), «Процедура нормализации для эквационального фрагмента маркированного естественного вывода», Logic Journal of the Interest Group in Pure and Applied Logics , т. 7, Oxford University Press , стр. 173–215. (Полная версия статьи, представленной на 2-й конференции WoLLIC'95 , Ресифи. Аннотация в журнале Journal of the Interest Group in Pure and Applied Logics 4(2):330–332, 1996.)
• Poernomo, Iman; Crossley, John; Wirsing; Martin (2005), Адаптация доказательств как программ: протокол Карри–Ховарда , Монографии по информатике, Springer , ISBN 978-0-387-23759-6, касается адаптации синтеза программ proofs-as-programs к проблемам разработки программ с грубым зерном и императивными методами с помощью метода, который авторы называют протоколом Карри–Ховарда. Включает обсуждение соответствия Карри–Ховарда с точки зрения компьютерной науки.
• de Queiroz, Ruy JGB; de Oliveira, Anjolina (2011), «Функциональная интерпретация прямых вычислений», Electronic Notes in Theoretical Computer Science , 269 , Elsevier : 19–40, doi : 10.1016/j.entcs.2011.03.003. (Полная версия доклада, представленного на LSFA 2010 , Натал, Бразилия.)

Философские интерпретации

• де Кейрос, Руй Ж.Б.Б. (1994), «Нормализация и языковые игры», Dialectica , 48 (2): 83–123, doi :10.1111/j.1746-8361.1994.tb00107.x, JSTOR  42968904. (Ранняя версия, представленная на Logic Colloquium '88 , Падуя. Аннотация в JSL 55:425, 1990.)
• de Queiroz, Ruy JGB (2001), «Значение, функция, цель, полезность, последствия – взаимосвязанные концепции», Logic Journal of the Interest Group in Pure and Applied Logics , т. 9, стр. 693–734. (Ранняя версия, представленная на Четырнадцатом международном симпозиуме имени Витгенштейна (празднование столетия), состоявшемся в Кирхберге/Векселе, 13–20 августа 1989 г.)
• де Кейрос, Руй Ж. Г. Б. (2008), «О правилах редукции, значении как использовании и семантике теории доказательств», Studia Logica , 90 (2): 211–247, doi :10.1007/s11225-008-9150-5, S2CID  11321602.

Синтетическая бумага

• Де Брёйн, Николаас Говерт (1995), «О роли типов в математике» (PDF) , в Groote, Филипп де (ред.), De Groote 1995, стр. 27–54., вклад самого де Брейна.
• Гейверс, Герман (1995), «Исчисление конструкций и логика высшего порядка», De Groote 1995, стр. 139–191, содержит синтетическое введение в соответствие Карри–Ховарда.
• Галлье, Жан Х. (1995), «О соответствии между доказательствами и лямбда-термами» (PDF) , De Groote 1995, стр. 55–138 , архивировано из оригинала (PDF) 5 июля 2017 г., содержит синтетическое введение в соответствие Карри–Ховарда.
• Вадлер, Филип (2014), «Предложения как типы» (PDF) , Сообщения ACM , 58 (12): 75–84, doi :10.1145/2699407, S2CID  11957500

Книги

• Де Гроот, Филипп, изд. (1995), Изоморфизм Карри-Ховарда , Cahiers du Centre de Logique (Католический университет Лувена), vol. 8, Академия-Брюян, ISBN 978-2-87209-363-2, воспроизводит основополагающие статьи Карри-Фейса и Ховарда, статью де Брейна и несколько других статей.
• Sørensen, Morten Heine; Urzyczyn, Paweł (2006) [1998], Lectures on the Curry–Howard isomorphism , Studies in Logic and the Foundations of Mathematics, т. 149, Elsevier Science , CiteSeerX  10.1.1.17.7385 , ISBN 978-0-444-52077-7, заметки по теории доказательств и теории типов, которые включают представление соответствия Карри–Ховарда с акцентом на соответствие формул как типов
• Жирар, Жан-Ив (1987–1990), Доказательство и типы, Cambridge Tracts in Theoretical Computer Science, т. 7, Перевод и приложения Лафонта, Ива и Тейлора, Пола, Cambridge University Press, ISBN 0-521-37181-3, архивировано из оригинала 2008-04-18, заметки по теории доказательств с презентацией соответствия Карри–Ховарда.
• Томпсон, Саймон (1991), Теория типов и функциональное программирование, Addison–Wesley, ISBN 0-201-41667-0.
• Poernomo, Iman; Crossley, John; Wirsing; Martin (2005), Адаптация доказательств как программ: протокол Карри–Ховарда , Монографии по информатике, Springer , ISBN 978-0-387-23759-6, касается адаптации синтеза программ proofs-as-programs к проблемам разработки программ с грубым зерном и императивными методами с помощью метода, который авторы называют протоколом Карри–Ховарда. Включает обсуждение соответствия Карри–Ховарда с точки зрения компьютерной науки.
• Бинард, Ф.; Фелти, А. (2008), «Генетическое программирование с полиморфными типами и функциями высшего порядка» (PDF) , Труды 10-й ежегодной конференции по генетическим и эволюционным вычислениям , Ассоциация вычислительной техники, стр. 1187–94, doi :10.1145/1389095.1389330, ISBN 9781605581309, S2CID  3669630
• де Кейрос, Руй Дж. ГБ.; де Оливейра, Аньолина Г.; Габбай, Дов М. (2011), Функциональная интерпретация логической дедукции, Advances in Logic, т. 5, Imperial College Press/World Scientific, ISBN 978-981-4360-95-1.

Дальнейшее чтение

• Джонстон, ПТ (2002), «D4.2 λ-исчисление и декартовы замкнутые категории», Sketches of an Elephant, A Topos Theory Compendium, т. 2, Clarendon Press, стр. 951–962, ISBN 978-0-19-851598-2— дает категорический взгляд на то, «что происходит» в переписке Карри–Ховарда.

Внешние ссылки

• Говард о Карри-Говарде
• Соответствие Карри-Говарда в Haskell
• Монада Хрестоматия 6: Приключения в Классической Стране: Карри–Ховард в Хаскелле, Закон Пирса.