如何编码 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
分配了一个(依赖)对,其第一个组件y
是A
的一个元素,第二个组件是第一个确实满足P x y
的证明。相反,论文中的f
必须只分配给x
y
,无需任何证明。
如您所见,从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/函数式编程中的选择公理?的主要内容,如果未能解决你的问题,请参考以下文章