1 
> {-# 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

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

注意：理想情况下，它应该是适用于Diaconescu 定理的选择公理的一个版本。

4

1 回答 1

3

这只是一个提示。

选择公理可以表示为：

如果对于每个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只是丢弃对中的证明组件的问题。

没有必要用 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
于 2015-12-06T09:31:03.987 回答