Как кодировать аксиому выбора в Haskell/ Функциональное программирование?

Question

> {-# LANGUAGE RankNTypes #-}

Мне было интересно, есть ли способ представить аксиому выбора в Haskell и / или некотором другом функциональном языке программирования.

Как мы знаем, false представлен типом без значений (Void в хаскеле).

> import Data.Void

Мы можем представить отрицание так

> type Not a = a -> Void

Мы можем выразить закон исключенного среднего для типа a вот так

> type LEM a = Either a (a -> Void)

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

> type Constructive a = (forall r. LEM r) -> a

Мы можем, например, сделать устранение двойного отрицания в нем

> doubleneg :: Constructive (((a -> Void) -> Void) -> a)
> doubleneg = \lem nna -> either id (absurd . nna) lem

У нас также может быть монада, где закон исключенного среднего не работает

> type AntiConstructive a = ((forall r. LEM r) -> Void) -> a

---

Теперь вопрос в том, как мы можем создать тип, который представляет аксиому выбора. Аксиома выбора говорит о множествах множеств. Это подразумевает, что нам понадобятся типы типов или что-то в этом роде. Есть ли что-то эквивалентное аксиоме выбора, которую можно закодировать? (Если вы можете закодировать отрицание, просто объедините его с законом исключенного среднего). Может быть, обман позволил бы нам иметь типы типов.

Примечание: в идеале, это должна быть версия аксиомы выбора, которая работает с теоремой Дьяконеску.

Answer 1

Это всего лишь подсказка.

Аксиома выбора может быть выражена как:

Если для каждого x : A есть y : B такой, что собственность P x y держит, то есть функция выбора f : A -> B такой, что для всех x : A у нас есть P x (f x),

Точнее

choice : {A B : Set} (P : A -> B -> Set) ->
   ((x : A) -> Σ B (λ y -> P x y)) ->
   Σ (A -> B) (λ f -> (x : A) -> P x (f x))
choice P h = ?

дано

data Σ (A : Set) (P : A -> Set) : Set where
  _,_ : (x : A) -> P x -> Σ A P

Выше, choice действительно доказуемо. В самом деле, h назначает каждому x (зависимая) пара, чей первый компонент y является элементом A а второй компонент является доказательством того, что первый действительно удовлетворяет P x y, Вместо этого f в дипломной работе необходимо присвоить x только yбез каких-либо доказательств.

Как видите, получение функции выбора f от h это просто вопрос отбрасывания компонента доказательства в паре.

Нет необходимости расширять Agda с помощью LEM или любой другой аксиомы, чтобы доказать это. Приведенное выше доказательство является полностью конструктивным.

Если мы использовали Coq, обратите внимание, что Coq запрещает удалять доказательства (такие как h : ... -> Prop) построить не доказательство (f), так что перевести это на Coq напрямую не получается. (Это необходимо для извлечения программы.) Однако, если мы избегаем Prop своего рода Coq и использовать Type напрямую, то вышеперечисленное можно перевести.

---

Вы можете использовать следующие прогнозы для этого упражнения:

pr1 : ∀ {A : Set} {P} -> Σ A P -> A
pr1 (x , _) = x

pr2 : ∀ {A : Set} {P} -> (p : Σ A P) -> P (pr1 p)
pr2 (_ , y) = y