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

Ответ 1

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

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

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

Для экземпляра типа функции, который не является полностью полиморфным и имеет логический смысл, рассмотрим p -> Void (для некоторого p), где Void - неинжинированный тип: тип без значений (кроме ⊥, в Haskell, но я доберусь до этого позже). Единственный способ получить значение типа 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, действуют как доказательство любого предложения, Но total языки, такие как Coq и Agda использовать соответствие, чтобы действовать как системы доказательств, а также языки, зависящие от языка программирования.

Ответ 2

Возможно, лучший способ понять, что это значит, - начать (или попробовать) использование типов в качестве предложений и программ в качестве доказательств. Лучше изучить язык с зависимыми типами, например Agda (он написан в Haskell и похож на Haskell). Существуют различные статьи и курсы на этом языке. Узнайте, что вы Agda является неполным, но он пытается упростить вещи, как и книга 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. В самом деле, изоморфизм Карри-Говарда может быть расширен до физика и топология и алгебраической топологии.

Ответ 3

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

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

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

• Отрицание соответствует первоклассным продолжениям. Не просите меня объяснить это.
• Универсальная квантификация по пропозициональным (не индивидуальным) переменным соответствует параметрическому полиморфизму. Так, например, полиморфная функция 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)

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