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

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

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

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

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

解决方法

您问题的答案很大程度上取决于您希望 Coq 中定义的函数在哪里计算。一般来说，使用例如步进索引在 Coq 中编码任意部分函数是没有问题的，有关详细信息，请参阅 Mc Bride 的“Turing completeness,totally free”。 但是您只能在 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 的计算简化机制。目前没有提供此功能的通用机制（即使有针对 add rewriting rules 的 coq 增强建议）。可能会滥用 definitional UIP 来评估部分函数。在所有情况下，在 Coq 中添加对部分函数求值的可能性，使其成为转换的一部分，自动地意味着理论本身是不可判定的（证明助手可能无法返回类型检查结果）。