Изоморфизм Карри-Говарда

Question

Я искал в Интернете, и я не могу найти никаких объяснений ОМС, которые бы быстро не переросли в лекцию по теории логики, которая резко у меня над головой. (Эти люди говорят так, как будто "исчисление интуиционистских высказываний" - это фраза, которая действительно что-то значит для нормальных людей!)

Грубо говоря, CHI говорит, что типы - это теоремы, а программы - доказательства этих теорем. Но что, черт возьми, это вообще значит?

До сих пор я понял это:

• Рассматривать id :: x -> x, Его тип говорит: "учитывая, что X истинно, мы можем заключить, что X истинно". Похоже, разумная теорема для меня.

• Теперь рассмотрим foo :: x -> y, Как скажет любой программист на Haskell, это невозможно. Вы не можете написать эту функцию. (Ну, в любом случае, без обмана.) Читайте как теорему, там говорится: "учитывая, что любой X истинен, мы можем заключить, что любой Y истинен". Это явно ерунда. И, конечно же, вы не можете написать эту функцию.

• В более общем смысле, аргументы функции могут рассматриваться как "это то, что предполагается истинным", а тип результата может рассматриваться как "то, что является истинным, если все остальные вещи есть". Если есть аргумент функции, скажем x -> yмы можем принять это как допущение, что X, будучи истинным, подразумевает, что Y должен быть истинным.

• Например, (.) :: (y -> z) -> (x -> y) -> x -> z можно принять как "если предположить, что Y подразумевает Z, что X подразумевает Y, и что X истинно, мы можем заключить, что Z истинно". Что кажется логически разумным для меня.

Теперь, что, черт возьми, делает Int -> Int имею в виду?? о_О

Единственный разумный ответ, который я могу придумать, заключается в следующем: если у вас есть функция X -> Y -> Z, тогда сигнатура типа говорит: "Если предположить, что можно построить значение типа X, а другое - типа Y, то можно построить значение типа Z". И тело функции точно описывает, как вы это сделаете.

Кажется, это имеет смысл, но это не очень интересно. Так ясно, что должно быть что-то большее, чем это...

Answer 1

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

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

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

Для экземпляра типа функции, который не является полностью полиморфным и имеет логическое значение, рассмотрим p -> Void (для некоторого р), где Void это необитаемый тип: тип без значений (кроме ⊥ в Хаскеле, но я вернусь к этому позже). Единственный способ получить значение типа Void если вы можете доказать противоречие (что, конечно, невозможно), и так как Void означает, что вы доказали противоречие, вы можете получить любое значение из него (т.е. существует функция absurd :: Void -> a). Соответственно, p -> Void соответствует ¬p: это означает, что "p подразумевает ложь".

Интуиционистская логика - это просто определенный вид логики, которой соответствуют общие функциональные языки. Главное, это конструктивно: в основном, доказательство a -> b дает вам алгоритм для вычисления b от a, что неверно в обычной классической логике (из-за закона исключенного среднего, который скажет вам, что что-то является либо истинным, либо ложным, но не почему).

Хотя функции как Int -> Int не так много значат, как предложения, мы можем делать заявления о них с другими предложениями. Например, мы можем объявить тип равенства двух типов (используя GADT):

data Equal a b where
    Refl :: Equal a a

Если у нас есть значение типа Equal a b, затем a это тот же тип b: Equal a b соответствует предложению a = b. Проблема в том, что таким образом мы можем говорить только о равенстве типов. Но если бы у нас были зависимые типы, мы могли бы легко обобщить это определение для работы с любым значением, и поэтому Equal a b будет соответствовать предположению, что значения a и b идентичны. Так, например, мы могли бы написать:

type IsBijection (f :: a -> b) (g :: b -> a) =
    forall x. Equal (f (g x)) (g (f x))

Здесь f и g являются регулярными функциями, поэтому f может легко иметь тип Int -> Int, Опять же, Хаскелл не может этого сделать; вам нужны зависимые типы, чтобы делать такие вещи.

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

Answer 2

Единственный разумный ответ, который я могу придумать, заключается в следующем: если у вас есть функция X -> Y -> Z, тогда сигнатура типа говорит: "Если предположить, что можно построить значение типа X, а другое - типа Y, то можно построить значение типа Z". И тело функции точно описывает, как вы это сделаете. Кажется, это имеет смысл, но это не очень интересно. Так ясно, что должно быть что-то большее, чем это...

Ну, да, их гораздо больше, потому что это имеет много последствий и открывает много вопросов.

Прежде всего, ваше обсуждение ОМС оформлено исключительно с точки зрения импликации / типов функций (->). Вы не говорите об этом, но вы, вероятно, также видели, как конъюнкция и дизъюнкция соответствуют типам продукта и суммы соответственно. Но как насчет других логических операторов, таких как отрицание, универсальная квантификация и экзистенциальная квантификация? Как мы переводим логические доказательства, связанные с этим, в программы? Оказывается, это примерно так:

• Отрицание соответствует первоклассным продолжениям. Не проси меня объяснить это.
• Универсальное количественное определение пропозициональных (не индивидуальных) переменных соответствует параметрическому полиморфизму. Так, например, полиморфная функция id действительно имеет тип forall a. a -> a
• Экзистенциальная квантификация по пропозициональным переменным соответствует нескольким вещам, связанным с сокрытием данных или реализаций: абстрактные типы данных, системы модулей и динамическая диспетчеризация. Экзистенциальные типы GHC связаны с этим.
• Универсальное и экзистенциальное количественное определение отдельных переменных приводит к системам зависимых типов.

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

Теперь, что, черт возьми, значит Int -> Int?? о_О

Это тип или альтернативное предложение. В f :: Int -> Int, (+1) называет "программу" (в определенном смысле, которая допускает как функции, так и константы как "программы", или, альтернативно, доказательство. Семантика языка должна либо обеспечивать f в качестве примитивного правила вывода или продемонстрировать, как f является доказательством того, что можно построить из таких правил и предпосылок.

Эти правила часто задаются в терминах эквациональных аксиом, которые определяют базовые члены типа и правила, которые позволяют вам доказать, какие другие программы населяют этот тип. Например, переключение с Int в Nat (натуральные числа от 0 вперед), мы могли бы иметь эти правила:

• Аксиома: 0 :: Nat (0 является примитивным доказательством Nat)
• Правило: x :: Nat ==> Succ x :: Nat
• Правило: x :: Nat, y :: Nat ==> x + y :: Nat
• Правило: x + Zero :: Nat ==> x :: Nat
• Правило: Succ x + y ==> Succ (x + y)

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

Answer 3

Возможно, лучший способ понять, что это значит - начать (или попробовать) использовать типы в качестве предложений и программы в качестве доказательств. Лучше изучать язык с зависимыми типами, такими как Agda (он написан на Haskell и похож на Haskell). На этом языке есть различные статьи и курсы. Узнать, что Агда неполна, но она пытается упростить вещи, как книга LYAHFGG.

Вот пример простого доказательства:

{-# OPTIONS --without-K #-} -- we are consistent

module Equality where

-- Peano arithmetic.
-- 
--   ℕ-formation:     ℕ is set.
-- 
--   ℕ-introduction:  o ∈ ℕ,
--                    a ∈ ℕ | (1 + a) ∈ ℕ.
-- 
data ℕ : Set where
  o : ℕ
  1+ : ℕ → ℕ

-- Axiom for _+_.
-- 
--   Form of ℕ-elimination.
-- 
infixl 6 _+_
_+_ : ℕ → ℕ → ℕ
o + m = m
1+ n + m = 1+ (n + m)

-- The identity type for ℕ.
-- 
infix 4 _≡_
data _≡_ (m : ℕ) : ℕ → Set where
  refl : m ≡ m

-- Usefull property.
-- 
cong : {m n : ℕ} → m ≡ n → 1+ m ≡ 1+ n
cong refl = refl

-- Proof _of_ mathematical induction:
-- 
--   P 0, ∀ x. P x → P (1 + x) | ∀ x. P x.
-- 
ind : (P : ℕ → Set) → P o → (∀ n → P n → P (1+ n)) → ∀ n → P n
ind P P₀ _ o = P₀
ind P P₀ next (1+ n) = next n (ind P P₀ next n)

-- Associativity of addition using mathematical induction.
-- 
+-associative : (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-associative m n p = ind P P₀ is m
  where
    P : ℕ → Set
    P i = (i + n) + p ≡ i + (n + p)
    P₀ : P o
    P₀ = refl
    is : ∀ i → P i → P (1+ i)
    is i Pi = cong Pi

-- Associativity of addition using (dependent) pattern matching.
-- 
+-associative′ : (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-associative′ o _ _ = refl
+-associative′ (1+ m) n p = cong (+-associative′ m n p)

Там вы можете увидеть (m + n) + p ≡ m + (n + p) предложение как тип и его доказательство как функция. Существуют более продвинутые методы для таких доказательств (например, рассуждения по предзаказу, комбинаторы в Agda подобны тактике в Coq).

Что еще можно доказать:

• head ∘ init ≡ head для векторов, здесь.

• Ваш компилятор создает программу, выполнение которой дает то же значение, что и значение, полученное при интерпретации той же (основной) программы, здесь, для Coq. Эта книга также является хорошим чтением на тему моделирования языков и верификации программ.

• Что-нибудь еще, что может быть доказано в конструктивной математике, поскольку теория типов Мартина-Лёфа по своей выразительной силе эквивалентна ZFC. Фактически изоморфизм Карри-Говарда может быть распространен на физику и топологию, а также на алгебраическую топологию.