3

这里我的意思是公理，我们可以Axiom在 Coq Gallina 中使用关键字来定义，而不是通过传递给 Coq 的命令行参数。

我知道一些公理使 Coq 不一致。然而，AFAIK 他们并没有使 Coq Turing 完整。在我粗略的理解中，这是因为它们不提供任何额外的计算行为。

有没有一个让 Coq 变得完整？如果不是，您能否更具体地解释为什么这是不可能的？

4

1 回答 1

6

您的问题的答案很大程度上取决于您希望在 Coq 中定义的函数在哪里计算。一般来说，在 Coq 中使用例如步进索引对任意部分函数进行编码是没有问题的，有关更多详细信息，请参阅 Mc Bride 的“图灵完备性，完全免费”。但是您只能在 Coq 中将这些函数评估到指定的有限界。

如果目标是编写可以使用任意递归并在 Coq 之外运行的经过形式验证的程序，那么您不需要公理，您可以使用该Extraction机制及其证明擦除语义，如下面的无界 while 示例所示环形：

Inductive Loop : Prop := Wrap : Loop -> Loop.
Notation next := (fun l => match l with Wrap l' => l' end).

Definition while {A : Type} (f : A -> A * bool) : Loop -> A -> A :=
  fix aux (l : Loop) (a : A) {struct l} :=
    let '(x, b) := f a in
    if b then aux (next l) x else x.

Require Extraction.
Recursive Extraction while.

提取结果：

type bool =
| True
| False

type ('a, 'b) prod =
| Pair of 'a * 'b

(** val while0 : ('a1 -> ('a1, bool) prod) -> 'a1 -> 'a1 **)

let rec while0 f x =
  let Pair (x0, b) = f x in (match b with
                             | True -> while0 f x0
                             | False -> x0)

请注意，函数 while 需要 Coq 中的终止证明，一旦转换为 ocaml，该终止证明就会被删除。

最后，正如您所解释的，如果您希望部分函数的评估留在 Coq 中，则需要扩展 Coq 的计算缩减机制。目前没有提供此功能的通用机制（即使有一个 coq 增强提案来添加重写规则）。可能会滥用定义性 UIP来评估部分功能。在所有情况下，在 Coq 中添加对部分函数求值的可能性，使其成为转换的一部分，自动导致理论本身因为不可判定（证明助手可能无法返回类型检查结果）。

于 2021-07-08T06:31:04.157 回答