Зависимые пары, карринг и Карри-Говард
Jan. 21st, 2013 02:01 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
thedeemonВсе мы помним про карринг, позволяющий функцию, принимающую пару аргументов, заменить на функцию от одного аргумента, возвращающую функцию от второго, которая уже возвращает нужный результат. Типы ((a,b) -> c) и (a -> b -> c) эквивалентны, т.к. мы можем описать две функции от одного к другому и обратно, композиция которых равна id, т.е. построить изоморфизмы. Запишем их на хаскелеподобном языке Идрис:
В хаскеле они есть в стандартной библиотеке под именами curry и uncurry. Теперь вспомним соответствие Карри-Говарда, связывающее типы с утверждениями, а значения с доказательствами. Произведение типов (тупл, product type) там превращается в конъюнкцию, функциональный тип - в следствие. Фактически, выше мы доказали утверждение
((A & B) => C) == (A => (B => C))
Теперь перенесемся в мир зависимых типов, взяв тот же язык Идрис. Одним из базовых элементов, появляющихся с зависимыми типами, является зависимая пара - обобщение произведения типов, также известное как зависимая сумма (dependent sum):
Σ(x:A),P(x)
Это тип пары элементов, где тип второго элемента зависит от значения первого элемента. Далее для порядка будем типы обозначать большими буквами, а значения маленькими. В идрисе зависимая пара определа так:
Слово Exists, как и знак Σ, появилось тут неслучайно. Логическая интепретация такой пары звучит как "существует такой x, для которого выполнено утверждение Р(х)". Сам Σ-тип становится утверждением о том, что это дело существует, а значения этого типа, пары конкретных значений, становятся доказательствами. В них первый элемент называется witness, свидетель, т.к. это конкретный пример того значения х, про которое мы утверждаем, что оно существует, а второй элемент называется proof, т.к. он служит доказательством выполненности утверждения Р для этого х. Для таких пар в идрисе есть специальный синтаксис:
(a ** b)
Аналогами функций fst и snd, извлекающих первый и второй элементы пары, служат функции getWitness и getProof:
Теперь давайте возьмем описанные в начале поста изоморфизмы про обычные пары, и запишем их для зависимых пар:
Тела функций те же самые, просто операции с туплами поменялись на операции с зависимыми парами. Что же нам говорят типы? Что мы доказали следующее утверждение:
((∃x:A . B(x)) => C) == (∀x:A . (B(x) => C))
Это то, что позволяет в языках вроде хаскеля и окамла записывать экзистенциальные типы, обходясь без ключевого слова exists, а лишь квантором всеобщности forall.
Еще один морфизм на ту же тему:
Он показывает, что
(∃x:A . (B(x) => C)) => ((∀x:A . B(x)) => C)
Говорят, что в обратную сторону тоже верно, но у меня такую функцию построить не получилось.
id1 : ((a,b) -> c) -> (a -> b -> c) id1 f = \a => \b => f (a,b) id2 : (a -> b -> c) -> ((a,b) -> c) id2 f = \pair => f (fst pair) (snd pair)
В хаскеле они есть в стандартной библиотеке под именами curry и uncurry. Теперь вспомним соответствие Карри-Говарда, связывающее типы с утверждениями, а значения с доказательствами. Произведение типов (тупл, product type) там превращается в конъюнкцию, функциональный тип - в следствие. Фактически, выше мы доказали утверждение
((A & B) => C) == (A => (B => C))
Теперь перенесемся в мир зависимых типов, взяв тот же язык Идрис. Одним из базовых элементов, появляющихся с зависимыми типами, является зависимая пара - обобщение произведения типов, также известное как зависимая сумма (dependent sum):
Σ(x:A),P(x)
Это тип пары элементов, где тип второго элемента зависит от значения первого элемента. Далее для порядка будем типы обозначать большими буквами, а значения маленькими. В идрисе зависимая пара определа так:
data Exists : (A : Type) -> (P : A -> Type) -> Type where
Ex_intro : {P : A -> Type} -> (a : A) -> P a -> Exists A PСлово Exists, как и знак Σ, появилось тут неслучайно. Логическая интепретация такой пары звучит как "существует такой x, для которого выполнено утверждение Р(х)". Сам Σ-тип становится утверждением о том, что это дело существует, а значения этого типа, пары конкретных значений, становятся доказательствами. В них первый элемент называется witness, свидетель, т.к. это конкретный пример того значения х, про которое мы утверждаем, что оно существует, а второй элемент называется proof, т.к. он служит доказательством выполненности утверждения Р для этого х. Для таких пар в идрисе есть специальный синтаксис:
(a ** b)
Аналогами функций fst и snd, извлекающих первый и второй элементы пары, служат функции getWitness и getProof:
getWitness : {P : a -> Type} -> Exists a P -> a
getWitness (a ** v) = a
getProof : {P : a -> Type} -> (s : Exists a P) -> P (getWitness s)
getProof (a ** v) = vТеперь давайте возьмем описанные в начале поста изоморфизмы про обычные пары, и запишем их для зависимых пар:
using (A : Type, B : A->Type, C : Type) id3 : ((x:A ** B x) -> C) -> ((x:A) -> B x -> C) id3 f = \a => \b => f (a ** b) id4 : ((x:A) -> B x -> C) -> ((x:A ** B x) -> C) id4 f = \p => f (getWitness p) (getProof p)
Тела функций те же самые, просто операции с туплами поменялись на операции с зависимыми парами. Что же нам говорят типы? Что мы доказали следующее утверждение:
((∃x:A . B(x)) => C) == (∀x:A . (B(x) => C))
Это то, что позволяет в языках вроде хаскеля и окамла записывать экзистенциальные типы, обходясь без ключевого слова exists, а лишь квантором всеобщности forall.
Еще один морфизм на ту же тему:
id5: (x:A ** (B x -> C)) -> (((x:A) -> B x) -> C) id5 p = \f => (getProof p) (f (getWitness p))
Он показывает, что
(∃x:A . (B(x) => C)) => ((∀x:A . B(x)) => C)
Говорят, что в обратную сторону тоже верно, но у меня такую функцию построить не получилось.
![[identity profile]](https://www.dreamwidth.org/img/silk/identity/openid.png){kind=small}
no subject
Date: 2013-01-22 10:27 am (UTC)no subject
Date: 2013-01-22 11:02 am (UTC)1. Понятно, но это относится к изначальной задаче (эквивалентность (∃x:A . (B(x) => C)) и ((∀x:A . B(x)) => C)).
Я думал вы имеете ввиду построение функции (C => A) как отдельную задачу, тогда не имеет значение какая именно функция, но лишь ее существование.
2. Насчет изоморфизмов: задача доказательства эквивалентности типов и задача доказательства эквивалентности задач доказательства населенности типов - это разные вещи.
Тут второе (по Карри-Говарду): т.е. доказать, что из того что тип Т1 населен выводится что Т2 тоже населен. Пример Bool и Int - справились без изоморфизма:
f1 : Bool => Int
f1 _ = 1
f2 : Int => Bool
f1 _ = true
3. Для доказательства эквивалентности типов существование обратной функции не обязательно, пример тип целых и тип рациональных - мы знаем что они эквивалентны. Допустим то, что с целых в рациональные мы уже нашли функцию f1, а с рациональных в целые возьмем таким образом:
f2 : Q => Z
f2 x = [x] -- [_] - дробная часть.
Эта функция не имеет обратной, но хорошо вписывается в доказательство: из f1 и f2 получаем эквивалентность Q и Z.
no subject
Date: 2013-01-22 11:18 am (UTC)no subject
Date: 2013-01-22 12:11 pm (UTC)Определение функции для целой части не имеет значения. Я имел ввиду теорему Кантора — Бернштейна (http://ru.wikipedia.org/wiki/%D0%A2%D0%B5%D0%BE%D1%80%D0%B5%D0%BC%D0%B0_%D0%9A%D0%B0%D0%BD%D1%82%D0%BE%D1%80%D0%B0_%E2%80%94_%D0%91%D0%B5%D1%80%D0%BD%D1%88%D1%82%D0%B5%D0%B9%D0%BD%D0%B0), которая для доказательства эквивалентности множеств оперирует инъекциями, а не биекциями.
no subject
Date: 2013-01-22 12:25 pm (UTC)Инъекции тут я тоже не вижу. f2 2.5 и f2 2.4 отобразятся в один элемент, такая функция не инъективна.
Опять же, применимость этой теоремы к типам, а не множествам, вызывает большие сомнения.
no subject
Date: 2013-01-22 12:38 pm (UTC)f3 : Z => Q
f3 x = x (грязно, но думаю все ясно)
Насчет применимости теории множеств к типам, согласен, есть скользкие моменты, но в данной ситуации все в порядке.
no subject
Date: 2013-01-22 01:30 pm (UTC)И ваше определение эквивалентности типов я так и не увидел пока.
no subject
Date: 2013-01-22 01:51 pm (UTC)2.То определение эквивалентности типов не мое, а аналог эквивалентности высказываний: из населенности одного типа следует населенность другого и наоборот, никаких изоморфизмов и близко нет. (обратитесь еще раз к п.2 http://thedeemon.livejournal.com/59265.html?thread=970369#t970369)
no subject
Date: 2013-01-22 01:59 pm (UTC)2. Я пока не понял, как населенность типов связана с их эквивалентностью. Населенность меня не особо интересует, мне же нужна именно эквивалентность типов. Ее определения я в упор не вижу у вас.
no subject
Date: 2013-01-22 02:06 pm (UTC)2. Два высказывание эквивалентны (A <=> B), если из правдивости одного выводится правдивость другого (A => B), и наоборот (A <= B). А теперь через соответствие Карри-Говарда переведите все это в теорию типов.
no subject
Date: 2013-01-22 02:24 pm (UTC)2. Занятно, получается, что для эквивалентности утверждений изоморфизм не требуется, но эквивалентность утверждений не дает эквивалентности типов тогда.
no subject
Date: 2013-01-22 02:28 pm (UTC)2. Эквивалентность утверждений это и есть эквивалентность типов (изоморфизм Карри-Говарда)
no subject
Date: 2013-01-22 02:57 pm (UTC)2. Эдак у вас все непустые типы окажутся эквивалентными. Плохое какое-то определение, негодное.
no subject
Date: 2013-01-22 03:17 pm (UTC)2. Определение очень даже хорошее и часто используемое.
no subject
Date: 2013-01-22 03:39 pm (UTC)2. Где, например?
no subject
Date: 2013-01-22 03:54 pm (UTC)2. В стандартной библиотеке Агда есть такой пустой тип:
data ⊥ : Set where -- нет конструкторов
⊥-elim : ∀ {w} {Whatever : Set w} → ⊥ → Whatever
⊥-elim ()
а функция ⊥-elim даст вам терм любого типа, если вы ей предоставите терм типа ⊥.
В Агда реализована через абсурд паттерн, в Coq по-другому, в Идрис думаю тоже есть.
Я ее использовал тут http://starosud.blogspot.com/2012/09/agda.html
no subject
Date: 2013-01-22 04:22 pm (UTC)no subject
Date: 2013-01-22 05:00 pm (UTC)no subject
Date: 2013-01-22 05:12 pm (UTC)no subject
Date: 2013-01-22 05:20 pm (UTC)*(надо НЕ большими буквами выделять)
> Эдак у вас все непустые типы окажутся эквивалентными
не окажутся, невозможно построить для любых A, B терм типа A => B
no subject
Date: 2013-01-22 05:54 pm (UTC)no subject
Date: 2013-01-22 06:27 pm (UTC)no subject
Date: 2013-01-22 06:50 pm (UTC)no subject
Date: 2013-01-22 08:09 pm (UTC)А если вы будете, доказывая эквивалентность, искать именно изоморфизм, то вам и Идрис НЕ нужен.
Поймите, когда вы говорите о изоморфизме Карри-Говарда и пишете (A <=> B), то другие видят просто две имликации (A -> B) и (B -> A), без каких либо взаимно-однозначных отображений, и я же уже упоминал о proof irrelevance - эта фраза занимает не последнее место в данной области.
Или если хотите и писать на Идрис, и использовать свою эквивалентность, то делайте это как-то так хотя бы:
Bijection : {A B : Set} (f : A → B) → Set
Bijection {A} {B} f = ∀ b → Σ[ a ∶ A ] f a ≡ b
record _<=>_ (A : Set) (B : Set) : Set where
constructor isomorphism
field
f₁ : A → B
f₂ : B → A
p₁ : Bijection f₁
p₂ : Bijection f₂
f : ∀ A B → A <=> B
f = _
и тогда ни у кого не будет лишних вопросов.
no subject
Date: 2013-01-22 12:50 pm (UTC)