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

> {-# LANGUAGE RankNTypes #-}

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

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

> 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

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

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


functional-programming choice haskell agda curry-howard
person PyRulez    schedule 06.12.2015    source источник
comment
Проголосовали против на том основании, что этот вопрос не требует каких-либо исследовательских усилий: поиск в Google аксиомы выбора agda дает довольно много дискуссий о том, как это сделать.   -  person Daniel Wagner    schedule 06.12.2015
comment
@DanielWagner Если на stackexchange ранее не обсуждалась эта тема, то она актуальна независимо от того, что еще вы можете найти в Google. Об этом много раз писали основатели stackexchange. Вся философия заключается в том, чтобы быть тем ресурсом, который будущие люди находят при поиске в Google.   -  person Nick Alger    schedule 06.12.2015
comment
@NickAlger Да; по этой причине я не голосовал (и не буду) голосовать за закрытие вопроса, что является действием, которое следует предпринять в отношении вещей, не относящихся к теме. (Я думаю, что вполне разумно, что подсчет вопросов и ответов и окончательный подсчет голосов означают разные вещи.)   -  person Daniel Wagner    schedule 06.12.2015
comment
Версия аксиомы, которая применяется к индексированным множествам, или мы пытаемся рассуждать даже о несчетных множествах?   -  person Davislor    schedule 06.12.2015

Ответы (1)


arrow_upward
3
arrow_downward

Это всего лишь намек.

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

Если для каждого 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
person chi    schedule 06.12.2015