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

Ответ 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

EDIT: ссылка, которую я бы рекомендовал всем, кто интересуется расширением C-H:

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

Ответ 2

Ты немного путаешься о нетерпении. Фальшивость представлена ​​необитаемыми типами, которые по определению не могут быть бесконечными, потому что в этом нет ничего такого типа.

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

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

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

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

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

Ответ 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 -> *.

Ответ 4

function composition      | syllogism

Ответ 5

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

• Я думаю, что типы сумм/типы объединения (например, 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 b)   (a   b). Например,     Другими словами, если оба a и b истинны, то гипотеза верна, но заключение ложно, и поэтому эта импликация должна быть ложной. Однако, очевидно, (a b b)   (a ∨ b), так как если оба a и b истинны, то по крайней мере одно верно. Таким образом, если дискриминационные союзы являются одной из форм дизъюнкции, они должны быть инклюзивным. Я считаю, что это является доказательством, но я чувствую больше, чем свободен, чтобы избавить меня от этого понятия.

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

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

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

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

• Пока у нас есть способ представить инклюзивную дизъюнкцию, у нас нет способа представлять эксклюзивный сорт. Мы должны иметь возможность использовать определение исключительной дизъюнкции для его представления: 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: Да, camcann.)

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

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

Ответ 6

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

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

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

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

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

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

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

Итак, □ и ◇ являются двойственными друг к другу так же, как и ∀ и ∃.

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

Ответ 7

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

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

Ответ 8

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

Ответ 9

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

Подробнее см. ниже: http://www.cs.cmu.edu/~rwh/courses/logic/www-old/handouts/callcc.pdf

Ответ 10

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. Это дает нам впечатляющую силу выразительности.

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