Coq 决策图多值函数

Question

我正在尝试完成某件事，但陷入困境。

首先，我的工作基于列表决策图。这表示一个多值输入二进制输出函数。

这里，假设我们有自然数作为输入值，最大值为 p。

我们通过测试一个值是否满足该函数并计算其余因子来定义该函数的香农展开式。 所以这个函数要求第一个变量的输入为0。它使用文字测试 0 是否被接受，如果是，则将第一个变量设置为 0。否则，它将继续到下一个值，即 1。

对于这样的函数，我们定义了一个DAG结构。这与 BDD 非常相似。我们暂时保持简单。

   Inductive ldd := 
      | Vertex (v : variable) (n : nat) (down_edge: ldd) (right_edge: ldd)
      | Leaf (val: Prop).
   Record ldd_var := Var { var_car : nat }.

这代表以下函数。 因此，在一个顶点中，我们有一个变量 (v)、一个标签 (n) 和两个直接子节点。 为了简单起见，我省略了一个重要因素，即 LDD 的右边缘必须具有相同的深度才能保持规范。此外，右子节点可能永远不会是真正的终端顶点，而下子节点可能永远不会是假终端顶点。

现在，我为这个 LDD 创建一个上下文。我们将变量绑定到 nat，如下所示。

  Definition var_bind : Type := ldd_var -> nat.
  Definition eq_bind (vb1 vb2 : var_bind) : Prop := 
      ∀ (v : ldd_var), vb1 v = vb2 v.

然后我们可以按如下方式限制该变量的值。

  Definition update (vb : var_bind) (v : ldd_var) (n : nat) : var_bind :=
      λ x : ldd_var, if eq_dec v x then n else vb x.

最后，我们将LDD表示的原始函数表示为

  Definition fun_inclusive := var_bind → bool.

要评估此功能，

  Definition eval_fun_inclusive (fi : fun_inclusive) (vb : var_bind) := fi vb.

但是现在，我想创建一个可以从 LDD 中提取的函数的构造/类型。需要这样做，以便我们可以测试 LDD 是否正确表示函数。例如，如果我们跟随 LDD 中的下降沿，我们就限制（即更新）具有值的变量。因此，我们需要有一个定义来表示这个选择，并且我们可以证明一个引理：选择这条路径等于将实函数限制为该值。 （参见香农展开）

最后，我想和 var_bind 一起，将其解释为 fun_inclusive 类型。

有人可以帮助我吗？我正在寻找如何处理这个问题的想法。我遇到的真正问题是，我们需要表示这个输入有 p 的最大值，它是一个 n 元函数，并且我们需要能够证明香农展开式的选择等于LDD中的选择。

Answer 1

我正在寻找如何处理这个问题的想法。

非常一般：我首先为这些函数定义一个抽象语法（即不直接使用 Coq 函数，或者你必须使用元 coq 来推理实现）直到评估器或求解器（等等）；然后我会定义同类函数的 LDD 编码，相应地达到评估器或求解器；最后，需要证明双方在任何级别上的等价性。认为使用函数作为规范的部分，使用LDD作为实现的部分，等价性是实现正确性的证明。

我遇到的真正问题是，我们需要表示此输入有 p 的最大值 [...]

您所问的问题已经很重要了（已经有很多代码了），因此，只要您有一些清晰的一般路径，（对于SO）针对最小示例提出单独且集中的编码问题可能更合适。 （更重要的是，因为你的函数不仅仅是布尔函数，而且你描绘的“有根香农展开”的定义并不完全精确，或者我无法完全解析它。）