Аксиома выбора это теорема

[thedeemon]

В теории типов, конечно. Сегодня в нашем тавтологическом кружке для самых маленьких азы зависимых типов мимоходом. Аксиома выбора может быть сформулирована по-разному, например так: для любого семейства непустых множеств A существует функция выбора f, определённая на A. Берем мы кучу непустых множеств, вводим индексацию, т.е. каждое множество из этой кучи соотносим с элементом из некоторого множества А, например, числом; получили семейство множеств. Для конечного набора множеств используем конечное множество индексов А, для счетного множества множеств - счетное множество индексов, например A=Nat, можем даже взять континуум разных множеств и адресовать их вещественными числами, так у нас в семействе даже будет множество с индексом Пи. Сами множества в семействе могут быть очень разной природы. Перейдя от множеств к типам, мы получаем семейство типов, индексированное типом А, т.е. для каждого х из А у нас будет тип B_x, для разных х тип может быть разным, и собрание всех этих B_x будет нашим семейством типов, зависимым типом. Исходное семейство множеств мы можем представить бинарным отношением R(x,y), где x из А, а y из B_x. Факт того, что это семейтсво непустых множеств, можно выразить требованием для R быть left-total: для каждого х из А обязан существовать хотя бы один y из B_x, для которых выполнено отношение R(x,y). Тогда из наличия такого вот отношения R следует существование функции f из А в B_x, которая для каждого х из А выбирает некоторый элемент y из множества B_x, для которого выполнено R(x,y). Это и есть аксиома выбора, и сейчас мы ее докажем конструктивно как теорему. Математически утверждение выглядит так:

(∀x:A . ∃y:B_x . R(x,y)) => (∃f : A -> B_x . ∀x:A . R(x, f x))

Запишем это утверждение и его доказательство на ЯП с зависимыми типами Idris. В соответствии с соответствием Карри-Говарда :), утверждения у нас превращаются в типы, а доказательства - в программы (термы). Поэтому представим отношение R типом, у которого будут два индекса x и y типов А и B_x. Так, например, если А=В=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 Харпера из Карнеги-Мелона, да попытался себе объяснить.