Аксиома выбора это теорема
Apr. 17th, 2013 08:09 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
thedeemonВ теории типов, конечно. Сегодня в нашем тавтологическом кружке для самых маленьких азы зависимых типов мимоходом. Аксиома выбора может быть сформулирована по-разному, например так: для любого семейства непустых множеств A существует функция выбора f, определённая на A. Берем мы кучу непустых множеств, вводим индексацию, т.е. каждое множество из этой кучи соотносим с элементом из некоторого множества А, например, числом; получили семейство множеств. Для конечного набора множеств используем конечное множество индексов А, для счетного множества множеств - счетное множество индексов, например A=Nat, можем даже взять континуум разных множеств и адресовать их вещественными числами, так у нас в семействе даже будет множество с индексом Пи. Сами множества в семействе могут быть очень разной природы. Перейдя от множеств к типам, мы получаем семейство типов, индексированное типом А, т.е. для каждого х из А у нас будет тип Bx, для разных х тип может быть разным, и собрание всех этих Bx будет нашим семейством типов, зависимым типом. Исходное семейство множеств мы можем представить бинарным отношением R(x,y), где x из А, а y из Bx. Факт того, что это семейтсво непустых множеств, можно выразить требованием для R быть left-total: для каждого х из А обязан существовать хотя бы один y из Bx, для которых выполнено отношение R(x,y). Тогда из наличия такого вот отношения R следует существование функции f из А в Bx, которая для каждого х из А выбирает некоторый элемент y из множества Bx, для которого выполнено R(x,y). Это и есть аксиома выбора, и сейчас мы ее докажем конструктивно как теорему. Математически утверждение выглядит так:
(∀x:A . ∃y:Bx . R(x,y)) => (∃f : A -> Bx . ∀x:A . R(x, f x))
Запишем это утверждение и его доказательство на ЯП с зависимыми типами Idris. В соответствии с соответствием Карри-Говарда :), утверждения у нас превращаются в типы, а доказательства - в программы (термы). Поэтому представим отношение R типом, у которого будут два индекса x и y типов А и Bx. Так, например, если А=В=Nat, R 2 3 - это тип, он может быть как населен, так и ненаселен. Если он населен, т.е. существуют значения типа R 2 3, это будет означать, что для 2 и 3 отношение R выполнено, иначе - нет.
Утверждение нашей "аксиомы" выше имеет вид импликации, поэтому оно превратится в тип функции. На входе этой функции будет доказательство левототальности (как это по-русски?) отношения R, а на выходе - конструктивное доказательство существования функции выбора f и того факта, что она выбирает значения, для которых R выполнено. Логическая связка ∀x:A . P(x) в теории типов превращается в так называемый пи-тип - тип функции, у которой тип результата может зависеть от значения аргумента. Доказательство такого утверждения, терм такого типа - это лямбда. Логическая связка ∃x:A . P(x) превращается в так называемый сигма-тип, зависимую пару - тупл, в котором тип второго элемента может зависеть от значения первого элемента. Доказательством такого утверждения, термом такого типа служит пара из двух значений, где первое значение влияет на тип второго. В Идрисе такая пара записывается (x : A ** P x). Две звездочки тут разделяют две половины тупла. Аналогами функций fst и snd извлечения первого и второго элементов служат функции getWitness и getProof. А вот и весь текст программы с формулировкой и доказательством теоремы:
Конструкция using вводит определения, которые станут неявными аргументами для входящих в последующий блок определений. В первой строчке мы говорим, что А - некий тип, а В - тип, индексированный А, семейство типов. Вторая строчка: R - тип, индексированный двумя значениями тех типов, наше отношение. Третья строчка - прямой перевод математической нотации из формулировки выше на Идрис. Определяет тип функции, назовем ее М. И последняя строчка: тело функции М, доказательство теоремы. Получив на вход доказательство t факта тотальности R, мы используем его чтобы из произвольного х:А получить пару из y : B x и R x y. Если из этой пары брать только первую часть, получим функцию из х:А в y : B x, т.е. как раз искомую f. Если же брать вторую часть той пары, получим значение-доказательство R x (f x). Таким образом, мы построили функцию выбора и построили доказательство того, что она выбирает что надо. Конечно, все это в некотором роде тавтология, т.к. доказательство лишь пользуется тем, что уже заложено в условии тотальности R, функция выбора уже неявно там содержалась, мы лишь выделили ее в явном виде. Но это демонстрирует важное отличие теории типов от чистой логики: в теории типов доказательства являются существенными математическими объектами, с которыми ведутся операции и которые что-то производят. В логике объектами служат лишь утверждения, а доказательства их не являются математическим объектом. Мопед не мой, я лишь перевел на Идрис подслушанное у Роберта existential_type Харпера из Карнеги-Мелона, да попытался себе объяснить.
(∀x:A . ∃y:Bx . R(x,y)) => (∃f : A -> Bx . ∀x:A . R(x, f x))
Запишем это утверждение и его доказательство на ЯП с зависимыми типами Idris. В соответствии с соответствием Карри-Говарда :), утверждения у нас превращаются в типы, а доказательства - в программы (термы). Поэтому представим отношение R типом, у которого будут два индекса x и y типов А и Bx. Так, например, если А=В=Nat, R 2 3 - это тип, он может быть как населен, так и ненаселен. Если он населен, т.е. существуют значения типа R 2 3, это будет означать, что для 2 и 3 отношение R выполнено, иначе - нет.
Утверждение нашей "аксиомы" выше имеет вид импликации, поэтому оно превратится в тип функции. На входе этой функции будет доказательство левототальности (как это по-русски?) отношения R, а на выходе - конструктивное доказательство существования функции выбора f и того факта, что она выбирает значения, для которых R выполнено. Логическая связка ∀x:A . P(x) в теории типов превращается в так называемый пи-тип - тип функции, у которой тип результата может зависеть от значения аргумента. Доказательство такого утверждения, терм такого типа - это лямбда. Логическая связка ∃x:A . P(x) превращается в так называемый сигма-тип, зависимую пару - тупл, в котором тип второго элемента может зависеть от значения первого элемента. Доказательством такого утверждения, термом такого типа служит пара из двух значений, где первое значение влияет на тип второго. В Идрисе такая пара записывается (x : A ** P x). Две звездочки тут разделяют две половины тупла. Аналогами функций fst и snd извлечения первого и второго элементов служат функции getWitness и getProof. А вот и весь текст программы с формулировкой и доказательством теоремы:
using (A : Type, B : A -> Type) R : (x:A) -> (y : B x) -> Type M : ((x:A) -> (y : B x ** R x y)) -> (f : (x:A) -> B x ** (x:A) -> R x (f x)) M t = (\x => getWitness (t x) ** \x => getProof (t x))
Конструкция using вводит определения, которые станут неявными аргументами для входящих в последующий блок определений. В первой строчке мы говорим, что А - некий тип, а В - тип, индексированный А, семейство типов. Вторая строчка: R - тип, индексированный двумя значениями тех типов, наше отношение. Третья строчка - прямой перевод математической нотации из формулировки выше на Идрис. Определяет тип функции, назовем ее М. И последняя строчка: тело функции М, доказательство теоремы. Получив на вход доказательство t факта тотальности R, мы используем его чтобы из произвольного х:А получить пару из y : B x и R x y. Если из этой пары брать только первую часть, получим функцию из х:А в y : B x, т.е. как раз искомую f. Если же брать вторую часть той пары, получим значение-доказательство R x (f x). Таким образом, мы построили функцию выбора и построили доказательство того, что она выбирает что надо. Конечно, все это в некотором роде тавтология, т.к. доказательство лишь пользуется тем, что уже заложено в условии тотальности R, функция выбора уже неявно там содержалась, мы лишь выделили ее в явном виде. Но это демонстрирует важное отличие теории типов от чистой логики: в теории типов доказательства являются существенными математическими объектами, с которыми ведутся операции и которые что-то производят. В логике объектами служат лишь утверждения, а доказательства их не являются математическим объектом. Мопед не мой, я лишь перевел на Идрис подслушанное у Роберта existential_type Харпера из Карнеги-Мелона, да попытался себе объяснить.
![[identity profile]](https://www.dreamwidth.org/img/silk/identity/openid.png){kind=small}
no subject
Date: 2013-05-28 04:05 pm (UTC)по-моему здесь путаница с тем, что такое A, что такое семейство множеств и кто кого индексирует.
Первая фраза говорит о семействе множеств A. Стало быть, A : X → Set
Вторая фраза говорит о соотнесении элементов A ("каждое множество из этой кучи") с ... элементами множества A (к тому же, "например, числом")?
По-моему, аксиома выбора говорит о следующем:
B : A → Set -- суръекция, ибо B x полностью определена индексом A
axiom : ∀ {a} → Σ (f : {a : A} → B a → A) (λ b → B (f b) ≡ B a) -- аксиома говорит о том, что суръекцию можно обратить; функция f обращает суръекцию, а существование типа B (f b) ≡ B a говорит о том, как именно суръекция обращена
(я конечно кривенько написал эту самую строчку - мысль та, что для любых A существует функция f от (B a) в A, которая given a value of type (B a) строит значение y такое, что B y ≡ B a)
Остача доказательства не противоречит вышесказанному, потому что R a (f a) следует из B (f b) ≡ B a.
(Ага, а теперь это всё умозрительное осталось загрузить в агду и увидеть, в чём я заблуждаюсь :)
no subject
Date: 2013-05-28 04:19 pm (UTC)В : А -> Set ни в коем случае не суръекция. Ведь А может быть unit или Bool, а справа от стрелки тут все множество типов (кроме вселенных более высоких индексов).
no subject
Date: 2013-05-28 04:23 pm (UTC)типа как вот здесь: http://en.wikipedia.org/wiki/Axiom_of_choice суръекцией является (i : I) → (S i). С помощью i выбирается одна точка среди всех S, а именно одно множество из семейства S_i.
no subject
Date: 2013-05-28 04:41 pm (UTC)no subject
Date: 2013-05-28 04:42 pm (UTC)Аксиома выбора говорит, что существует функция выбора, и мы ее доказываем, произведя на свет как раз такую f : (a:A) -> B a.
> для любых A существует функция f от (B a) в A, которая given a value of type (B a) строит значение y такое, что B y ≡ B a)
Это что-то сложное, затрагивающее равенство типов. Оно у нас определено вообще? Ведь B y - это тип.
Давайте сперва на примере отточим. Пусть А = Bool, B : Bool -> Set, B a = if a then Nat else Bool.
no subject
Date: 2013-05-28 04:50 pm (UTC)с тараканами разобраться :)
То, что "существует функция выбора", понятно. Не понятно, кого из чего она должна выбирать?
Ну на пальцах так: есть функция f из A в B; какие-то значения A отображаются в значения B, выбранные другими значениями A. Тогда аксиома выбора говорит, что эту функцию можно обратить таким образом, что эти значения отображаются функцией f обратно так, что f . f-1 . f = f
По-моему, здесь функцией выбора является f-1, ибо она выбирает "правильные" значения A - она умеет "обратить" функцию f так, что из "дубликатов" значений A, которые отображаются в одинаковое B, выбирается какой-то один - не важно, какой.
Более того, поскольку речь о суръекции, то ещё и f-1 . f . f-1 = f-1
Вот. На пальцах вроде всё понятно. Но если функцией выбора является f-1 : (a : A) → (B a), то как выглядит суръекция f? f : (B a) → (a : A) ? Стгьянно.
no subject
Date: 2013-05-28 05:17 pm (UTC)More explicitly, it states that for every indexed family S_i (i : I) of nonempty sets there exists an indexed family x_i of elements such that x_i in S_i for every i in I.
Т.е. у нас есть множество индексов I, для каждого индекса дано множество S_i.
S : I -> Type
Аксиома говорит, что для каждого такого набора непустых множеств S существует набор таких x_i, что для каждого i : I, x_i in S_i. Этот набор мы можем представить в виде функции: существует функция, которая для каждого i : I даст нам x_i типа S_i.
Такая функция f : (i:I) -> S i и есть функция выбора.
Можно, конечно, говорить о такой же по смыслу функции, но берущей в качестве аргумента не индекс i:I, а соответствующее ему множество S_i, из которого она будет выбирать ответ, но при ее записи на Агде или Идрисе нам все равно придется сделать i аргументом, чтобы можно было S_i как-то обозначить.
no subject
Date: 2013-05-28 06:24 pm (UTC)Но ваш аргумент убедителен. Я понял, в каком смысле (i:I)->S i - функция выбора. С т.з. f . f-1 . f = f и одновременно f-1 . f . f-1 = f-1 может также оказаться, что доказывать всё равно в какую сторону.
no subject
Date: 2013-05-28 06:31 pm (UTC)no subject
Date: 2013-05-28 06:34 pm (UTC)f : Either A B → Bool
f (Left _) = false
f (Right _) = true
аксиома выбора - это "копродукт можно паттерн-матчить"
no subject
Date: 2013-05-28 06:52 pm (UTC)no subject
Date: 2013-05-28 07:38 pm (UTC)ну да бог с ним. primary goal достигнута - в каком смысле искомая функция есть ф-ция выбора стало понятно.