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

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

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

Это обобщение синтаксической аналогии между системами формальной логики и вычислительными исчислениями, которая была впервые открыта американским математиком Хаскеллом Карри и логиком Уильямом Элвином Ховардом . ^[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 . Икс и λ Икс .λ y . y типа α → α → α не будет выделяться в переписке. Примеры приведены ниже.

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

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

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

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

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

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

Секвенционное исчисление

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

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

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

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

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

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

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

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

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

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

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

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

Иоахим Ламбек показал в начале 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 такое, что iff доказуемо в импликативной интуиционистской логике. ${\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 . Икс . То есть я = (( S K ) K ) . В качестве описания доказательства говорится, что для доказательства α → α можно использовать следующие шаги :

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

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

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

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

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

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

К  : α → β → α

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

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

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

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

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

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

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

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

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

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

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) : (β → α) → (γ → β) → γ → α

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

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

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

Обобщения

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

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

Рекомендации

1. Впервые переписка была явно выражена Ховардом в 1980 году. См., например, раздел 4.6, стр. 53 Герт Смолка и Ян Швинхаммер (2007-8), Конспекты лекций по семантике.
2. Интерпретацию Брауэра-Хейтинга-Колмогорова также называют «интерпретацией доказательства»: с. 161 Джульетты Кеннеди, Роман Коссак, ред. 2011. Теория множеств, арифметика и основы математики: теоремы, философия ISBN  978-1-107-00804-5.
3. Касадио, Клаудия; Скотт, Филип Дж. (2021). Иоахим Ламбек: Взаимодействие математики, логики и лингвистики. Спрингер. п. 184. ИСБН 978-3-030-66545-6.
4. Куке, Боб; Киссинджер, Алекс (2017). Изображение квантовых процессов. Издательство Кембриджского университета. п. 82. ИСБН 978-1-107-10422-8.
5. "Вычислительная трилогия". нЛаб . Проверено 29 октября 2023 г.
6. Карри 1934.
7. Карри и Фейс 1958.
8. Ховард 1980.
9. Моджи, Эухенио (1991), «Понятия вычислений и монад» (PDF) , Information and Computation , 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. Упомянутая «слабая» модальность принадлежит Бентону; Бирман; де Пайва (1998), «Вычислительные типы с логической точки зрения», Журнал функционального программирования , 8 (2): 177–193, CiteSeerX 10.1.1.258.6004 , doi : 10.1017/s0956796898002998, S2CID  6149614 
12. Ф. Бинар и А. Фелти, «Генетическое программирование с полиморфными типами и функциями высшего порядка». В материалах 10-й ежегодной конференции по генетическим и эволюционным вычислениям, страницы 1187–1194, 2008 г. [1]
13. «Статья». bat8.inria.fr . Архивировано из оригинала 17 ноября 2013 г. Проверено 31 января 2020 г.
14. Джон ок. Баэз и Майк Стей, «Физика, топология, логика и вычисления: Розеттский камень», (2009) ArXiv 0903.0340 в « Новых структурах для физики» , изд. Боб Коке, Конспекты лекций по физике, том. 813 , Springer, Берлин, 2011, стр. 95–174.
15. "Теория гомотопических типов - Google Trends" . Trends.google.com . Проверено 26 января 2018 г.^{[ постоянная мертвая ссылка ]}
16. Теория гомотопических типов: одновалентные основы математики. (2013) Программа Uniвалентных фондов. Институт перспективных исследований .

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

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

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

1. Пфеннинг, Фрэнк; Дэвис, Роуэн (2001), «Осмысленная реконструкция модальной логики» (PDF) , Математические структуры в информатике , 11 (4): 511–540, CiteSeerX 10.1.1.43.1611 , doi : 10.1017/S0960129501003322, S2CID  1646726 8 
2. Дэвис, Роуэн; Пфеннинг, Франк (2001), «Модальный анализ поэтапных вычислений» (PDF) , Journal of the ACM , 48 (3): 555–604, CiteSeerX 10.1.1.3.5442 , doi : 10.1145/382780.382785, S2CID  52148006 

• Гриффин, Тимоти Г. (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. S2CID  7159005.. (Полная версия статьи представлена ​​на коллоквиуме Logic '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.
• де Кейрос, Руи; Габбай, Дов (1999), «Маркированная естественная дедукция», в Ольбахе, Ханс-Юрген; Рейл, Уве (ред.), Логика, язык и рассуждение. Очерки в честь Дова Габая , Тенденции в логике, т. 7, Клювер, стр. 173–250, ISBN. 978-0-7923-5687-5.
• де Оливейра, Анжолина; де Кейроз, Рюи (1999), "Процедура нормализации для фрагмента уравнения помеченной естественной дедукции", Логический журнал группы по интересам в области чистой и прикладной логики , том. 7, Oxford University Press , стр. 173–215.. (Полная версия статьи, представленной на 2-м WoLLIC'95 , Ресифи. Аннотация в журнале группы по интересам в области Pure and Applied Logics 4(2):330–332, 1996.)
• Поэрномо, Иман; Кроссли, Джон; Вирсинг; Мартин (2005), Адаптация доказательств как программ: протокол Карри-Ховарда , Монографии по информатике, Springer , ISBN 978-0-387-23759-6, касается адаптации синтеза программ «доказательства как программы» к крупнозернистым и императивным задачам разработки программ с помощью метода, который авторы называют протоколом Карри-Ховарда. Включает обсуждение переписки Карри-Ховарда с точки зрения информатики.
• де Кейрос, Руи ЖГБ; де Оливейра, Анджолина (2011), «Функциональная интерпретация прямых вычислений», Электронные заметки по теоретической информатике , 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), «Значение, функция, цель, полезность, последствия - взаимосвязанные концепции», Логический журнал группы по интересам в области чистой и прикладной логики , том. 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., содержит синтетическое введение в переписку Карри – Ховарда.
• Уодлер, Филип (2014), «Предложения как типы» (PDF) , Communications of the 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, воспроизводит основополагающие статьи Карри-Фейса и Ховарда, статью де Брейна и несколько других статей.
• Соренсен, Мортен Хейне; Уржичин, Павел (2006) [1998], Лекции по изоморфизму Карри – Ховарда , Исследования по логике и основам математики, том. 149, Elsevier Science , CiteSeerX  10.1.1.17.7385 , ISBN 978-0-444-52077-7, заметки по теории доказательств и теории типов, которые включают представление соответствия Карри – Ховарда с упором на соответствие формул как типов.
• Жирар, Жан-Ив (1987–1990), Доказательства и типы, Кембриджские трактаты по теоретической информатике, том. 7, Перевод и с приложениями Лафона, Ива и Тейлора, Пола, Cambridge University Press, 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, издательство Имперского колледжа/World Scientific, ISBN 978-981-4360-95-1.

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

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

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

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