Переписка Карри – Ховарда - Curry–Howard correspondence

Доказательство, написанное как функциональная программа
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)) (fun 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 m = m + 0}$${\ Displaystyle S (m + y) = m + Sy}$

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

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

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

Зачатки заочной Карри-Говарда лежат в нескольких наблюдений:

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

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

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

Это соответствие стало отправной точкой большого спектра новых исследований после его открытия, что привело, в частности, к новому классу формальных систем, предназначенных для работы как в качестве системы доказательства, так и в качестве типизированного функционального языка программирования . Это включает в себя Martin-LOF «s интуиционистской теории типа и Coquand » s Исчисление конструкций , двух исчислений , в которых доказательства являются обычными объектами дискурса и в котором можно утверждать , свойства доказательств точно так же , как любой программы. Эту область исследований принято называть современной теорией типов .

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Вначале это было простое замечание из книги Карри и Фейса по комбинаторной логике 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}}}$

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

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

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

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

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

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

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

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

α → ( β → α ) и

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

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

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

Интуиционистский импликационный естественный вывод	Правила присвоения типов лямбда-исчисления
${\ 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 xt: \ 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 типа α → α → α не выделялись бы в соответствии. Примеры приведены ниже .

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Толкование BHK

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

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

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

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

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

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

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

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

• ${\ displaystyle \ top}$ это объект
• если α и β - объекты, то и являются объектами.${\ Displaystyle \ альфа \ раз \ бета}$${\ displaystyle \ alpha \ rightarrow \ beta}$

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

• ${\ displaystyle id}$, , , И морфизмы${\ displaystyle \ star}$${\ displaystyle \ operatorname {eval}}$${\ displaystyle \ pi _ {1}}$${\ displaystyle \ pi _ {2}}$
• если t - морфизм, λ t - морфизм
• если t и u - морфизмы, и - морфизмы.${\ Displaystyle (т, и)}$${\ 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 т \ CIRCID = т}$
• ${\ Displaystyle (v \ circ u) \ circ t = v \ circ (и \ circ t)}$
• ${\ displaystyle \ star = id}$ (если набрано правильно)
• ${\ displaystyle \ star \ circ u = \ star}$
• ${\ Displaystyle \ pi _ {1} \ circ (т, и) = т}$
• ${\ Displaystyle \ пи _ {2} \ circ (т, и) = и}$
• ${\ 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  : ( β → γ ) → ( α → β ) → α → γ.

Перестановка имен переменных α и γ дает нам

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

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

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

Ниже схема дает доказательство ( & beta ; → & alpha ; ) → ( & gamma ; → & beta ; ) → гамма → альфа в естественной дедукции и показывает , как это может быть интерпретировано как Х-выражение λ в сОе б .λ г . ( ( Б г )) типа ( β → α ) → ( γ → β ) → γ → α .

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

Обобщения

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

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

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

Семинальные ссылки

• Карри, HB (1934-09-20). «Функциональность в комбинаторной логике» . Труды Национальной академии наук Соединенных Штатов Америки . 20 (11): 584–90. Bibcode : 1934PNAS ... 20..584C . DOI : 10.1073 / pnas.20.11.584 . ISSN  0027-8424 . PMC  1076489 . PMID  16577644 .
• Карри, Haskell B; Фейс, Роберт (1958). Крейг, Уильям (ред.). Комбинаторная логика . Исследования по логике и основам математики. 1 . Издательская компания Северной Голландии. LCCN  a59001593 ; с двумя разделами Крейга, Уильяма; см. пункт 9ECS1 maint: postscript ( ссылка )
• Де Брейн, Николаас (1968), Automath, язык для математики , факультет математики, Технологический университет Эйндховена, 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, Санкт-Петербург, Россия , Lecture Notes in Computer Science, 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. DOI : 10.2307 / 2275370 . JSTOR  2275370 .. (Полная версия статьи представлена ​​на Logic Colloquium '90 , Хельсинки. Аннотация в JSL 56 (3): 1139–1140, 1991.)
• де Кейруш, Руи; Габбай, Дов (1994), «Равенство в помеченных дедуктивных системах и функциональная интерпретация пропозиционального равенства», в Dekker, Paul; Стохоф, Мартин (ред.), Труды девятого Амстердамского коллоквиума , ILLC / Департамент философии, Амстердамский университет, стр. 547–565, ISBN 978-90-74795-07-4.
• де Кейруш, Руи; Габбай, Дов (1995), "Функциональная интерпретация экзистенциального квантора" , Бюллетень группы интересов по чистой и прикладной логике , 3 , стр. 243–290.. (Полная версия статьи представлена ​​на Logic Colloquium '91 , Упсала. Аннотация в JSL 58 (2): 753–754, 1993.)
• де Кейруш, Руи; Габбай, Дов (1997), «Функциональная интерпретация модальной необходимости», in de Rijke, Maarten (ed.), Advances in Intensional Logic , Applied Logic Series, 7 , Springer-Verlag , pp. 61–91, ISBN 978-0-7923-4711-8.
• де Кейруш, Руи; Габбай, Дов (1999), «Маркированная естественная дедукция» , в Ольбахе, Ханс-Юрген; Рейл, Уве (ред.), Логика, язык и рассуждение. Очерки в честь Дов Габбая , Тенденции в логике, 7 , Kluwer, стр. 173–250, ISBN 978-0-7923-5687-5.
• де Оливейра, Анжолина; de Queiroz, Ruy (1999), "Процедура нормализации для фрагмента уравнения помеченного естественного вывода", Logic Journal of the Interest Group in Pure and Applied Logics , 7 , Oxford University Press , стр. 173–215. (Полная версия статьи представлена ​​на 2-й конференции WoLLIC'95 , Ресифи. Резюме в Journal of the Interest Group in Pure and Applied Logics 4 (2): 330–332, 1996.)
• Поэрномо, Иман; Кроссли, Джон; Wirsing; Мартин (2005), « Адаптация доказательств как программы: протокол Карри – Ховарда» , монографии в области компьютерных наук, Springer , ISBN 978-0-387-23759-6, касается адаптации программного синтеза «доказательства как программы» к грубым и императивным задачам разработки программ с помощью метода, который авторы называют протоколом Карри – Ховарда. Включает обсуждение соответствия Карри – Ховарда с точки зрения информатики.
• де Кейруш, Руи Дж.Б. де Оливейра, Анджолина (2011), «Функциональная интерпретация прямых вычислений», Электронные заметки по теоретической информатике , Elsevier , 269 : 19–40, doi : 10.1016 / j.entcs.2011.03.003. (Полная версия статьи представлена ​​на LSFA 2010 , Натал, Бразилия.)

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

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

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

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

Книги

• Де Гроот, Филипп, изд. (1995), Изоморфизм Карри-Ховарда , Cahiers du Centre de Logique (Католический университет Лувена), 8 , Academia-Bruylant, 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, Архивируются с оригинала на 2008-04-18, заметки по теории доказательств с изложением соответствия Карри – Ховарда.
• Томпсон, Саймон (1991), Теория типов и функциональное программирование , Аддисон-Уэсли, ISBN 0-201-41667-0.
• Поэрномо, Иман; Кроссли, Джон; Wirsing; Мартин (2005), « Адаптация доказательств как программы: протокол Карри – Ховарда» , монографии в области компьютерных наук, Springer , ISBN 978-0-387-23759-6, касается адаптации программного синтеза «доказательства как программы» к грубым и императивным задачам разработки программ с помощью метода, который авторы называют протоколом Карри – Ховарда. Включает обсуждение соответствия Карри – Ховарда с точки зрения информатики.
• Binard, F .; Felty, A. (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

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

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

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

• Говард о Карри-Ховарде
• Соответствие Карри – Ховарда в Haskell
• The Monad Reader 6: Adventures in Classical-Land : Curry – Howard in Haskell, закон Пирса.