Аксиома выбора это теорема
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-04-17 09:39 pm (UTC)С другой стороны, я мог неправильно прочитать то, что написано в посте, и тогда окажется, что в конкретном описанном случае (учитывая какие-то изложенные гипотезы) аксиома выбора может быть выведена как теорема.
(сильно не вникал в пост, голова другим занята.)
no subject
Date: 2013-04-17 10:16 pm (UTC)Но если вы выводите её как теорему, значит, она требуется, верно?
Мне в принципе-то интересно, но я слишком уверен в ответе. В смысле, я и раньше подозревал, что зависимые типы почему-то только в булевой логике существуют; а тут ещё бац - и аксиома выбора.
no subject
Date: 2013-04-17 10:22 pm (UTC)Мне тоже интересно, поэтому займусь в пределах пары недель, результат опубликую.
no subject
Date: 2013-04-17 10:37 pm (UTC)no subject
Date: 2013-04-18 12:26 pm (UTC)В чятике #coq объяснили, что такое возникает из-за того, что у нас тут не "классическая логика", а "конструктивная", и "(∀x:A . ∃y:Bx . R(x,y))" -- доказательство, которое, если уж подано, значит было сконструировано -- был дан конкретный способ для любого x выбирать такое y, чтобы отношение R было удовлетворено. В классической логике предикат "существует" не содержит подобного доказательства (и, более того, способа построения y:Bx), оттуда и необходимость аксиомы выбора или её аналогов.
no subject
Date: 2013-04-18 02:28 pm (UTC)no subject
Date: 2013-04-18 03:43 pm (UTC)http://www.cs.nott.ac.uk/~txa/g53cfr/
Посмотри вот эту лекцию —
http://www.cs.nott.ac.uk/~txa/g53cfr/l08.html/l08.html
no subject
Date: 2013-04-18 05:36 am (UTC)no subject
Date: 2013-04-18 04:06 am (UTC)Никак нет. Сериализация массива интов в JSON - тоже теорема, но зависимым типам она не требуется, она требуется конечным пользователям, которые эту теорему в виде бинарника запускают у себя.
no subject
Date: 2013-04-18 05:35 am (UTC)Я понимаю, что ты хотел сказать.
Но терминологически не верно.
Если она выводится, то требуй или не требуй — она есть.
А вот если она независима от остального, тогда уже можно её потребовать или не потребовать.