Что самые интересные эквивалентности являются результатом Изоморфизма Карри-Говарда?

function composition      | syllogism

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

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

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

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

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

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

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

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

    andImpliesOr :: (a, b) -> Либо a b
   andImpliesOr (a, _) = Влево a
   

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

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

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

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

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

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

    данных ⊥
   данные Xor a b = Xor (Либо a b) ((a, b) -> ⊥)
   

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

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

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

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

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

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 -> *.