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

Posted

技术标签:

【中文标题】如何编码 Haskell/函数式编程中的选择公理?【英文标题】:How to encode the axiom of choice in Haskell/Functional programming? 【发布时间】: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 分配了一个(依赖)对,其第一个组件yA 的一个元素,第二个组件是第一个确实满足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

【讨论】:

以上是关于如何编码 Haskell/函数式编程中的选择公理?的主要内容,如果未能解决你的问题,请参考以下文章

Matrix技术分享| Haskell与函数式编程简介

JI workshop |前方高能计算机语言中的清流——Haskell和函数式编程

活动预告Haskell与函数式编程

轻松一下: 一些黑Haskell语言的漫画

将“为啥函数式编程很重要”翻译成 Haskell

惯用的 Haskell 中如何实现动态规划算法?