Coq中具有非確定性組件的數據結構

我試圖在Haskell中經常使用的Coq中對非確定性（比MonadPlus和常用列表天真少）進行建模的不太樸素的monadic編碼;例如列表的編碼看起來像Coq中具有非確定性組件的數據結構

data List m a = Nil | Cons (m a) (m (List m a))

而在Coq中的相應定義如下所示。

Inductive List (M: Type -> Type) (A: Type) := 
    Nil: List M A 
| Cons : M A -> M (List M A) -> List M A.

然而，這種定義在勒柯克是不允許的，因爲感應數據類型「嚴格正」 -condition的。

我不確定我是否希望針對Coq特定的答案或Haskell中的另一個實現，我可以在Coq中正式化，但我很樂意閱讀有關如何解決此問題的任何建議。

來源

2016-04-05 ichistmeinname

你可能尋找['Freer']（http://okmij.org/ ftp/Haskell/extensible/more.pdf）單元和那裏的'NDet'效果。一切都是嚴格肯定的，這種表述甚至會給你提供[確定選擇]的非確定性（http://okmij.org/ftp/papers/LogicT.pdf）。我[實現]（https://github.com/effectfully/Eff/blob/master/Simple/Effect/NonDet.agda）在Agda中，但由於Agda處理宇宙多態性的方式，代碼非常糟糕。 – user3237465

承諾的選擇（或FLP社區喜歡稱之爲呼叫時間選擇）正是我想用Coq正式確定的！我目前的來源是[另一篇論文]（http://homes.soic.indiana.edu/ccshan/rational/lazy-nondet.pdf），它明確地建模了與monad的非確定性的類FLP語義。由於我仍在試圖找出最適合在Coq中使用哪種模型，所以我一定會看看Oleg的「Freer」monad的代表性 - 據我所知，我已經閱讀過論文（針對不同的背景）。所以感謝提醒！ – ichistmeinname

請參閱Chlipala's "Certified Programming with Dependent Types"。如果您有Definition Id T := T -> T，則List Id可能會產生非終止條款。我認爲你也可以通過Definition Not T := T -> False推導出一個矛盾，特別是如果你放棄Nil的構造函數並接受排除中等規律。

如果有某種方式將M註釋爲僅在正位置使用它的參數，那將會很不錯。我認爲安德烈亞斯阿貝爾可能在這方面做了一些工作。

無論如何，如果你願意限制你的數據類型的只是一點點，你可以使用：

Fixpoint SizedList M A (n : nat) : Type := 
    match n with 
    | 0 => unit 
    | S m => option (M A * M (SizedList M A m)) 
    end. 

Definition List M A := { n : nat & SizedList M A n }.

來源

2016-04-05 10:50:41 jbapple

Abel在這方面的工作是在[MiniAgda]（http://www2.tcs.ifi.lmu.de/~abel/miniagda/）中實施的。 – gallais

感謝您的快速回答;不幸的是，我忘了寫我仍然是Coq的初學者。你能否詳細闡述一下這種編碼背後的想法？這是用'existT'來定義'List M A'類型值的正確方法嗎？這種結構對我來說是新的，並且以某種方式使用谷歌搜索並沒有幫助。 – ichistmeinname

Coq中具有非確定性組件的數據結構

回答

相關問題