在Coq中形式化可计算性理论

Question

我试着 通过形式化教自己Coq 形式化 我熟悉的数学定理:停止问题的不可判定性 可计算性理论中的各种定理.

由于我对形式化计算模型的细节不感兴趣(例如,图灵机,注册机,lambda calculi等),我试图通过 "教授Coq Church-Turing论文",即假设Axioms表示Coq认为可计算的函数的属性(即,可定义的类型函数nat -> nat).

例如,如果我想告诉Coq有部分可计算函数的有效枚举,我可以说

Definition partial := nat -> nat -> option nat.
Axiom Phi : nat -> partial.

这里,部分可计算函数被认为是(总)可计算函数,给定第一个参数s,模拟s许多步骤的原始部分可计算函数的计算.我还可以添加其他Axioms,如Padding Lemma,我可能能够证明停止问题的不可判定性,以及可计算性理论中的其他一些定理.

我的第一个问题是我到目前为止是否走在正确的轨道上.难道不是我正在尝试做的事情显然不可能出现不完整现象或Coq类型系统的性质吗？

我的第二个问题是关于相对化.如果我试图在可计算性理论中证明更严肃的事情,我会考虑在oracles中进行计算.由于oracles经常被构造为部分二值函数的极限,所以似乎(至少天真地)使oracles具有类型是自然的nat -> bool.同时,为了使神谕变得不平凡,它们必须是不可计算的.考虑到这一点,具有类型的oracle是否nat -> bool有意义？

这是关于oracles的另一个问题:如果对于每个oracle,存在相对于该特定oracle的部分可计算函数的类型,那将是非常好的.我可以通过在Coq中利用依赖类型系统来做到这一点吗？这种可能性是否取决于上文所述的一些形式化神谕的选择？

编辑:上面的方法肯定不能正常工作,因为我需要一个额外的公理:

Axiom Phi_inverse: partial -> nat.

这应该不会成为预言真的.有没有像我上面描述的方法(我的意思是,那个不涉及计算模型形式化的方法)？

编辑:为了澄清我的意图,我编辑了上面的问题陈述.另外,为了呈现我想到的形式化的风格,我提出了一个不完整的证据,证明这里停止问题的不可解决性:

Require Import Arith.
Require Import Classical.
Definition ext_eq (A B : Set) (f g : A -> B) := forall (x : A), f x = g x.
Definition partial := nat -> nat -> option nat.
Axiom Phi : nat -> partial.
Axiom Phi_inverse : partial -> nat.
Axiom effective_enumeration :
  forall (f : partial) (e : nat),
    Phi e = f <-> Phi_inverse f = e.
Axiom modulus : partial -> nat -> nat.
Axiom persistence :
  forall (f : partial) n s,
    s >= modulus f n -> f s n = f (modulus f n) n.
Definition limit (f : partial) n := f (modulus f n) n.
Definition total (f : partial)
  := forall n, exists s, exists m, f s n = Some m.
Definition flip n := match n with O => 1 | S _ => 0 end.
Definition K e := exists n, limit (Phi e) e = Some n.
Theorem K_is_undecidable :
  ~ exists e,
      total (Phi e)
      /\ forall e', limit (Phi e) e' = Some 0 <-> ~K e'. 
Proof.
  intro.
  destruct H as [e].
  destruct H.
  pose proof (H0 (Phi_inverse (fun s e' =>
                                match (Phi e s e') with
                                  | Some n => Some (flip n)
                                  | None => None end))).
(* to be continued *)

Answer 1

首先，一些澄清：

Coq 认为可计算的函数（即 nat -> nat 类型的可定义函数）

严格来说，Coq 并不认为函数是可计算的。Coq 的逻辑断言可以定义某些函数，并且可以用它们做某些事情，但就 Coq 而言，任意函数都是黑匣子。特别是，假设不可计算函数的存在是一致的。

现在，回答实际问题。这是一个或多或少遵循 Atsby 答案的解决方案。我们将用 类型的 Coq 函数来表示图灵机函数nat -> nat -> option bool。这个想法是，第一个参数是输入，第二个参数是我们要运行的最大步数。输出是None如果我们未能产生答案，并且Some b计算终止并产生b答案。我冒昧地使用了 Ssreflect 来使代码更简单一些：

Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool.
Require Import Ssreflect.ssrnat Ssreflect.choice.

Section Halting.

(* [code f c] holds if [f] is representable by some
   Turing machine code [c]. Notice that we don't assume that
   [code] is computable, nor do we assume that all functions 
   [nat -> nat -> option bool] can be represented by some code, 
   which means that we don't rule out the existence of
   non-computable functions. *)
Variable code : (nat -> nat -> option bool) -> nat -> Prop.

(* We assume that we have a [decider] for the halting problem, with
   its specification given by [deciderP]. Specifically, when running
   on a number [m] that represents a pair [(c, n)], where [c] is the
   code for some Turing machine [f] and [n] some input for [f], we
   know that [decider m] will halt at some point, producing [true] iff
   [f] halts on input [n].

   This definition uses a few convenience features from Ssreflect to
   make our lives simpler, namely, the [pickle] function, that
   converts from [nat * nat] to [nat], and the implicit coercion from
   [option] to [bool] ([Some] is mapped to [true], [None] to [false]) *)
Variable decider : nat -> nat -> option bool.
Hypothesis deciderP :
  forall f c, code f c ->
  forall (n : nat),
     (forall s,
        match decider (pickle (c, n)) s with
        | Some true  => exists s', f n s'
        | Some false => forall s', negb (f n s')
        | None => True
        end) /\
     exists s, decider (pickle (c, n)) s.

(* Finally, we define the usual diagonal function, and postulate that
   it is representable by some code [f_code]. *)
Definition f (n : nat) s :=
  match decider (pickle (n, n)) s with
  | Some false => Some false
  | _ => None
  end.
Variable f_code : nat.
Hypothesis f_codeP : code f f_code.

(* The actual proof is straightforward (8 lines long). 
   I'm omitting it to avoid spoiling the fun. *)
Lemma pandora : False.
Proof. (* ... *) Qed.

End Halting.

综上所述，使用 Coq 函数来讨论 Halting 问题是完全合理的，而且结果也相当简单。请注意，上述定理根本不强制code与图灵机相关 - 例如，您可以将上述定理解释为预言机图灵机无法解决预言机图灵机的停机问题。最后，使这些结果彼此不同的是底层计算模型的形式化，这正是您想要避免的。

至于您尝试开始使用的模板，假设Phi存在并且具有逆已经导致矛盾。这是通常的对角论证：

Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool.
Require Import Ssreflect.ssrnat Ssreflect.choice.

Definition partial := nat -> nat -> option nat.
Axiom Phi : nat -> partial.
Axiom Phi_inverse : partial -> nat.
Axiom effective_enumeration :
  forall (f : partial) (e : nat),
    Phi e = f <-> Phi_inverse f = e.

Lemma pandora : False.
Proof.
pose f n (m : nat) :=
  if Phi n n n is Some p then None
  else Some 0.
pose f_code := Phi_inverse f.
move/effective_enumeration: (erefl f_code) => P.
move: (erefl (f f_code f_code)).
rewrite {1}/f P.
by case: (f _ _).
Qed.

问题是，尽管从外部我们知道 Coq 可定义函数与 是双射的nat，但我们无法在内部断言这一事实​​。断言无效code 关系的存在可以解决这个问题。

至于预言机，让预言机成为类型的函数nat -> bool确实有意义，但您需要确保这样做不会违反证明中的其他假设。例如，您可以假设所有nat -> nat函数都是可计算的，通过公理化您有一个像您的函数Phi，但这意味着您的预言机也是可计算的。使用上述关系code可以让您两全其美。

最后，至于相对化结果，这很大程度上取决于你想证明什么。例如，如果您只是想表明可以编写预言机上的某些函数，则可以编写一个参数函数，并在预言机具有某种行为时表明它具有某种属性，而不需要依赖类型。例如

Definition foo (oracle : nat -> bool) (n : nat) : bool :=
  (* some definition ... *).

Definition oracle_spec (oracle : nat -> bool) : Prop :=
  (* some definition ... *).

Lemma fooP oracle :
  oracle_spec oracle ->
  (* some property of [foo oracle]. *)

最后，这里有一个有趣的链接，讨论 Church 在依赖类型理论中的论文，您可能会觉得有趣：https ://existentialtype.wordpress.com/2012/08/09/churchs-law/