Каковы наиболее интересные эквивалентности, вытекающие из изоморфизма Карри-Говарда?

Question

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

program/definition        | proof
type/declaration          | proposition
inhabited type            | theorem/lemma
function                  | implication
function argument         | hypothesis/antecedent
function result           | conclusion/consequent
function application      | modus ponens
recursion                 | induction
identity function         | tautology
non-terminating function  | absurdity/contradiction
tuple                     | conjunction (and)
disjoint union            | disjunction (or)          -- corrected by Antal S-Z
parametric polymorphism   | universal quantification

Итак, на мой вопрос: Каковы некоторые из наиболее интересных / неясных последствий этого изоморфизма? Я не логик, поэтому я уверен, что только поцарапал поверхность этим списком.

Например, вот некоторые понятия программирования, для которых я не знаю содержательных имен в логике:

currying                  | "((a & b) => c) iff (a => (b => c))"
scope                     | "known theory + hypotheses"

А вот несколько логических понятий, которые я не совсем закрепил в терминах программирования:

primitive type?           | axiom
set of valid programs?    | theory

Edit:

Вот еще несколько эквивалентов, полученных из ответов:

function composition      | syllogism                -- from Apocalisp
continuation-passing      | double negation          -- from camccann

Answer 1

Поскольку вы явно спросили о самых интересных и неясных из них:

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

evaluation             | proof normalisation/cut-elimination
variable               | assumption
S K combinators        | axiomatic formulation of logic   
pattern matching       | left-sequent rules 
subtyping              | implicit entailment (not reflected in expressions)
intersection types     | implicit conjunction
union types            | implicit disjunction
open code              | temporal next
closed code            | necessity
effects                | possibility
reachable state        | possible world
monadic metalanguage   | lax logic
non-termination        | truth in an unobservable possible world
distributed programs   | modal logic S5/Hybrid logic
meta variables         | modal assumptions
explicit substitutions | contextual modal necessity
pi-calculus            | linear logic

РЕДАКТИРОВАТЬ: ссылку, которую я бы порекомендовал всем, кто хочет узнать больше о расширениях C-H:

«Судебная реконструкция модальной логики» http://www.cs.cmu.edu/~fp/papers/mscs00.pdf - это отличное место для начала, потому что оно начинается с первых принципов, и большая часть его предназначена для того, чтобы быть доступными для не логиков / теоретиков языка. (Хотя я второй автор, поэтому я предвзят.)

Answer 2

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

Не окончание представляет противоречие - противоречивая логика.Несовместимая логика, конечно, позволит вам доказать что угодно , включая ложь, однако.

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

Главная особенность конструктивистского аромата заключается в том, что двойное отрицание не эквивалентно неотрицанию.Фактически, отрицание редко является примитивом в системе типов, поэтому вместо этого мы можем представить его как ложную, например, not P становится P -> Falsity.Таким образом, двойное отрицание было бы функцией с типом (P -> Falsity) -> Falsity, которая явно не эквивалентна чему-то просто типа P.

Однако в этом есть интересный поворот!В языке с параметрическим полиморфизмом переменные типа варьируются по всем возможным типам, включая необитаемые, поэтому полностью полиморфный тип, такой как ∀a. a, в некотором смысле почти ложен.Так что, если мы напишем двойное почти отрицание, используя полиморфизм?Мы получаем тип, который выглядит следующим образом: ∀a. (P -> a) -> a.Это эквивалентно чему-то типа P? На самом деле это , просто примените его к функции идентификации.

Но какой в ​​этом смысл?Зачем писать такой тип?Значит ли это в программировании?Что ж, вы можете думать о ней как о функции, которая уже где-то имеет тип P и требует, чтобы вы дали ей функцию, которая принимает P в качестве аргумента, при этом все это является полиморфным в конечном типе результата.В некотором смысле он представляет собой приостановленное вычисление , ожидающее предоставления остальных.В этом смысле эти приостановленные вычисления могут быть составлены вместе, переданы, вызваны, что угодно.Это должно звучать знакомо для поклонников некоторых языков, таких как Scheme или Ruby - потому что это означает, что двойное отрицание соответствует стиль передачи продолжения , и фактическиТип, который я дал выше, является именно монадой продолжения в Хаскеле.

Answer 3

Ваш график не совсем правильный; во многих случаях вы путаете типы с терминами.

function type              implication
function                   proof of implication
function argument          proof of hypothesis
function result            proof of conclusion
function application RULE  modus ponens
recursion                  n/a [1]
structural induction       fold (foldr for lists)
mathematical induction     fold for naturals (data N = Z | S N)
identity function          proof of A -> A, for all A
non-terminating function   n/a [2]
tuple                      normal proof of conjunction
sum                        disjunction
n/a [3]                    first-order universal quantification
parametric polymorphism    second-order universal quantification
currying                   (A,B) -> C -||- A -> (B -> C), for all A,B,C
primitive type             axiom
types of typeable terms    theory
function composition       syllogism
substitution               cut rule
value                      normal proof

[1] Логика функционального языка, полного по Тьюрингу, противоречива. Рекурсия не имеет соответствия в последовательных теориях. В непоследовательной логике / теории несостоятельности вы можете назвать это правилом, которое вызывает несостоятельность / несостоятельность.

[2] Опять же, это является следствием полноты. Это было бы доказательством анти-теоремы, если бы логика была последовательной - следовательно, она не может существовать.

[3] Не существует в функциональных языках, поскольку они исключают логические функции первого порядка: все количественное определение и параметризация выполняются по формулам. Если бы у вас были функции первого порядка, был бы вид, отличный от *, * -> * и т. Д .; вид элементов предметной области. Например, в диапазоне Father(X,Y) :- Parent(X,Y), Male(X), X и Y в области дискурса (назовите его Dom) и Male :: Dom -> *.

Answer 4

function composition      | syllogism

Answer 5

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

1. Я думаю, что типы сумм / типы объединений ( например, data Either a b = Left a | Right b) эквивалентны включительно дизъюнкции. И, хотя я не очень хорошо знаком с Карри-Говардом, я думаю, что это демонстрирует это. Рассмотрим следующую функцию:

   andImpliesOr :: (a,b) -> Either a b
   andImpliesOr (a,_) = Left a
   

   Если я правильно понимаю вещи, тип говорит, что ( a ∧ b ) → ( a ★ b ) и определение говорит, что это правда, где ★ является либо включающим, либо исключительным, или, в зависимости от того, Either представляет. У вас есть Either, представляющий эксклюзив или, ⊕; однако ( a ∧ b ) ↛ ( a ⊕ b ). Например, ⊤ ∧ ⊤ ≡ ⊤, но ⊤ ⊕ ⊥ ≡ ⊥ и ⊤ ↛ ⊥. Другими словами, если оба a и b верны, то гипотеза верна, но вывод неверен, и поэтому это предположение должно быть ложным. Однако ясно, что ( a ∧ b ) → ( a ∨ b ), поскольку, если оба a и b - правда, тогда, по крайней мере, один - правда. Таким образом, если дискриминационные союзы являются какой-то формой дизъюнкции, они должны быть всеобъемлющим разнообразием. Я думаю, что это является доказательством, но не стесняйтесь разубеждать меня в этом понятии.

2. Точно так же ваши определения тавтологии и абсурда как функции тождества и не завершающих функций, соответственно, немного неправильны. Истинная формула представлена ​​ типом единицы , который является типом, который имеет только один элемент (data ⊤ = ⊤; часто пишется () и / или Unit в функциональных языках программирования). Это имеет смысл: поскольку этот тип гарантированно заселен, и поскольку существует только один возможный обитатель, это должно быть правдой. Функция тождества просто представляет особую тавтологию, которая a → a .

   Ваш комментарий о не завершающих функциях, в зависимости от того, что именно вы имели в виду, более полезен. Curry-Howard работает в системе типов, но нетерминация там не кодируется. Согласно Wikipedia , проблема с прерыванием является проблемой, так как добавление этого приводит к несовместимой логике ( например , я могу определить wrong :: a -> b с помощью wrong x = wrong x и, таким образом, «доказать» что a → b для любых a и b ). Если это то, что вы имели в виду под «абсурдом», тогда вы совершенно правы. Если вместо этого вы имели в виду ложное утверждение, то вместо этого вам нужен любой необитаемый тип, например, , определенный как data ⊥, то есть тип данных без какого-либо способа его создания. Это гарантирует, что у него вообще нет значений, и поэтому он должен быть необитаем, что эквивалентно false. Я думаю, что вы, вероятно, могли бы также использовать a -> b, поскольку, если мы запрещаем не завершающие функции, то это также необитаемо, но я не уверен на 100%.

3. Википедия говорит, что аксиомы кодируются двумя различными способами, в зависимости от того, как вы интерпретируете Curry-Howard: либо в комбинаторах, либо в переменных. Я думаю, что представление комбинатора означает, что примитивные функции, которые нам даны, кодируют то, что мы можем сказать по умолчанию (подобно тому, как modus ponens является аксиомой, потому что приложение функции является примитивным). И я думаю , что представление переменных может фактически означать одно и то же - комбинаторы, в конце концов, являются просто глобальными переменными, которые являются конкретными функциями. Что касается примитивных типов: если я правильно об этом думаю, то я думаю, что примитивные типы - это сущности - примитивные объекты, о которых мы пытаемся доказать.

4. Согласно моей логике и семантике класс, фактв ( a ∧ b ) → c ≡ a → ( b → c ) (а также то, что b → ( a → c )) называется законом эквивалентности экспорта, по крайней мере, в доказательствах естественного вывода.В то время я не заметил, что это было просто карри - хотелось бы, потому что это круто!

5. Хотя у нас теперь есть способ представить включительно у нас нет способа представить эксклюзивное разнообразие.Мы должны быть в состоянии использовать определение исключительного дизъюнкции для его представления: a ⊕ b ≡ ( a ∨ b ) ∧ ¬( a ∧ b ).Я не знаю, как написать отрицание, но я знаю, что ¬ p ≡ p → ⊥, и импликация, и ложь просты.Таким образом, мы должны представлять исключительную дизъюнкцию следующим образом:

   data ⊥
   data Xor a b = Xor (Either a b) ((a,b) -> ⊥)
   

   Это определяет ⊥ как пустой тип без значений, что соответствует ложности;Затем определяется Xor, который содержит ( и ) Either a или b ( или ) и функцию( значение ) от (a, b) ( и ) до нижнего типа ( false ). Однако я понятия не имею, что означает . ( Редактировать 1: Теперь я вижу, см. Следующий абзац!) Поскольку значений неттипа (a,b) -> ⊥ (есть?), я не могу понять, что это будет означать в программе.Кто-нибудь знает лучший способ подумать об этом или другом определении? ( Редактировать 1: Да, camccann .)

   Редактировать1: Благодаря ответу Камкканна (точнее, комментариям, которые он оставил, чтобы помочь мне), я думаю, что я вижу, что здесь происходит.Чтобы создать значение типа Xor a b, вам нужно предоставить две вещи.Во-первых, свидетельство существования элемента либо a, либо b в качестве первого аргумента;то есть Left a или Right b.И, во-вторых, доказательство того, что нет элементов обоих типов a и b - другими словами, доказательство того, что (a,b) необитаемо - в качестве второго аргумента.Поскольку вы сможете написать функцию из (a,b) -> ⊥, только если (a,b) необитаем, что это значит?Это будет означать, что некоторая часть объекта типа (a,b) не может быть построена;другими словами, что по крайней мере один, а возможно и оба из a и b также необитаемы!В этом случае, если мы думаем о сопоставлении с образцом, вы не могли бы сопоставить шаблон с таким кортежем: предположим, что b необитаем, что бы мы написали, что могло бы соответствовать второй части этого кортежа?Таким образом, мы не можем сопоставить шаблон с ним, что может помочь вам понять, почему это делает его необитаемым.Теперь, единственный способ иметь функцию total, которая не принимает аргументов (как этот должен, так как (a,b) необитаем), заключается в том, чтобы результат был тоже необитаемого типа - если мы думаем об этом из шаблона -с точки зрения соответствия, это означает, что, хотя у функции нет ни одного случая, нет возможности body , в котором она могла бы быть, и поэтому все в порядке.

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

Answer 6

Вот немного неясный вопрос, который, как я удивился, раньше не поднимался: «классическое» функциональное реактивное программирование соответствует временной логике.

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

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

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

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

А что такое временная логика? Соответственно, это набор логических правил для работы с предложениями, определенными количественно с течением времени. По сути, он расширяет нормальную логику первого порядка двумя квантификаторами: □ и ◇. Первое означает «всегда»: читайте □ φ как «φ всегда имеет место». Второе - «в конце концов»: ◇ φ означает, что «φ в конечном итоге будет иметь место». Это особый вид модальной логики . Следующие два закона касаются квантификаторов:

□φ ⇔ ¬◇¬φ
◇φ ⇔ ¬□¬φ

Таким образом, □ и ◇ двойственны друг другу так же, как ∀ и ∃.

Эти два квантификатора соответствуют двум типам в FRP. В частности, □ соответствует поведению, а ◇ соответствует событиям. Если мы думаем о том, как эти типы обитаемы, это должно иметь смысл: поведение обитается в каждое возможное время, в то время как событие происходит только один раз.

Answer 7

Относительно связи между продолжениями и двойным отрицанием тип вызова / cc - это закон Пирса http://en.wikipedia.org/wiki/Call-with-current-continuation

C-H обычно определяется как соответствие между интуиционистской логикой и программами. Однако, если мы добавим оператор call-with-current-continue (callCC) (тип которого соответствует закону Пирса), мы получим соответствие между классической логикой и программами с callCC.

Answer 8

2-continuation           | Sheffer stoke
n-continuation language  | Existential graph
Recursion                | Mathematical Induction

Одной вещью, которая важна, но еще не исследована, является отношение 2-продолжения (продолжения, которое принимает 2 параметра) и Шеффера . В классической логике инсульт Шеффера сам по себе может сформировать целостную логическую систему (плюс некоторые неоператорные концепции). Это означает, что знакомые and, or, not могут быть реализованы, используя только сток Шеффера или nand.

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

Типовая сигнатура 2-продолжения (a,b) -> Void. С помощью этой реализации мы можем определить 1-продолжение (нормальное продолжение) как (a,a) -> Void, тип продукта как ((a,b)->Void,(a,b)->Void)->Void, тип суммы как ((a,a)->Void,(b,b)->Void)->Void. Это дает нам впечатляющую силу выразительности.

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

Answer 9

Первоклассная поддержка продолжений позволяет вам выразить $ P \ lor \ neg P $. Уловка основана на том факте, что отсутствие вызова продолжения и выхода с некоторым выражением эквивалентно вызову продолжения с тем же выражением.

Для более детального просмотра смотрите: http://www.cs.cmu.edu/~rwh/courses/logic/www-old/handouts/callcc.pdf

Answer 10

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