任何额外的公理可以使 Coq Turing 完整吗？

Question

这里我的意思是公理是我们可以用AxiomCoq Gallina 中的关键字定义的东西，而不是传递给 Coq 的命令行参数。

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

有没有一种可以使 Coq 转动完成的？如果没有，您能否更具体地解释为什么不可能？

Answer 1

您问题的答案很大程度上取决于您希望 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.

提取结果：

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.

请注意，函数 while 需要 Coq 中的终止证明，一旦它变成 ocaml 就会被擦除。

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