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

Question

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

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

有没有一个能让库克完成转身？如果没有，你能更具体地解释为什么这是不可能的吗？

Answer 1

问题的答案在很大程度上取决于您希望在Coq中定义的函数计算在哪里。通常，使用例如步进索引对Coq中的任意部分函数进行编码是没有问题的，参见McBride的"；图灵完备，完全自由"；了解更多详细信息。但是，您将只能在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内部偏函数的可能性，使其成为转换的一部分，会自动导致理论本身是不可判定的(证明助手可能无法返回类型检查结果(。