coq - 任何额外的公理都能使 Coq Turing 完备吗？

Question

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

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

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

Answer 1

您的问题的答案在很大程度上取决于您希望在 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 中添加评估部分函数的可能性，使其成为转换的一部分，自动蕴含理论本身，因为它是不可判定的(证明助手可能无法返回类型检查结果)。