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

Доказательство, написанное в виде функциональной программы
plus_comm = fun n m : nat => nat_ind ( fun n0 : nat => n0 + m = m + n0 ) ( plus_n_0 m ) ( fun ( y : nat ) ( H : y + m = m + y ) => eq_ind ( S ( m + y )) ( весело n0 : nat => S ( y + m ) = n0 ) ( f_equal S H ) ( m + S y ) ( plus_n_Sm m y )) n : forall n m : nat , n + m = m + n
Доказательство коммутативности сложения натуральных чисел в помощнике по доказательству Coq . nat_indозначает математическую индукцию , eq_indзамену равенства и f_equalвзятие одной и той же функции с обеих сторон равенства. Ссылки на более ранние теоремы показывают и .${\ Displaystyle м = м + 0}$${\ Displaystyle S (м + у) = м + Sy}$

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

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

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

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

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

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

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

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

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

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

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

Можно предположить, что соответствие Карри-Ховарда приведет к существенному объединению математической логики и фундаментальной компьютерной науки:

Логика в стиле Гильберта и естественная дедукция — всего лишь два вида систем доказательства в большом семействе формализмов. Альтернативные синтаксисы включают исчисление секвенций , сети доказательств , исчисление структур и т. д . Если принять соответствие Карри-Ховарда как общий принцип, согласно которому любая система доказательств скрывает модель вычислений, теорию лежащей в основе нетипизированной вычислительной структуры этих видов доказательств. система должна быть возможной. Тогда возникает естественный вопрос: можно ли сказать что-нибудь математически интересное об этих лежащих в основе вычислительных исчислениях.

И наоборот, комбинаторная логика и просто типизированное лямбда-исчисление — не единственные модели вычислений . Линейная логика Жирара была разработана на основе тонкого анализа использования ресурсов в некоторых моделях лямбда-исчисления; существует ли типизированная версия машины Тьюринга, которая будет вести себя как система доказательств? Типизированные языки ассемблера являются таким экземпляром «низкоуровневых» моделей вычислений, которые несут типы.

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

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

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

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

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

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

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

Системы вывода в стиле Гильберта и комбинаторная логика

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

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

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

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

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

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

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

Интуиционистская импликационная логика в стиле Гильберта	Просто типизированная комбинаторная логика
${\ displaystyle {\ frac {\ alpha \ in \ Gamma} {\ Gamma \ vdash \ alpha}} \ qquad \ qquad {\ text {Assum}}}$	${\ displaystyle {\ frac {x: \ alpha \ in \ Gamma} {\ Gamma \ vdash x: \ alpha}}}$
${\displaystyle {\frac {}{\Gamma \vdash \alpha \rightarrow (\beta \rightarrow \alpha )}}\qquad {\text{Ax}}_{K}}$	${\displaystyle {\frac {}{\Gamma \vdash K:\alpha \rightarrow (\beta \rightarrow \alpha )}}}$
${\displaystyle {\frac {}{\Gamma \vdash (\alpha \!\rightarrow \!(\beta \!\rightarrow \!\gamma ))\!\rightarrow \!((\alpha \!\rightarrow \!\beta )\!\rightarrow \!(\alpha \!\rightarrow \!\gamma ))}}\;{\text{Ax}}_{S}}$	${\displaystyle {\frac {}{\Gamma \vdash S:(\alpha \!\rightarrow \!(\beta \!\rightarrow \!\gamma ))\!\rightarrow \!((\alpha \!\rightarrow \!\beta )\!\rightarrow \!(\alpha \!\rightarrow \!\gamma ))}}}$
${\displaystyle {\frac {\Gamma \vdash \alpha \rightarrow \beta \qquad \Gamma \vdash \alpha }{\Gamma \vdash \beta }}\quad {\text{Modus Ponens}}}$	${\displaystyle {\frac {\Gamma \vdash E_{1}:\alpha \rightarrow \beta \qquad \Gamma \vdash E_{2}:\alpha }{\Gamma \vdash E_{1}\;E_{2}:\beta }}}$

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

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

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

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

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

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

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

α → ( β → α ) и

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

Естественная дедукция и лямбда-исчисление

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

Интуиционистская импликация естественная дедукция	Правила назначения типа лямбда-исчисления
${\displaystyle {\frac {}{\Gamma _{1},\alpha ,\Gamma _{2}\vdash \alpha }}{\text{Ax}}}$	${\displaystyle {\frac {}{\Gamma _{1},x:\alpha ,\Gamma _{2}\vdash x:\alpha }}}$
${\displaystyle {\frac {\Gamma ,\alpha \vdash \beta }{\Gamma \vdash \alpha \rightarrow \beta }}\rightarrow I}$	${\displaystyle {\frac {\Gamma ,x:\alpha \vdash t:\beta }{\Gamma \vdash (\lambda x\!:\!\alpha .~t):\alpha \rightarrow \beta }}}$
${\displaystyle {\frac {\Gamma \vdash \alpha \rightarrow \beta \qquad \Gamma \vdash \alpha }{\Gamma \vdash \beta }}\rightarrow E}$	${\displaystyle {\frac {\Gamma \vdash t:\alpha \rightarrow \beta \qquad \Gamma \vdash u:\alpha }{\Gamma \vdash t\;u:\beta }}}$

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

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

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

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

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

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

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

секвенциальное исчисление

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

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

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

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

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

интерпретация БХК

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

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

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

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

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

Переписка Карри – Ховарда – Ламбека

Иоахим Ламбек показал в начале 1970-х годов, что доказательства интуиционистской логики высказываний и комбинаторы типизированной комбинаторной логики имеют общую эквациональную теорию, которая является теорией декартовых замкнутых категорий .. Выражение соответствия Карри-Ховарда-Ламбека теперь используется некоторыми людьми для обозначения трехстороннего изоморфизма между интуиционистской логикой, типизированным лямбда-исчислением и декартовскими замкнутыми категориями, при этом объекты интерпретируются как типы или предложения, а морфизмы - как термины или доказательства. Соответствие работает на эквациональном уровне и не является выражением синтаксической идентичности структур, как это имеет место для каждого из соответствий Карри и Ховарда: т. е. структура четко определенного морфизма в декартово-замкнутой категории не сравнима с структура доказательства соответствующего суждения либо в логике в стиле Гильберта, либо в естественной дедукции. Чтобы прояснить это различие, основная синтаксическая структура картезианских закрытых категорий перефразируется ниже.

Объекты (типы) определяются

• ${\displaystyle \top }$является объектом
• если α и β — объекты, то и — объекты.${\displaystyle \alpha \times \beta }$${\displaystyle \alpha \rightarrow \beta }$

Морфизмы (термы) определяются

• ${\displaystyle id}$, , , и являются морфизмами${\displaystyle \star }$${\displaystyle \operatorname {eval} }$${\displaystyle \pi _{1}}$${\displaystyle \pi _{2}}$
• если t — морфизм, λ t — морфизм
• если t и u — морфизмы, и — морфизмы.${\displaystyle (t,u)}$${\displaystyle u\circ t}$

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

Личность:

${\displaystyle {\frac {}{id:\!\!-~~\alpha ~\vdash ~\alpha }}}$

Сочинение:

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

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

${\displaystyle {\frac {}{\star :\!\!-~~\alpha ~\vdash ~\top }}}$

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

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

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

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

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

${\displaystyle {\frac {t:\!\!-~~\alpha \times \beta ~\vdash ~\gamma }{\lambda t:\!\!-~~\alpha ~\vdash ~\beta \rightarrow \gamma }}}$

Применение :

${\displaystyle {\frac {}{eval:\!\!-~~(\alpha \rightarrow \beta )\times \alpha ~\vdash ~\beta }}}$

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

• ${\displaystyle id\circ t=t}$
• ${\displaystyle t\circ id=t}$
• ${\displaystyle (v\circ u)\circ t=v\circ (u\circ t)}$
• ${\displaystyle \star =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 eval\circ (\lambda t\circ \pi _{1},\pi _{2})=t}$
• ${\displaystyle \lambda eval=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 (eval\circ (t\circ \pi _{1},\pi _{2}))=t}$

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

Примеры

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

Комбинатор тождеств, рассматриваемый как доказательство α → α в логике в стиле Гильберта

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

КС  : δ → ( α → β → γ ) → ( α → β ) → α → γ

Это теорема, которая соответствует типу ( 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) : (γ → β) -> γ → α ——————————————————————————————————— ⊢ λ а. λ б. λ г. a (bg) : (β → α) -> (γ → β) -> γ → α

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

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

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

Обобщения

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

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

использованная литература

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

Основные ссылки

• Карри, HB (1934-09-20). «Функциональность в комбинаторной логике» . Труды Национальной академии наук Соединенных Штатов Америки . 20 (11): 584–90. Бибкод : 1934PNAS...20..584C . doi : 10.1073/pnas.20.11.584 . ISSN  0027-8424 . ПМС  1076489 . PMID  16577644 .
• Карри, Хаскелл Б.; Фейс, Роберт (1958). Крейг, Уильям (ред.). Комбинаторная логика . Исследования по логике и основам математики. Том. 1. Издательство Северной Голландии. LCCN  a59001593 ; с двумя разделами Крейга, Уильяма; см. пункт 9Е{{cite book}}: CS1 maint: постскриптум ( ссылка )
• Де Брюйн, Николаас (1968), Автоматика, язык для математики , Математический факультет Эйндховенского технологического университета, отчет TH 68-WSK-05. Перепечатано в исправленном виде с комментариями на двух страницах в: Автоматизация и рассуждения, том 2, Классические статьи по вычислительной логике 1967–1970 , Springer Verlag, 1983, стр. 159–200.
• Ховард, Уильям А. (сентябрь 1980 г.) [оригинальная бумажная рукопись 1969 г.], «Понятие построения формул как типов», у Селдина, Джонатана П .; Хиндли, Дж. Роджер (ред.), Х. Б. Карри: Очерки комбинаторной логики, лямбда-исчисления и формализма , Academic Press , стр. 479–490, ISBN 978-0-12-349050-6.

Расширения переписки

• Гриффин, Тимоти Г. (1990), «Понятие контроля в виде формул как типов», Conf. Рекордный 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, Санкт-Петербург, Россия , Конспект лекций по информатике, том . 624, Springer-Verlag , стр. 190–201, ISBN . 978-3-540-55727-2.
• Гербелин, Хьюго (1995), «Структура лямбда-исчисления, изоморфная структуре последовательного исчисления в стиле Генцена», в Пачольски, Лешек; Тюрин, Ежи (ред.), Логика компьютерных наук, 8-й международный семинар, CSL '94, Казимеж, Польша, 25–30 сентября 1994 г., Избранные статьи , Конспект лекций по информатике, том. 933, Springer-Verlag , стр. 61–75, ISBN . 978-3-540-60017-6.
• Габбай, Дов; де Кейрос, Рюи (1992). «Расширение интерпретации Карри – Ховарда на линейную, релевантную и другую логику ресурсов». Журнал символической логики . Журнал символической логики . Том. 57. стр. 1319–1365. дои : 10.2307/2275370 . JSTOR  2275370 .. (Полная версия статьи представлена ​​на Logic Colloquium '90 , Helsinki. Abstract in JSL 56(3):1139–1140, 1991.)
• де Кейроз, Рюи; Габбай, Дов (1994), «Равенство в размеченных дедуктивных системах и функциональная интерпретация пропозиционального равенства», Деккер, Пол; Стохоф, Мартин (ред.), Труды девятого Амстердамского коллоквиума , ILLC / факультет философии Амстердамского университета, стр. 547–565, ISBN 978-90-74795-07-4.
• де Кейроз, Рюи; Габбай, Дов (1995), «Функциональная интерпретация квантора существования» , Бюллетень исследовательской группы по чистой и прикладной логике , том. 3, стр. 243–290.. (Полная версия статьи, представленной на Logic Colloquium '91 , Uppsala. Abstract in JSL 58(2):753–754, 1993.)
• де Кейроз, Рюи; Габбай, Дов (1997), «Функциональная интерпретация модальной необходимости», в де Рийке, Маартен (ред.), « Достижения в области интенсиональной логики », серия «Прикладная логика», том. 7, Springer-Verlag , стр. 61–91, ISBN . 978-0-7923-4711-8.
• де Кейроз, Рюи; Габбай, Дов (1999), «Маркированная естественная дедукция» , в Ольбахе, Ханс-Юрген; Рейле, Уве (ред.), Логика, язык и мышление. Очерки в честь Дова Габая , Тенденции в логике, т. 1, с. 7, Клювер, стр. 173–250, ISBN . 978-0-7923-5687-5.
• де Оливейра, Анжолина; де Кейроз, Рюи (1999), «Процедура нормализации фрагмента уравнения помеченной естественной дедукции», Logic Journal of the Interest Group in Pure and Applied Logics , vol. 7, издательство Оксфордского университета , стр. 173–215.. (Полная версия статьи, представленной на 2nd WoLLIC'95 , Recife. Abstract in Journal of the Interest Group in Pure and Applied Logics 4(2):330–332, 1996.)
• Поерномо, Иман; Кроссли, Джон; проводка; Мартин (2005), Адаптация доказательств как программ: протокол Карри-Ховарда , Монографии по компьютерным наукам, Springer , ISBN 978-0-387-23759-6, касается адаптации синтеза программ «доказательства как программы» к грубым и императивным задачам разработки программ с помощью метода, который авторы называют протоколом Карри-Ховарда. Включает обсуждение переписки Карри-Ховарда с точки зрения информатики.
• де Кейроз, Рюи Ж.Г.Б.; де Оливейра, Анжолина (2011), «Функциональная интерпретация прямых вычислений», Electronic Notes in Theoretical Computer Science , Elsevier , 269 : 19–40, doi : 10.1016/j.entcs.2011.03.003. (Полная версия статьи, представленной на LSFA 2010 , Натал, Бразилия.)

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

• де Кейроз, Рюи ЖГБ (1994), «Нормализация и языковые игры» , Dialectica , vol. 48, стр. 83–123.. (Ранняя версия представлена ​​на Logic Colloquium '88 , Падуя. Резюме в JSL 55:425, 1990.)
• де Кейроз, Рюи ЖГБ (2001), «Значение, функция, цель, полезность, последствия - взаимосвязанные понятия» , Logic Journal of the Interest Group in Pure and Applied Logics , vol. 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), «Исчисление конструкций и логика высшего порядка», Де Гроот, 1995 , стр. 139–191., содержит синтетическое введение в переписку Карри-Ховарда.
• Галье, Жан Х. (1995), «О соответствии между доказательствами и лямбда-терминами» (PDF) , De Groote 1995 , стр. 55–138., содержит синтетическое введение в переписку Карри-Ховарда.
• Уодлер, Филип (2014), «Предложения как типы» (PDF) , Communications of the ACM , 58 (12): 75–84, doi : 10.1145/2699407 , S2CID  11957500

Книги

• Де Гроот, Филипп, изд. (1995), Изоморфизм Карри-Ховарда , Cahiers du Center de Logique (Католический университет Лувена), vol. 8, Академия-Брюйлант, ISBN 978-2-87209-363-2, воспроизводит основополагающие статьи Карри-Фейса и Ховарда, статью де Брейна и несколько других статей.
• Соренсен, Мортен Хайне; Ужичин, Павел (2006) [1998], Лекции по изоморфизму Карри – Ховарда , Исследования по логике и основам математики, том. 149, Elsevier Science , CiteSeerX  10.1.1.17.7385 , ISBN 978-0-444-52077-7, заметки по теории доказательств и теории типов, которые включают представление соответствия Карри – Ховарда с акцентом на соответствие формул как типов.
• Жирар, Жан-Ив (1987–1990), Доказательство и типы , Cambridge Tracts in Theoretical Computer Science, vol. 7, переведено Лафонтом, Ивом и Тейлором, Полом и с приложениями, издательство Кембриджского университета, ISBN 0-521-37181-3, заархивировано из оригинала 18 апреля 2008 г., заметки по теории доказательств с представлением соответствия Карри – Ховарда.
• Томпсон, Саймон (1991), Теория типов и функциональное программирование , Аддисон-Уэсли, ISBN 0-201-41667-0.
• Поерномо, Иман; Кроссли, Джон; проводка; Мартин (2005), Адаптация доказательств как программ: протокол Карри-Ховарда , Монографии по компьютерным наукам, Springer , ISBN 978-0-387-23759-6, касается адаптации синтеза программ «доказательства как программы» к грубым и императивным задачам разработки программ с помощью метода, который авторы называют протоколом Карри-Ховарда. Включает обсуждение переписки Карри-Ховарда с точки зрения информатики.
• Бинар, Ф.; Фелти, А. (2008), «Генетическое программирование с полиморфными типами и функциями высшего порядка» (PDF) , Труды 10-й ежегодной конференции по генетическим и эволюционным вычислениям , Ассоциация вычислительной техники, стр. 1187–94, doi : 10.1145 /1389095.1389330 , ISBN 9781605581309, S2CID  3669630
• де Кейроз, Рюи Ж.Г.Б.; де Оливейра, Анжолина Г.; Габбай, Дов М. (2011), Функциональная интерпретация логической дедукции , Достижения в области логики, том. 5, Imperial College Press/World Scientific, ISBN 978-981-4360-95-1.
• Мимрам, Самуэль (2020), Программа = доказательство , опубликовано независимо, ISBN 979-8615591839

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

• Джонстон, П.Т. (2002), «D4.2 λ-исчисление и декартовы закрытые категории», Очерки слона , Сборник по теории топосов, том. 2, Clarendon Press, стр. 951–962, ISBN . 978-0-19-851598-2- дает категорическое представление о том, «что происходит» в переписке Карри-Ховарда.

внешняя ссылка

В Wikibook Haskell есть страница на тему: Изоморфизм Карри – Ховарда.

• Ховард о Карри-Ховарде
• Переписка Карри-Ховарда в Haskell
• Читатель монад 6: Приключения в классической стране : Карри-Ховард в Хаскелле, закон Пирса.