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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Логическая сторона	Сторона программирования
формула	тип
доказательство	срок
формула верна	тип имеет элемент
формула неверна	тип не имеет элемента
логическая константа ⊤ (истина)	тип устройства
логическая константа ⊥ (ложь)	пустой тип
импликация	тип функции
соединение	тип продукта
дизъюнкция	тип суммы
универсальная количественная оценка	зависимый тип продукта
экзистенциальная квантификация	тип зависимой суммы

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

Логическая сторона	Сторона программирования
Система дедукции в стиле Гильберта	система типов для комбинаторной логики
естественный вычет	система типов для лямбда-исчисления

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

Логическая сторона	Сторона программирования
гипотезы	свободные переменные
последствий (modus ponensустранение	приложение
введение импликации	абстракция

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

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

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

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

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

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

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

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

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

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

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

Логическая сторона	Сторона программирования
предположение	переменная
схемы аксиом	комбинаторы
установка настроения	приложение
теорема о дедукции	устранение абстракции

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

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

(( а → б ) → а ) → а .

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

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

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

а → ( б → а ) и

( а → ( б → с )) → (( а → б ) → ( а → с )).

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

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

Интуиционистская импликационная естественная дедукция	Правила назначения типов лямбда-исчисления
${\frac {}{\Gamma _{1},\alpha ,\Gamma _{2}\vdash \alpha }}{\text{Ax}}$	${\frac {}{\Gamma _{1},x:\alpha ,\Gamma _{2}\vdash x:\alpha }}$
${\frac {\Gamma ,\alpha \vdash \beta }{\Gamma \vdash \alpha \rightarrow \beta }}\rightarrow I$	${\frac {\Gamma ,x:\alpha \vdash t:\beta }{\Gamma \vdash (\lambda x\!:\!\alpha .~t):\alpha \rightarrow \beta }}$
${\frac {\Gamma \vdash \alpha \rightarrow \beta \qquad \Gamma \vdash \alpha }{\Gamma \vdash \beta }}\rightarrow E$	${\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 _ω
• индуктивные типы как алгебраический тип данных
• необходимость $\Box$ в модальной логике и поэтапных вычислениях
• возможность $\Diamond$ в модальной логике и монадических типах эффектов
• Исчисление λ _I (где абстракция ограничена λx . E , где x имеет хотя бы одно свободное вхождение в E) и исчисление CL _I соответствуют соответствующей логике .
• Модальность локальной истины (∇) в топологии Гротендика или эквивалентная «слабая» модальность (◯) Бентона, Бирмана и де Пайвы (1998) соответствуют CL-логике, описывающей «типы вычислений».

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

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

Логическая сторона	Сторона программирования
Закон Пирса : (( a → b ) → a ) → a	вызов с текущим продолжением
перевод с двойным отрицанием	перевод в стиле продолжения-передачи

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

Далее следуют расчеты

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

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

Логическая сторона	Сторона программирования
исключение сокращения	сокращение в виде абстрактной машины
правильные правила знакомства	конструкторы кода
левые правила знакомства	конструкторы стеков оценок
приоритет правой стороны при исключении разреза	вызовов по имени сокращение количества
приоритет левой стороны при исключении разреза	количества звонков по ценности сокращение

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Личность:

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

Состав:

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

Тип устройства ( терминальный объект ):

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

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

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

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

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

Карри :

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

Приложение :

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

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

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

Эти уравнения подразумевают следующее $\eta$-законы:

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

Теперь существует t такое, что $t:\!\!-~\alpha _{1}\times \ldots \times \alpha _{n}\vdash \beta$ если только $\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 [ α знак равно ( α → β → γ ) → ( α → β ) → α → γ , β знак равно δ] : (( α → β → γ ) → ( α → β ) → α → γ ) → δ → ( а → б → c ) → ( а → б ) → а → c

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

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

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

S : ( а → б → с ) → ( а → б ) → а → с ,

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

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

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

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

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

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

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

К : а → б → а

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

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

S (KS) K : ( б → c ) → ( а → б ) → а → c

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

( б → а ) → ( c → б ) → c → а

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

Обычное доказательство ( β → α ) → ( γ → β ) → γ → α в естественной дедукции, рассматриваемой как λ-член

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

                                     a:β → α, b:γ → β, g:γ ⊢ b : γ → β    a:β → α, b:γ → β, g:γ ⊢ g : γ
———————————————————————————————————  ————————————————————————————————————————————————————————————————————
a:β → α, b:γ → β, g:γ ⊢ a : β → α      a:β → α, b:γ → β, g:γ ⊢ b g : β
————————————————————————————————————————————————————————————————————————
               a:β → α, b:γ → β, g:γ ⊢ a (b g) : α
               ————————————————————————————————————
               a:β → α, b:γ → β ⊢ λ g. a (b g) : γ → α
               ————————————————————————————————————————
                        a:β → α ⊢ λ b. λ g. a (b g) : (γ → β) → γ → α
                        ————————————————————————————————————
                                ⊢ λ a. λ b. λ g. a (b g) : (β → α) → (γ → β) → γ → α

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

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

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

Обобщения

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

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

Ссылки

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

• Карри, HB (20 сентября 1934 г.). «Функциональность в комбинаторной логике» . Труды Национальной академии наук Соединенных Штатов Америки . 20 (11): 584–90. Бибкод : 1934PNAS...20..584C . дои : 10.1073/pnas.20.11.584 . ISSN   0027-8424 . ПМЦ   1076489 . ПМИД   16577644 .
• Карри, Хаскелл Б; Фейс, Роберт (1958). Крейг, Уильям (ред.). Комбинаторная логика . Исследования по логике и основам математики. Том. 1. Издательство «Северная Голландия». LCCN   a59001593 ; с двумя разделами Крейга Уильяма; см. пункт 9E {{cite book}}: CS1 maint: постскриптум ( ссылка )
• Де Брёйн, Николаас (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 .

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

• Гриффин, Тимоти Г. (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 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 .
• де Кейрос, Руи; Габбай, Дов (1999), «Маркированная естественная дедукция» , в Ольбахе, Ханс-Юрген; Рейл, Уве (ред.), Логика, язык и рассуждение. Очерки в честь Дова Габбая , Тенденции в логике, т. 7, Клювер, стр. 173–250, ISBN.  978-0-7923-5687-5 .
• де Оливейра, Анжолина; де Кейроз, Руи (1999), "Процедура нормализации для эквационального фрагмента помеченной естественной дедукции", Логический журнал группы по интересам в области чистой и прикладной логики , том. 7, Oxford University Press , стр. 173–215 . (Полная версия статьи, представленной на 2-м WoLLIC'95 , Ресифи. Аннотация в журнале Journal of the Interest Group in Pure and Applied Logics 4(2):330–332, 1996.)
• Поэрномо, Иман; Кроссли, Джон; Вирсинг; Мартин (2005), Адаптация доказательств как программ: протокол Карри-Ховарда , Монографии по информатике, Springer , ISBN  978-0-387-23759-6 , касается адаптации синтеза программ «доказательства как программы» к крупнозернистым и императивным задачам разработки программ с помощью метода, который авторы называют протоколом Карри-Ховарда. Включает обсуждение переписки Карри-Ховарда с точки зрения информатики.
• де Кейрос, Руи ЖГБ; де Оливейра, Анджолина (2011), «Функциональная интерпретация прямых вычислений», Электронные заметки по теоретической информатике , 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.)
• де Кейроз, Руи ЖГБ (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 Logicique (Католический университет Лувена), 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
• Читатель монад 6: Приключения в классической стране : Карри-Ховард в Хаскеле, закон Пирса.