Какие наиболее интересные эквивалентности вытекают из изоморфизма Карри-Ховарда?
Я столкнулся с изоморфизмом Карри-Ховарда относительно поздно в моей жизни программиста, и, возможно, это способствует тому, что он меня полностью очаровывает. Это подразумевает, что для каждой концепции программирования существует точный аналог в формальной логике, и наоборот. Вот "базовый" список таких аналогий, в верхней части моей головы:
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
Редактировать:
Вот еще несколько эквивалентов, собранных из ответов:
function composition | syllogism -- from Apocalisp
continuation-passing | double negation -- from camccann
10 ответов
Поскольку вы явно спросили о самых интересных и неясных из них:
Вы можете расширить CH на множество интересных логик и формулировок логик, чтобы получить действительно широкий спектр соответствий. Здесь я попытался сфокусироваться на некоторых из более интересных, а не на неясных вещах, а также на нескольких фундаментальных, которые еще не появились.
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
РЕДАКТИРОВАТЬ: ссылку, которую я бы порекомендовал всем, кто хочет узнать больше о расширениях CH:
"Судебная реконструкция модальной логики" http://www.cs.cmu.edu/~fp/papers/mscs00.pdf - это отличное место, чтобы начать, потому что оно начинается с первых принципов, и большая часть его призвана стать доступный для не логиков / теоретиков языка. (Хотя я второй автор, поэтому я предвзят.)
Вы немного запачкали вещи относительно недопущения. Ложность представлена необитаемыми типами, которые по определению не могут быть неразрывными, потому что нет ничего такого типа для оценки в первую очередь.
Не прекращение представляет противоречие- противоречивую логику. Несовместимая логика, конечно, позволит вам доказать что угодно, в том числе и ложь.
Игнорируя несоответствия, системы типов обычно соответствуют интуиционистской логике и по необходимости являются конструктивистскими, что означает, что некоторые части классической логики не могут быть выражены напрямую, если они вообще есть. С другой стороны, это полезно, потому что, если тип является допустимым конструктивным доказательством, тогда термин этого типа является средством построения того, что вы доказали в существовании.
Главная особенность конструктивистского аромата заключается в том, что двойное отрицание не эквивалентно неотрицанию. На самом деле, отрицание редко является примитивом в системе типов, поэтому вместо этого мы можем представить его как ложную, например: not P становится P -> Falsity, Таким образом, двойное отрицание будет функцией с типом (P -> Falsity) -> Falsityчто явно не эквивалентно чему-то типа P,
Тем не менее, есть интересный поворот в этом! В языке с параметрическим полиморфизмом переменные типа располагаются по всем возможным типам, включая необитаемые, поэтому это полностью полиморфный тип, такой как ∀a. a в некотором смысле почти ложно. Так что, если мы напишем двойное почти отрицание, используя полиморфизм? Мы получаем тип, который выглядит следующим образом: ∀a. (P -> a) -> a, Это эквивалентно чему-то типа P? На самом деле это так, просто примените его к функции идентичности.
Но какой в этом смысл? Зачем писать такой тип? Значит ли это что- либо в терминах программирования? Ну, вы можете думать об этом как о функции, которая уже имеет что-то типа P где-то, и нужно, чтобы вы дали ему функцию, которая принимает P в качестве аргумента, все это полиморфно в конечном типе результата. В некотором смысле, он представляет собой приостановленное вычисление, ожидая, когда будет предоставлено остальное. В этом смысле эти приостановленные вычисления могут быть составлены вместе, переданы, вызваны, что угодно. Это должно звучать знакомо для поклонников некоторых языков, таких как Scheme или Ruby - потому что это означает, что двойное отрицание соответствует стилю передачи продолжения, и на самом деле тип, который я дал выше, является именно монадой продолжения в Haskell.
Ваша диаграмма не совсем верна; во многих случаях вы путаете типы с терминами.
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 -> *,
Вот немного неясный вопрос, который, как я удивляюсь, раньше не поднимался: "классическое" функциональное реактивное программирование соответствует временной логике.
Конечно, если вы не философ, математик или одержимый функциональный программист, это, вероятно, поднимает еще несколько вопросов.
Итак, во-первых: что такое функциональное реактивное программирование? Это декларативный способ работы с изменяющимися во времени значениями. Это полезно для написания таких вещей, как пользовательские интерфейсы, потому что входные данные пользователя являются значениями, которые меняются во времени. "Классический" FRP имеет два основных типа данных: события и поведение.
События представляют собой значения, которые существуют только в дискретное время. Клавиши - отличный пример: вы можете думать о вводе с клавиатуры как о символе в определенный момент времени. Каждое нажатие клавиши - это просто пара с характером клавиши и временем ее нажатия.
Поведения - это ценности, которые существуют постоянно, но могут постоянно меняться. Положение мыши - отличный пример: это просто поведение координат x, y. В конце концов, мышь всегда имеет свою позицию, и, концептуально, эта позиция постоянно меняется при перемещении мыши. В конце концов, перемещение мыши - это одно длительное действие, а не набор отдельных шагов.
А что такое временная логика? Соответственно, это набор логических правил для работы с предложениями, определенными количественно с течением времени. По сути, он расширяет нормальную логику первого порядка двумя квантификаторами: □ и ◇. Первое означает "всегда": читайте □φ как "φ всегда имеет место". Второе - "в конце концов": ◇φ означает, что "φ в конечном итоге будет иметь место" Это особый вид модальной логики. Следующие два закона касаются квантификаторов:
□φ ⇔ ¬◇¬φ
◇φ ⇔ ¬□¬φ
Таким образом, □ и ◇ двойственны друг другу так же, как ∀ и ∃.
Эти два квантификатора соответствуют двум типам в FRP. В частности, □ соответствует поведению, а ◇ соответствует событиям. Если мы думаем о том, как эти типы обитаемы, это должно иметь смысл: поведение обитается в любое возможное время, в то время как событие происходит только один раз.
Мне очень нравится этот вопрос. Я немного знаю, но у меня есть несколько вещей (при поддержке статьи в Википедии, в которой есть несколько аккуратных таблиц и тому подобное):
Я думаю, что сумма типов / объединение типов (например,
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 верны, то по крайней мере один верен. Таким образом, если дискриминационные союзы являются какой-либо формой разъединения, они должны быть всеобъемлющим разнообразием. Я думаю, что это является доказательством, но не стесняйтесь разубеждать меня в этом понятии.Точно так же ваши определения тавтологии и абсурда как функции тождества и не завершающих функций, соответственно, немного ошибочны. Истинная формула представлена типом блока, который является типом, который имеет только один элемент (
data ⊤ = ⊤; часто пишется()и / илиUnitв функциональных языках программирования). Это имеет смысл: поскольку этот тип гарантированно обитаем, и поскольку существует только один возможный обитатель, это должно быть правдой. Тождественная функция просто представляет особую тавтологию, что a → a.Ваш комментарий о не завершающих функциях, в зависимости от того, что именно вы имели в виду, более полезен. Curry-Howard функционирует в системе типов, но не завершается там. Согласно Википедии, проблема отсутствия терминации является проблемой, так как добавление ее приводит к противоречивой логике (например, я могу определить
wrong :: a -> bотwrong x = wrong xи тем самым "докажем", что a → b для любых a и b). Если это то, что вы имели в виду под "абсурдом", тогда вы совершенно правы. Если вместо этого вы имели в виду ложное утверждение, то вместо этого вам нужен любой необитаемый тип, например, определенный какdata ⊥То есть тип данных без какого-либо способа его построения. Это гарантирует, что у него вообще нет значений, и поэтому он должен быть необитаем, что эквивалентно false. Я думаю, что вы могли бы также использоватьa -> b, поскольку если мы запрещаем не завершающие функции, то это тоже необитаемо, но я не уверен на 100%.Википедия говорит, что аксиомы кодируются двумя различными способами, в зависимости от того, как вы интерпретируете Curry-Howard: либо в комбинаторах, либо в переменных. Я думаю, что представление комбинатора означает, что примитивные функции, которые нам даны, кодируют то, что мы можем сказать по умолчанию (подобно тому, как modus ponens является аксиомой, потому что приложение функции является примитивным). И я думаю, что представление переменных может фактически означать одно и то же - комбинаторы, в конце концов, являются просто глобальными переменными, которые являются определенными функциями. Что касается примитивных типов: если я правильно об этом думаю, то я думаю, что примитивные типы - это сущности - примитивные объекты, о которых мы пытаемся доказать.
Согласно моей логике и классу семантики, тот факт, что (a ∧ b) → c ≡ a → (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затем определяется как содержащий (и)Eithera или a b (или) и функция (импликация) от (a, b) (и) до нижнего типа (false).Однако я понятия не имею, что это значит.(Изменить 1: Теперь я вижу, см. Следующий абзац!)Поскольку нет значений типа(a,b) -> ⊥(есть?), я не могу понять, что это будет означать в программе.Кто-нибудь знает лучший способ думать об этом определении или другом?(Изменить 1: Да, Camccann.)Редактировать 1: Благодаря ответу Camccann (в частности, комментарии, которые он оставил на нем, чтобы помочь мне), я думаю, что я вижу, что здесь происходит. Чтобы построить значение типа
Xor a bВам нужно предоставить две вещи. Во-первых, свидетель наличия элементаaили жеbв качестве первого аргумента; этоLeft aилиRight b, И второе, доказательство того, что нет элементов обоих типовaа такжеbДругими словами, доказательство того, что(a,b)необитаем - как второй аргумент. Поскольку вы сможете написать только функцию из(a,b) -> ⊥если(a,b)является необитаемым, что это значит для этого быть? Это будет означать, что некоторая часть объекта типа(a,b)не может быть построен; другими словами, что по крайней мере один, и, возможно, оба изaа такжеbтакже необитаемы! В этом случае, если мы думаем о сопоставлении с шаблоном, вы не могли бы сопоставить шаблон с таким кортежем: предположим, чтоbявляется необитаемым, что бы мы написали, что может соответствовать второй части этого кортежа? Таким образом, мы не можем сопоставить шаблон с ним, что может помочь вам понять, почему это делает его необитаемым. Теперь, единственный способ иметь тотальную функцию, которая не принимает аргументов (как этот должен, так как(a,b)является необитаемым) для того, чтобы результат тоже был необитаемым типом - если мы думаем об этом с точки зрения сопоставления с образцом, это означает, что, хотя у функции нет ни одного случая, у нее нет ни одного возможного тела, и так что все в порядке.
Многое из того, что я думаю вслух / доказываю (надеюсь) вещи на лету, но я надеюсь, что это полезно. Я действительно рекомендую статью в Википедии; Я не читал его во всех подробностях, но его таблицы - действительно хорошее резюме, и оно очень подробное.
Относительно связи между продолжениями и двойным отрицанием тип вызова / cc является законом Пирса http://en.wikipedia.org/wiki/Call-with-current-continuation
СН обычно определяется как соответствие между интуиционистской логикой и программами. Однако, если мы добавим оператор call-with-current-продолжение (callCC) (тип которого соответствует закону Пирса), мы получим соответствие между классической логикой и программами с callCC.
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-продолжение, но я не видел ни одного из существующих языков в этой форме. Так что изобретать что-то может быть интересно, я думаю.
Хотя это не простой изоморфизм, это обсуждение конструктивной LEM является очень интересным результатом. В частности, в разделе "Выводы" Олег Киселев обсуждает, как использование монад для получения исключения двойного отрицания в конструктивной логике аналогично выделению вычислимо разрешимых предложений (для которых LEM действителен в конструктивном контексте) из всех предложений. Представление о том, что монады захватывают вычислительные эффекты, является старым, но этот пример изоморфизма Карри - Говарда помогает взглянуть на него в перспективе и помогает понять, что в действительности означает "двойное отрицание".
Поддержка продолжений первого класса позволяет выразить $P \lor \neg P$. Уловка основана на том факте, что отсутствие вызова продолжения и выхода с некоторым выражением эквивалентно вызову продолжения с тем же выражением.
Для более детального просмотра, пожалуйста, смотрите: http://www.cs.cmu.edu/~rwh/courses/logic/www-old/handouts/callcc.pdf