如何在Haskell /函數式編程中對選擇的公理進行編碼？

> {-# LANGUAGE RankNTypes #-}

我想知道是否有方法來表示haskell和/或其他函數式編程語言中的選擇公理。如何在Haskell /函數式編程中對選擇的公理進行編碼？

正如我們所知，false由沒有值的類型表示（haskell中的Void）。

> 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一起使用的選擇公理的一個版本。

2015-12-06 PyRulez

Downvoted的理由是，這個問題並沒有表現出任何的研究工作：谷歌搜索「的選擇AGDA的公理」給人蠻很多關於如何做到這一點的討論。 –

@DanielWagner如果之前沒有關於這個話題的stackexchange的討論，那麼無論你在google上還能找到什麼，它都是話題。 stackexchange的創始人已經寫了很多次。整個理念就是成爲未來人在搜索谷歌時找到的資源。 –

@NickAlger是;出於這個原因，我沒有（也不會）投票結束這個問題，這是針對脫離主題的事情采取的行動。（我認爲對於問題善意投票計數和近距離投票計數意味着不同的事情是完全合理的。） –

這只是一個提示。

選擇公理可表示爲：

如果每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

2015-12-06 09:31:03 chi

回答