Coq 中具有非确定性组件的数据结构

Posted 2023-02-16

【中文标题】Coq 中具有非确定性组件的数据结构

【英文标题】：Data structures with nondeterministic components in Coq

【发布时间】：2016-04-05 09:24:18

【问题描述】：

我尝试在 Coq 中为 Haskell 中经常使用的非确定性（比 MonadPlus 和常见列表更简单）建模一个不那么幼稚的单子编码；例如列表的编码看起来像

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.

但是，这种定义在 Coq 中是不允许的，因为归纳数据类型的“严格肯定”条件。

我不确定我的目标是针对特定于 Coq 的答案还是在 Haskell 中可以在 Coq 中形式化的替代实现，但我很高兴阅读有关如何克服此问题的任何建议。

【问题讨论】：

您可能正在那里寻找Freer monads 和NDet 效果。一切都是积极的，这种表示甚至给你committed choice 的不确定性。我在 Agda 中 implemented，但由于 Agda 处理宇宙多态性的方式，代码很糟糕。

承诺选择（或 FLP 社区喜欢称之为调用时间的选择）正是我想用 Coq 形式化的内容！我目前的来源是another paper，它使用单子显式地建模了一个类似 FLP 的非确定性语义。由于我仍在尝试找出最适合在 Coq 中使用的模型，因此我肯定会使用 Oleg 的 Freer monads 来查看表示形式——据我记得，我已经阅读了纸（用于不同的上下文）。所以谢谢你的提醒！

【参考方案1】：

见Chlipala's "Certified Programming with Dependent Types"。如果您有Definition Id T := T -> T，那么List Id 可能会产生一个非终止项。我认为您也可以通过Definition Not T := T -> False 得出一个矛盾，特别是如果您放弃Nil 构造函数并接受排中定律。

如果有某种方法可以将 M 注释为仅在正位置使用其参数，那就太好了。我认为 Andreas Abel 可能在这方面做了一些工作。

无论如何，如果您愿意稍微限制您的数据类型，您可以使用：

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 .

【讨论】：

Abel 在这个方向上的工作在MiniAgda 中实现。

感谢您的快速回答；不幸的是，我忘了写我还是 Coq 的初学者。您能否详细说明一下这种编码背后的想法？用existT 定义List M A 类型的值是否正确？这种结构对我来说是新的，不知何故谷歌搜索没有帮助。