如何编码 Haskell/函数式编程中的选择公理？答案

【问题标题】：How to encode the axiom of choice in Haskell/Functional programming?如何编码 Haskell/函数式编程中的选择公理？
【发布时间】：2016-03-10 20:39:56
【问题描述】：

> {-# LANGUAGE RankNTypes #-}

我想知道是否有一种方法可以在 haskell 和/或其他一些函数式编程语言中表示选择公理。

我们知道，false 由没有值的类型表示（Void in haskell）。

> import Data.Void

我们可以这样表示否定

> type Not a = a -> Void

我们可以像这样表达类型a的排中律

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

这意味着我们可以将建设性逻辑变成Reader monad

> 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

现在的问题是，我们如何创建一个表示选择公理的类型？选择公理是关于集合的集合。这意味着我们需要类型的类型或其他东西。是否有可以编码的选择公理等价？（如果您可以对否定进行编码，只需将其与排中律结合即可）。也许诡计可以让我们拥有类型的类型。

注意：理想情况下，它应该是与Diaconescu's theorem 一起使用的选择公理的一个版本。

【问题讨论】：

投了反对票，理由是这个问题没有显示任何研究工作：谷歌搜索“选择公理 agda”对如何做到这一点进行了很多讨论。
@DanielWagner 如果之前在 stackexchange 上没有关于这个话题的讨论，那么不管你在谷歌上还能找到什么，它都是主题。 stackexchange 的创始人已经写过很多次了。整个理念是成为未来人们在搜索谷歌时发现的资源。
@NickAlger 是的；出于这个原因，我没有（也不会）投票结束这个问题，这是对离题的事情采取的行动。（我认为问题的好投票数和接近投票数的含义不同是完全合理的。）
适用于索引集的公理版本，还是我们试图推理甚至不可数集？

【解决方案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必须只分配给xy，无需任何证明。

如您所见，从h 获得选择函数f 只是丢弃该对中的证明组件。

没有必要用 LEM 或任何其他公理扩展 Agda 来证明这一点。上述证明完全是建设性的。

如果我们使用 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

【讨论】：