在 Coq 中形式化可计算性理论
Formalizing computability theory in Coq
我正在尝试通过形式化形式化我熟悉的数学定理来自学 Coq：停机问题的不可判定性 可计算性理论中的各种定理
由于我对形式化计算模型的细节（例如，图灵机、寄存器机、lambda 演算等）不感兴趣，我正在尝试通过 "teaching Coq Church-Turing thesis"，即， 假设 Axiom 声明 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 似乎（至少天真地）很自然。同时，要使神谕变得不平凡，它们就必须是不可计算的。考虑到这一点，具有类型 nat -> bool 的 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 *)
这是介绍一个有意义的公理的方法（我自己仍在学习 Coq，所以希望如果我做错了，有人会纠正我）。
在 Parameter 中，我们规定了一个名为 compute 的函数的存在，但没有给出定义。对于 Axiom，我们正在修复它的一些属性（希望不会引入矛盾）。据称，Parameter和Axiom在内部做同样的事情。
与 compute 的声明类似，您的 Axiom Phi 规定存在从 nat 到 partial 的函数 Phi，但您不能在 Coq 但是因为它没有已知的属性。请注意，Phi 的存在并不意味着 "there is an effective enumeration of the partial computable functions".
这里的公理指出，当使用更多允许的计算步骤调用时，compute 永远不会将 ACCEPT 更改为 REJECT，反之亦然或备份到 NOTYET。通过这些定义，我检查了是否有可能证明简单的引理 test 作为入门。
显然，我没有进行此操作以查看您是否可以证明停机问题的不可判定性，但应该可以通过添加一个断言 nat 代表计算程序的存在的公理来实现等同于证明停机问题所需的结构。当然，这样做基本上失去了整个证明点，但仍有一点需要证明。
Inductive result :=
| ACCEPT : result
| REJECT : result
| NOTYET : result.
Definition narrowing a b : Prop :=
(match a with
| ACCEPT => b = ACCEPT
| REJECT => b = REJECT
| NOTYET => True
end).
Parameter compute : nat (* program *) -> nat (* argument *) -> nat (* steps *) -> result.
Axiom compute_narrowing:
forall program input steps steps',
(steps' >= steps) ->
(narrowing (compute program input steps) (compute program input steps')).
Lemma test: ~ exists program input steps, (compute program input steps) = ACCEPT /\ (compute program input (steps + 1)) = NOTYET
编辑： 这里还有一点。稍微考虑一下这个问题后，我意识到我绝对错了，这样的证明必然要将有趣的结构公理化。可以插入只允许简单的低级构造的公理，并在它们之上构建更高级别的构造。我假设目标是遵循明斯基的证明，因为形式化似乎更简单：
http://www.cs.odu.edu/~toida/nerzic/390teched/computability/unsolv-1.html
这里，附加公理断言 1) 存在一个总是接受的程序 2) 存在一个总是拒绝的程序和 3) 对于任何三个程序 conditional when_accept when_reject，存在一个首先运行 conditional 然后基于该运行 when_accept 或 when_reject 的程序（所有子程序调用都在给定组合程序的相同输入上）。有了这些公理，就可以证明，对于任何程序 target 都存在运行 target 然后输出相反结果的程序（但如果 target 永远循环，也会永远循环） .这个 "negation" 构造只是一个简单的例子，而不是明斯基证明中使用的构造之一。
要遵循明斯基的证明，需要为循环程序的存在以及复印机构造添加更多公理。然后添加一个程序何时是决策者的定义，并证明停机问题没有决策者。 codec 公理省去了在 Coq 中定义函数 encode_pair 和 decode_pair 并证明 codec 作为引理的麻烦。我认为复印机构造和最终证明需要 encode_pair 和 decode_pair 的属性（当然，暂停问题的决策者的定义需要它，因为机器输入是一对） .
Require Import List.
Require Import Arith.
Require Import Omega.
Ltac mp_cancel :=
repeat match goal with
| [ H2 : ?P -> ?Q , H1 : ?P |- _ ] => specialize (H2 H1)
end.
Ltac mp_cancel_reflexivity :=
repeat match goal with
| [ H1 : ?P = ?P -> ?Q |- _ ] => assert (H_mp_cancel_reflexivity : P = P) by reflexivity; specialize (H1 H_mp_cancel_reflexivity); clear H_mp_cancel_reflexivity
end.
Inductive result :=
| ACCEPT : result
| REJECT : result
| NOTYET : result
.
Definition narrowing a b : Prop :=
(match a with
| ACCEPT => b = ACCEPT
| REJECT => b = REJECT
| NOTYET => True
end)
.
Parameter encode_pair : (nat * nat) -> nat.
Parameter decode_pair : nat -> (nat * nat).
Axiom codec:
forall a b,
(decode_pair (encode_pair (a, b))) = (a, b).
Parameter compute : nat (* program *) -> nat (* input *) -> nat (* steps *) -> result.
Axiom compute_narrowing:
forall program input steps steps',
(steps' >= steps) -> (narrowing (compute program input steps) (compute program input steps')).
Axiom exists_always_accept:
exists program_always_accept,
forall input,
exists steps,
(compute program_always_accept input steps) = ACCEPT.
Axiom exists_always_reject:
exists program_always_reject,
forall input,
exists steps,
(compute program_always_reject input steps) = REJECT.
Definition result_compose_conditional (result_conditional : result) (result_when_accept : result) (result_when_reject : result) : result :=
(match result_conditional with
| ACCEPT => result_when_accept
| REJECT => result_when_reject
| NOTYET => NOTYET
end).
Axiom exists_compose_conditional:
forall program_conditional program_when_accept program_when_reject,
exists program_composition,
forall input steps_control steps_when result_conditional result_when_accept result_when_reject,
(
((compute program_conditional input steps_control) = result_conditional) ->
((compute program_when_accept input steps_when) = result_when_accept) ->
((compute program_when_reject input steps_when) = result_when_reject) ->
(exists steps_composition, (compute program_composition input steps_composition) = (result_compose_conditional result_conditional result_when_accept result_when_reject))
).
Definition result_negation (result_target : result) : result :=
(match result_target with
| ACCEPT => REJECT
| REJECT => ACCEPT
| NOTYET => NOTYET
end).
Lemma exists_negation:
forall program_target,
exists program_negation,
forall input steps_target result_target,
(
((compute program_target input steps_target) = result_target) ->
(exists steps_negation, (compute program_negation input steps_negation) = (result_negation result_target))
).
intros.
elim exists_always_accept; intros program_always_accept H_always_accept.
elim exists_always_reject; intros program_always_reject H_always_reject.
elim exists_compose_conditional with (program_conditional := program_target) (program_when_accept := program_always_reject) (program_when_reject := program_always_accept); intros program_negation H_program_negation.
exists program_negation.
intros.
specialize H_always_accept with input. elim H_always_accept; clear H_always_accept; intros steps_accept H_always_accept.
specialize H_always_reject with input. elim H_always_reject; clear H_always_reject; intros steps_reject H_always_reject.
pose (steps_when := (steps_accept + steps_reject)).
specialize H_program_negation with input steps_target steps_when result_target (compute program_always_reject input steps_when) (compute program_always_accept input steps_when).
mp_cancel.
mp_cancel_reflexivity.
elim H_program_negation; clear H_program_negation; intros steps_negation H_program_negation.
exists (steps_negation).
rewrite H_program_negation; clear H_program_negation.
replace (compute program_always_reject input steps_when) with REJECT; symmetry.
replace (compute program_always_accept input steps_when) with ACCEPT; symmetry.
unfold result_compose_conditional.
unfold result_negation.
reflexivity.
assert (T := (compute_narrowing program_always_accept input steps_accept steps_when)).
assert (steps_when >= steps_accept).
unfold steps_when.
omega.
mp_cancel.
unfold narrowing in T.
rewrite H_always_accept in T.
assumption.
assert (T := (compute_narrowing program_always_reject input steps_reject steps_when)).
assert (steps_when >= steps_reject).
unfold steps_when.
omega.
mp_cancel.
unfold narrowing in T.
rewrite H_always_reject in T.
assumption.
Qed.
EDIT#2：我有点理解你希望能够在 Coq 中对结构进行编程，但我还没有弄清楚如何在我之前编辑的时间。在下面的片段中，它是使用公理 exists_program_of_procedure 完成的，它断言存在一个 nat 表示一个程序，该程序与任何给定过程具有相同的行为（至少对于 "narrowing" 在他们的计算中）。包括明斯基证明的直接形式化。您的方法肯定有更清晰的公理，并且由于使用 modulus 来 oracle-ify 稳定步骤而不是处理 narrowing，可能会导致更短的证明。最有趣的是您的方法是否可以在不使用 Classical 的情况下执行。 更新： 您的公理似乎引入了矛盾，因为 modulus 不应该是可计算的 (?)。
Require Import List.
Require Import Arith.
Require Import Omega.
Ltac mp_cancel :=
repeat match goal with
| [ H2 : ?P -> ?Q , H1 : ?P |- _ ] => specialize (H2 H1)
end.
Ltac mp_cancel_reflexivity :=
repeat match goal with
| [ H1 : ?P = ?P -> ?Q |- _ ] => assert (H_mp_cancel_reflexivity : P = P) by reflexivity; specialize (H1 H_mp_cancel_reflexivity); clear H_mp_cancel_reflexivity
end.
Parameter encode_pair: (nat * nat) -> nat.
Parameter decode_pair: nat -> (nat * nat).
Axiom decode_encode: forall a b, (decode_pair (encode_pair (a, b))) = (a, b).
Inductive result :=
| ACCEPT : result
| REJECT : result
| NOTYET : result.
Definition result_narrowing (a : result) (b : result) : Prop :=
(match a with
| ACCEPT => b = ACCEPT
| REJECT => b = REJECT
| NOTYET => True
end).
Lemma result_narrowing_trans: forall a b c, result_narrowing a b -> result_narrowing b c -> result_narrowing a c.
intros until 0.
destruct a; destruct b; destruct c;
unfold result_narrowing;
intros;
try discriminate;
reflexivity.
Qed.
Parameter compute: nat (* program *) -> nat (* input *) -> nat (* steps *) -> result.
Axiom compute_narrowing:
forall program input steps steps',
(steps' >= steps) -> (result_narrowing (compute program input steps) (compute program input steps')).
Require Import Classical.
Lemma compute_non_divergent:
forall program input steps steps',
(compute program input steps) = ACCEPT ->
(compute program input steps') = REJECT ->
False.
intros.
assert (T := (classic (steps' >= steps))).
destruct T.
assert (T := (compute_narrowing program input steps steps')).
mp_cancel.
rewrite H, H0 in T.
unfold result_narrowing in T.
discriminate T.
unfold not in H1.
assert (T := (classic (steps' = steps))).
destruct T.
rewrite H2 in H0.
rewrite H in H0.
discriminate.
assert (steps >= steps').
omega.
assert (T := (compute_narrowing program input steps' steps)).
mp_cancel.
rewrite H, H0 in T.
unfold result_narrowing in T.
discriminate.
Qed.
Definition procedure_type := nat (* input *) -> nat (* depth *) -> result.
Definition procedure_narrowing (procedure : procedure_type) : Prop :=
forall input depth depth',
(depth' >= depth) -> (result_narrowing (procedure input depth) (procedure input depth')).
Axiom exists_program_of_procedure:
forall procedure : procedure_type,
(procedure_narrowing procedure) ->
exists program,
forall input,
(
forall depth,
exists steps,
(result_narrowing (procedure input depth) (compute program input steps))
) /\
(
forall steps,
exists depth,
(result_narrowing (compute program input steps) (procedure input depth))
).
Definition program_halts_on_input (program : nat) (input : nat) : Prop :=
(exists steps, (compute program input steps) <> NOTYET).
Definition program_is_decider (program : nat) : Prop :=
forall input,
exists steps,
(compute program input steps) <> NOTYET.
Definition program_solves_halting_problem_partially (program : nat) : Prop :=
forall input,
forall steps,
(
((compute program input steps) = ACCEPT)
-> (match (decode_pair input) with | (target_program, target_input) => ( (program_halts_on_input target_program target_input)) end)
) /\
(
((compute program input steps) = REJECT)
-> (match (decode_pair input) with | (target_program, target_input) => (~ (program_halts_on_input target_program target_input)) end)
).
Lemma minsky: (~ (exists halts, (program_is_decider halts) /\ (program_solves_halting_problem_partially halts))).
unfold not.
intros H_ph.
elim H_ph; clear H_ph; intros invocation_halts [H_ph_d H_ph_b].
pose
(procedure_modified := (fun (input : nat) (depth : nat) =>
(match (compute invocation_halts input depth) with
| ACCEPT => NOTYET
| REJECT => REJECT
| NOTYET => NOTYET
end))).
pose
(procedure_wrapper := (fun (input : nat) (depth : nat) =>
(procedure_modified (encode_pair (input, input)) depth))).
unfold procedure_modified in procedure_wrapper.
clear procedure_modified.
assert (T1 := (exists_program_of_procedure procedure_wrapper)).
assert (T2 : (procedure_narrowing procedure_wrapper)).
{
clear T1.
unfold procedure_narrowing, procedure_wrapper.
intros.
unfold result_narrowing.
case_eq (compute invocation_halts (encode_pair (input, input)) depth); try intuition.
assert (T := (compute_narrowing invocation_halts (encode_pair (input, input)) depth depth')).
mp_cancel.
rewrite H0 in T.
unfold result_narrowing in T.
rewrite T.
reflexivity.
}
mp_cancel.
clear T2.
elim T1; clear T1; intros program_wrapper H_pw.
unfold procedure_wrapper in H_pw.
clear procedure_wrapper.
specialize (H_pw program_wrapper).
destruct H_pw as [H_pw_fwd H_pw_rev].
unfold program_is_decider in H_ph_d.
specialize (H_ph_d (encode_pair (program_wrapper, program_wrapper))).
elim H_ph_d; clear H_ph_d; intros steps_inner H_ph_d.
unfold program_solves_halting_problem_partially in H_ph_b.
specialize (H_ph_b (encode_pair (program_wrapper, program_wrapper)) steps_inner).
destruct H_ph_b as [H_ph_b_1 H_ph_b_2].
case_eq (compute invocation_halts (encode_pair (program_wrapper, program_wrapper)) steps_inner).
{
intros.
rewrite H in *.
mp_cancel_reflexivity.
unfold program_halts_on_input in H_ph_b_1.
rewrite decode_encode in H_ph_b_1.
elim H_ph_b_1; clear H_ph_b_1; intros steps_outer H_ph_b_1.
specialize (H_pw_rev steps_outer).
case_eq (compute program_wrapper program_wrapper steps_outer).
{
intros.
rewrite H0 in *.
unfold result_narrowing in H_pw_rev.
elim H_pw_rev; clear H_pw_rev; intros depth H_pw_rev.
case_eq (compute invocation_halts (encode_pair (program_wrapper, program_wrapper)) depth); intros Hx; rewrite Hx in *; try discriminate.
}
{
intros.
rewrite H0 in *.
unfold result_narrowing in H_pw_rev.
elim H_pw_rev; clear H_pw_rev; intros depth H_pw_rev.
case_eq (compute invocation_halts (encode_pair (program_wrapper, program_wrapper)) depth); intros Hx; rewrite Hx in *; try discriminate.
assert (T := (compute_non_divergent invocation_halts (encode_pair (program_wrapper, program_wrapper)) steps_inner depth)).
mp_cancel.
assumption.
}
{
intros.
intuition.
}
}
{
intros.
rewrite H in *.
mp_cancel_reflexivity.
unfold not, program_halts_on_input in H_ph_b_2.
specialize (H_pw_fwd steps_inner).
rewrite H in H_pw_fwd.
unfold result_narrowing in H_pw_fwd.
elim H_pw_fwd; intros.
rewrite decode_encode in H_ph_b_2.
contradict H_ph_b_2.
exists x.
unfold not.
intros.
rewrite H0 in H1.
discriminate.
}
{
intros.
unfold not in H_ph_d.
mp_cancel.
assumption.
}
Qed.
首先，澄清一下：
Functions that Coq thinks to be computable (i.e., definable functions of type nat -> nat)
严格来说，Coq 不认为函数是可计算的。 Coq 的逻辑断言可以定义某些函数，并且您可以用它们做某些事情，但就 Coq 而言，任意函数是一个黑盒子。特别是，假设存在一个不可计算的函数是一致的。
现在，进入实际问题。这是或多或少遵循 Atsby's answer 的解决方案。我们将用 nat -> nat -> option bool 类型的 Coq 函数表示图灵机函数。这个想法是第一个参数是输入，第二个参数是我们将 运行 的最大步数。如果我们未能生成答案，则输出为 None，如果计算以生成 b 作为答案而终止，则输出为 Some 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 与图灵机相关——例如，您可以将上述定理解释为 oracle 图灵机无法解决 oracle 图灵机的停机问题机器。最后，使这些结果彼此不同的是底层计算模型的形式化，这正是您想要避免的。
至于你试图开始的模板，假设 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 关系 解决了这个问题。
至于 oracles，让 oracle 成为 nat -> bool 类型的函数确实有意义，但您需要确保这样做不会违反证明中的其他假设。例如，你可以假设所有 nat -> nat 函数都是可计算的，通过公理化你有一个像你的 Phi 的函数，但这意味着你的 oracle 也是可计算的。使用像上面的 code 这样的关系可以让你两全其美。
最后，关于相对论的结果，很大程度上取决于你想证明什么。例如，如果你只是想证明可以编写 oracle 上的某些函数，你可以编写一个参数函数并在 oracle 具有特定行为时显示它具有特定的 属性，而不需要依赖类型.例如
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]. *)
最后，这里有一个有趣的 link 讨论 Church 在依赖类型理论中的论文，您可能会觉得有趣：https://existentialtype.wordpress.com/2012/08/09/churchs-law/
我想我会添加一个新的答案来充实我在对 OP post 关于预言机处理的评论中提出的方案的细节。
我不确定 DeAmorim 处理预言机的方案是否也能正常工作。这里的哲学是应该避免 post 引用 具有各种属性的构造的存在，而只是简单地定义它们（例如，作为 Coq 函数）并证明它们具有必需的属性。因为我们不想将图灵机的实际描述处理到状态机级别，所以使用的 hack 是 post 制定从 Coq 函数到程序的映射。当假设 Coq 函数可以映射到程序时，当以 Coq 函数 的形式引入不可计算的预言机 时，逻辑必然会变得不一致（即使显然不会提供一个建设性的定义）。虽然不太可能在手动证明中利用这种出现的逻辑不一致，但完全避免不一致的逻辑更令人放心。
（但是，尚不清楚提议的策略是否实现了这一点。DeAmorim 的回答中链接的文章说 "The claim is that Church’s Law, stated as a type (proposition) within ETT, is false, which is to say that it entails a contradiction." 这背后的数学似乎比我的水平高出很多；不清楚我是否适用。）
这里考虑的示例问题是解决 H_TM 假设我们有 A_TM 的 oracle。 H_TM 告诉我们图灵机 ("program") 停止 特定输入，而 A_TM 告诉我们图灵机 接受一个特定的输入。
显然，拥有 H_TM 的 oracle 并试图解决 A_TM 的相反情况是完全微不足道的。只需查询 oracle 以确定程序是否停止，如果是，则程序可以 运行 终止以确定是否接受。
稍微不那么琐碎的是，如果我们得到 A_TM 的预言，就可以决定 H_TM。显然，如果机器接受输入，则 oracle 查询可以确定这一点。现在的诀窍是构建一个与原始程序相反的修改后的程序（交换 ACCEPT 和 REJECT），并且对这个修改后的程序的 oracle 查询现在确定原始程序是否会 reject输入。如果 oracle 拒绝了这两种情况，则原始程序在给定输入上循环，我们拒绝（在其他情况下我们接受）。
此处实现的 "machinery" 允许定义 nat (* query *) -> nat (* wisdom *) -> bool (* advice *) 类型的 oracle verifiers。对应于验证者的真实预言机将输出真当且仅当存在一个智慧的值导致验证者输出真。聪明的一点是，不可计算的神谕可以从可计算的验证者中生成，并且单个存在量词足以生成相当强大的神谕。
A "procedure with oracle" (pwo) 必须根据循环状态来实现，因为不能简单地使用函数应用程序来调用此设置中的 oracle。
归纳 pwo_entails 基本上定义了 pwo 的求值，类似于软件基础中 ceval 定义的 Imp 程序的求值方式。
A_TMorv_atm的oracle验证器只是执行wisdom步的程序来判断是否接受，而pwo_hfa弥补到两个 oracle 调用来决定 H_TM。引理 H_from_A 表明这是可行的。
与之前涉及停机问题的答案相比，一个很大的变化是允许将 Coq 函数转换为可以传递给 compute 的程序的基本公理得到了加强，现在假设一个可计算函数存在以执行此类转换。以前，只有相应程序的存在是 post 计算出来的。此更改是必需的，因为 pwo_hfa 需要生成程序 "programmatically".
Require Import List.
Require Import Arith.
Require Import Omega.
Ltac mp_cancel :=
repeat match goal with
| [ H2 : ?P -> ?Q , H1 : ?P |- _ ] => specialize (H2 H1)
end.
Ltac mp_cancel_reflexivity :=
repeat match goal with
| [ H1 : ?P = ?P -> ?Q |- _ ] => assert (H_mp_cancel_reflexivity : P = P) by reflexivity; specialize (H1 H_mp_cancel_reflexivity); clear H_mp_cancel_reflexivity
end.
Parameter encode_pair: (nat * nat) -> nat.
Parameter decode_pair: nat -> (nat * nat).
Axiom decode_encode: forall a b, (decode_pair (encode_pair (a, b))) = (a, b).
Axiom encode_decode: forall x, (encode_pair (decode_pair x)) = x.
Inductive result :=
| ACCEPT : result
| REJECT : result
| NOTYET : result.
Definition result_narrowing (a : result) (b : result) : Prop :=
(match a with
| ACCEPT => b = ACCEPT
| REJECT => b = REJECT
| NOTYET => True
end).
Lemma result_narrowing_trans: forall a b c, result_narrowing a b -> result_narrowing b c -> result_narrowing a c.
intros until 0.
destruct a; destruct b; destruct c;
unfold result_narrowing;
intros;
try discriminate;
reflexivity.
Qed.
Lemma result_push_accept: forall x, result_narrowing ACCEPT x -> x = ACCEPT.
unfold result_narrowing.
intuition.
Qed.
Lemma result_push_reject: forall x, result_narrowing REJECT x -> x = REJECT.
unfold result_narrowing.
intuition.
Qed.
Parameter compute: nat (* program *) -> nat (* input *) -> nat (* steps *) -> result.
Axiom compute_narrowing:
forall program input steps steps',
(steps' >= steps) -> (result_narrowing (compute program input steps) (compute program input steps')).
Require Import Classical.
Lemma compute_non_divergent:
forall program input steps steps',
(compute program input steps) = ACCEPT ->
(compute program input steps') = REJECT ->
False.
intros.
assert (T := (classic (steps' >= steps))).
destruct T.
assert (T := (compute_narrowing program input steps steps')).
mp_cancel.
rewrite H, H0 in T.
unfold result_narrowing in T.
discriminate T.
unfold not in H1.
assert (T := (classic (steps' = steps))).
destruct T.
rewrite H2 in H0.
rewrite H in H0.
discriminate.
assert (steps >= steps').
omega.
assert (T := (compute_narrowing program input steps' steps)).
mp_cancel.
rewrite H, H0 in T.
unfold result_narrowing in T.
discriminate.
Qed.
Definition procedure_type := nat (* input *) -> nat (* depth *) -> result.
Definition procedure_narrowing (procedure : procedure_type) : Prop :=
forall input depth depth',
(depth' >= depth) -> (result_narrowing (procedure input depth) (procedure input depth')).
Parameter program_of_procedure: procedure_type (* procedure *) -> nat (* program *).
Axiom program_of_procedure_behavior:
forall procedure : procedure_type,
(procedure_narrowing procedure) ->
forall input,
(
forall depth,
exists steps,
(result_narrowing (procedure input depth) (compute (program_of_procedure procedure) input steps))
) /\
(
forall steps,
exists depth,
(result_narrowing (compute (program_of_procedure procedure) input steps) (procedure input depth))
).
Definition program_halts_on_input (program : nat) (input : nat) : Prop :=
(exists steps, (compute program input steps) <> NOTYET).
(* orv = oracle verifier *)
Definition orv_type := nat (* query *) -> nat (* wisdom *) -> bool (* advice *).
Definition oracle_accepts (oracle : orv_type) (query : nat) :=
exists wisdom, (oracle query wisdom) = true.
Definition oracle_rejects (orv : orv_type) (inp : nat) := (~ (oracle_accepts orv inp)).
(* pwo = procedure with oracle *)
Inductive pwo_out :=
| PWO_RESULT : bool (* result *) -> pwo_out
| PWO_ORACLE : nat (* state *) -> nat (* query *) -> pwo_out
.
Definition pwo_type := nat (* input *) -> nat (* state *) -> bool (* advice *) -> pwo_out.
Inductive pwo_entails: orv_type (* oracle *) -> pwo_type (* procedure *) -> nat (* input *) -> nat (* state *) -> bool (* advice *) -> bool (* result *) -> Prop :=
| PwoEntailsResult:
forall oracle procedure input state advice result,
(procedure input state advice) = (PWO_RESULT result) ->
(pwo_entails oracle procedure input state advice result)
| PwoEntailsOracleAccept:
forall oracle procedure input state advice result state' query,
(procedure input state advice) = (PWO_ORACLE state' query) ->
(oracle_accepts oracle query) ->
(pwo_entails oracle procedure input state' true result) ->
(pwo_entails oracle procedure input state advice result)
| PwoEntailsOracleReject:
forall oracle procedure input state advice result state' query,
(procedure input state advice) = (PWO_ORACLE state' query) ->
(oracle_rejects oracle query) ->
(pwo_entails oracle procedure input state' false result) ->
(pwo_entails oracle procedure input state advice result)
.
Definition pwo_decider_relative (orv : orv_type) (pwo : pwo_type) :=
forall input,
(pwo_entails orv pwo input 0 false false) \/
(pwo_entails orv pwo input 0 false true).
(* define oracle for A_TM (turing machine accepts a particular input) *)
Definition orv_atm (pair_program_input : nat) (wisdom : nat) : bool :=
(match (decode_pair pair_program_input) with
| (target_program, target_input) =>
(match (compute target_program target_input wisdom) with
| ACCEPT => true
| _ => false
end)
end).
(* define procedure for H_TM (turing machine halts on a particular input) relative to an oracle for A_TM *)
Definition pwo_hfa_construction (target_program : nat) :=
(fun input depth =>
(match (compute target_program input depth) with
| ACCEPT => REJECT
| REJECT => ACCEPT
| NOTYET => NOTYET
end)).
Lemma pwo_hfa_construction_narrowing: forall target_program, (procedure_narrowing (pwo_hfa_construction target_program)).
intros.
unfold procedure_narrowing, result_narrowing, pwo_hfa_construction.
intros.
case_eq (compute target_program input depth); intro; try
(
case_eq (compute target_program input depth'); intro; try reflexivity; try
(
assert (T := (compute_narrowing target_program input depth depth'));
mp_cancel;
unfold result_narrowing in T;
rewrite H0 in T;
rewrite H1 in T;
discriminate
)
).
Qed.
Definition pwo_hfa (input : nat) (state : nat) (advice : bool) : pwo_out :=
(match (decode_pair input) with
| (target_program, target_input) =>
(match state with
| O =>
(PWO_ORACLE 1 (encode_pair (target_program, target_input)))
| (S O) =>
(if advice
then (PWO_RESULT true)
else (PWO_ORACLE 2 (encode_pair ((program_of_procedure (pwo_hfa_construction target_program)), target_input))))
| _ =>
(PWO_RESULT advice)
end)
end).
Lemma H_from_A:
exists pwo_hfa,
(pwo_decider_relative orv_atm pwo_hfa) /\
(
forall input,
(pwo_entails orv_atm pwo_hfa input 0 false true ->
(match (decode_pair input) with | (target_program, target_input) => ( (program_halts_on_input target_program target_input)) end)) /\
(pwo_entails orv_atm pwo_hfa input 0 false false ->
(match (decode_pair input) with | (target_program, target_input) => (~ (program_halts_on_input target_program target_input)) end))
)
.
exists pwo_hfa.
split.
{
unfold pwo_decider_relative.
intros.
pose (pair := (decode_pair input)).
case_eq (pair); intros target_program target_input H_pair.
replace input with (encode_pair (target_program, target_input)).
Focus 2.
{
rewrite <- H_pair.
unfold pair.
apply encode_decode.
}
Unfocus.
assert (T1 := (classic (oracle_accepts orv_atm (encode_pair (target_program, target_input))))).
destruct T1 as [T1 | T1].
{
right.
eapply PwoEntailsOracleAccept.
Focus 2.
eexact T1.
unfold pwo_hfa.
rewrite decode_encode.
instantiate (1 := 1).
reflexivity.
apply PwoEntailsResult.
unfold pwo_hfa.
rewrite decode_encode.
reflexivity.
}
{
assert (T2 := (classic (oracle_accepts orv_atm (encode_pair ((program_of_procedure (pwo_hfa_construction target_program)), target_input))))).
destruct T2 as [T2 | T2].
{
right.
eapply PwoEntailsOracleReject.
Focus 2.
unfold oracle_rejects.
eexact T1.
unfold pwo_hfa.
rewrite decode_encode.
instantiate (1 := 1).
reflexivity.
eapply PwoEntailsOracleAccept.
Focus 2.
eexact T2.
unfold pwo_hfa.
rewrite decode_encode.
instantiate (1 := 2).
reflexivity.
apply PwoEntailsResult.
unfold pwo_hfa.
rewrite decode_encode.
reflexivity.
}
{
left.
eapply PwoEntailsOracleReject.
Focus 2.
unfold oracle_rejects.
eexact T1.
unfold pwo_hfa.
rewrite decode_encode.
instantiate (1 := 1).
reflexivity.
eapply PwoEntailsOracleReject.
Focus 2.
eexact T2.
unfold pwo_hfa.
rewrite decode_encode.
instantiate (1 := 2).
reflexivity.
apply PwoEntailsResult.
unfold pwo_hfa.
rewrite decode_encode.
reflexivity.
}
}
}
{
intros.
case_eq (decode_pair input); intros target_program target_input H_input.
replace input with (encode_pair (target_program, target_input)).
Focus 2.
{
rewrite <- H_input.
rewrite encode_decode.
reflexivity.
}
Unfocus.
clear H_input.
split.
{
intros.
inversion H; subst.
{
unfold pwo_hfa in H0.
rewrite decode_encode in H0.
discriminate H0.
}
{
unfold pwo_hfa in H0.
rewrite decode_encode in H0.
injection H0.
intros.
rewrite <- H3 in H1.
unfold oracle_accepts in H1.
unfold program_halts_on_input.
elim H1; intros.
exists x.
unfold orv_atm in H5.
rewrite decode_encode in H5.
destruct (compute target_program target_input x); try intuition; try discriminate.
}
{
unfold pwo_hfa in H0.
rewrite decode_encode in H0.
injection H0.
intros.
rewrite <- H4 in *.
inversion H2; subst.
{
unfold pwo_hfa in H5.
rewrite decode_encode in H5.
discriminate.
}
{
unfold pwo_hfa in H5.
rewrite decode_encode in H5.
injection H5; intros.
subst.
unfold oracle_accepts in H6.
unfold program_halts_on_input.
elim H6; intros.
unfold orv_atm in H3.
rewrite decode_encode in H3.
case_eq (compute (program_of_procedure (pwo_hfa_construction target_program)) target_input x); intros; rewrite H4 in H3; try discriminate.
assert
(T :=
(program_of_procedure_behavior
(pwo_hfa_construction target_program)
(pwo_hfa_construction_narrowing target_program)
target_input
)).
destruct T.
specialize H9 with x.
elim H9; intros.
assert ((pwo_hfa_construction target_program target_input x0) = ACCEPT).
eapply result_push_accept.
rewrite <- H4.
assumption.
unfold pwo_hfa_construction in H11.
case_eq (compute target_program target_input x0); intros; rewrite H12 in H11; try discriminate.
exists x0.
unfold not.
intros.
rewrite H12 in H13.
discriminate.
}
{
unfold pwo_hfa in H5.
rewrite decode_encode in H5.
injection H5; intros.
subst.
inversion H7.
unfold pwo_hfa in H3.
rewrite decode_encode in H3.
discriminate H3.
unfold pwo_hfa in H3.
rewrite decode_encode in H3.
discriminate H3.
unfold pwo_hfa in H3.
rewrite decode_encode in H3.
discriminate H3.
}
}
}
{
intros.
unfold not.
intros.
inversion H; subst; unfold pwo_hfa in H1; rewrite decode_encode in H1; try discriminate; injection H1; intros; subst.
{
inversion H3; subst; unfold pwo_hfa in H4; rewrite decode_encode in H4; try discriminate; injection H4; intros; subst.
}
{
inversion H3; subst; unfold pwo_hfa in H4; rewrite decode_encode in H4; try discriminate; injection H4; intros; subst.
{
inversion H6; subst; unfold pwo_hfa in H7; rewrite decode_encode in H7; try discriminate.
}
{
(* oracle rejected both on a program that halts *)
clear H H3 H1 H6 H4.
unfold program_halts_on_input in H0.
elim H0; clear H0; intros.
unfold not in H.
case_eq (compute target_program target_input x); intros; try ( solve [ intuition ] ).
{
rename H2 into HH.
unfold oracle_rejects, not in HH.
apply HH.
clear HH.
unfold oracle_accepts.
exists x.
unfold orv_atm.
rewrite decode_encode.
rewrite H0.
reflexivity.
}
{
rename H5 into HH.
unfold oracle_rejects, not in HH.
apply HH.
clear HH.
unfold oracle_accepts.
assert
(T :=
(program_of_procedure_behavior
(pwo_hfa_construction target_program)
(pwo_hfa_construction_narrowing target_program)
target_input
)).
destruct T.
assert ((pwo_hfa_construction target_program target_input x) = ACCEPT).
unfold pwo_hfa_construction.
rewrite H0.
reflexivity.
specialize H1 with x.
elim H1; intros.
rewrite H4 in H5.
unfold result_narrowing in H5.
exists x0.
unfold orv_atm.
rewrite decode_encode.
rewrite H5.
reflexivity.
}
}
}
}
}
Qed.
我正在尝试通过形式化形式化我熟悉的数学定理来自学 Coq：停机问题的不可判定性 可计算性理论中的各种定理
由于我对形式化计算模型的细节（例如，图灵机、寄存器机、lambda 演算等）不感兴趣，我正在尝试通过 "teaching Coq Church-Turing thesis"，即， 假设 Axiom 声明 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 似乎（至少天真地）很自然。同时，要使神谕变得不平凡，它们就必须是不可计算的。考虑到这一点，具有类型 nat -> bool 的 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 *)
这是介绍一个有意义的公理的方法（我自己仍在学习 Coq，所以希望如果我做错了，有人会纠正我）。
在 Parameter 中，我们规定了一个名为 compute 的函数的存在，但没有给出定义。对于 Axiom，我们正在修复它的一些属性（希望不会引入矛盾）。据称，Parameter和Axiom在内部做同样的事情。
与 compute 的声明类似，您的 Axiom Phi 规定存在从 nat 到 partial 的函数 Phi，但您不能在 Coq 但是因为它没有已知的属性。请注意，Phi 的存在并不意味着 "there is an effective enumeration of the partial computable functions".
这里的公理指出，当使用更多允许的计算步骤调用时，compute 永远不会将 ACCEPT 更改为 REJECT，反之亦然或备份到 NOTYET。通过这些定义，我检查了是否有可能证明简单的引理 test 作为入门。
显然，我没有进行此操作以查看您是否可以证明停机问题的不可判定性，但应该可以通过添加一个断言 nat 代表计算程序的存在的公理来实现等同于证明停机问题所需的结构。当然，这样做基本上失去了整个证明点，但仍有一点需要证明。
Inductive result :=
| ACCEPT : result
| REJECT : result
| NOTYET : result.
Definition narrowing a b : Prop :=
(match a with
| ACCEPT => b = ACCEPT
| REJECT => b = REJECT
| NOTYET => True
end).
Parameter compute : nat (* program *) -> nat (* argument *) -> nat (* steps *) -> result.
Axiom compute_narrowing:
forall program input steps steps',
(steps' >= steps) ->
(narrowing (compute program input steps) (compute program input steps')).
Lemma test: ~ exists program input steps, (compute program input steps) = ACCEPT /\ (compute program input (steps + 1)) = NOTYET
编辑： 这里还有一点。稍微考虑一下这个问题后，我意识到我绝对错了，这样的证明必然要将有趣的结构公理化。可以插入只允许简单的低级构造的公理，并在它们之上构建更高级别的构造。我假设目标是遵循明斯基的证明，因为形式化似乎更简单：
http://www.cs.odu.edu/~toida/nerzic/390teched/computability/unsolv-1.html
这里，附加公理断言 1) 存在一个总是接受的程序 2) 存在一个总是拒绝的程序和 3) 对于任何三个程序 conditional when_accept when_reject，存在一个首先运行 conditional 然后基于该运行 when_accept 或 when_reject 的程序（所有子程序调用都在给定组合程序的相同输入上）。有了这些公理，就可以证明，对于任何程序 target 都存在运行 target 然后输出相反结果的程序（但如果 target 永远循环，也会永远循环） .这个 "negation" 构造只是一个简单的例子，而不是明斯基证明中使用的构造之一。
要遵循明斯基的证明，需要为循环程序的存在以及复印机构造添加更多公理。然后添加一个程序何时是决策者的定义，并证明停机问题没有决策者。 codec 公理省去了在 Coq 中定义函数 encode_pair 和 decode_pair 并证明 codec 作为引理的麻烦。我认为复印机构造和最终证明需要 encode_pair 和 decode_pair 的属性（当然，暂停问题的决策者的定义需要它，因为机器输入是一对） .
Require Import List.
Require Import Arith.
Require Import Omega.
Ltac mp_cancel :=
repeat match goal with
| [ H2 : ?P -> ?Q , H1 : ?P |- _ ] => specialize (H2 H1)
end.
Ltac mp_cancel_reflexivity :=
repeat match goal with
| [ H1 : ?P = ?P -> ?Q |- _ ] => assert (H_mp_cancel_reflexivity : P = P) by reflexivity; specialize (H1 H_mp_cancel_reflexivity); clear H_mp_cancel_reflexivity
end.
Inductive result :=
| ACCEPT : result
| REJECT : result
| NOTYET : result
.
Definition narrowing a b : Prop :=
(match a with
| ACCEPT => b = ACCEPT
| REJECT => b = REJECT
| NOTYET => True
end)
.
Parameter encode_pair : (nat * nat) -> nat.
Parameter decode_pair : nat -> (nat * nat).
Axiom codec:
forall a b,
(decode_pair (encode_pair (a, b))) = (a, b).
Parameter compute : nat (* program *) -> nat (* input *) -> nat (* steps *) -> result.
Axiom compute_narrowing:
forall program input steps steps',
(steps' >= steps) -> (narrowing (compute program input steps) (compute program input steps')).
Axiom exists_always_accept:
exists program_always_accept,
forall input,
exists steps,
(compute program_always_accept input steps) = ACCEPT.
Axiom exists_always_reject:
exists program_always_reject,
forall input,
exists steps,
(compute program_always_reject input steps) = REJECT.
Definition result_compose_conditional (result_conditional : result) (result_when_accept : result) (result_when_reject : result) : result :=
(match result_conditional with
| ACCEPT => result_when_accept
| REJECT => result_when_reject
| NOTYET => NOTYET
end).
Axiom exists_compose_conditional:
forall program_conditional program_when_accept program_when_reject,
exists program_composition,
forall input steps_control steps_when result_conditional result_when_accept result_when_reject,
(
((compute program_conditional input steps_control) = result_conditional) ->
((compute program_when_accept input steps_when) = result_when_accept) ->
((compute program_when_reject input steps_when) = result_when_reject) ->
(exists steps_composition, (compute program_composition input steps_composition) = (result_compose_conditional result_conditional result_when_accept result_when_reject))
).
Definition result_negation (result_target : result) : result :=
(match result_target with
| ACCEPT => REJECT
| REJECT => ACCEPT
| NOTYET => NOTYET
end).
Lemma exists_negation:
forall program_target,
exists program_negation,
forall input steps_target result_target,
(
((compute program_target input steps_target) = result_target) ->
(exists steps_negation, (compute program_negation input steps_negation) = (result_negation result_target))
).
intros.
elim exists_always_accept; intros program_always_accept H_always_accept.
elim exists_always_reject; intros program_always_reject H_always_reject.
elim exists_compose_conditional with (program_conditional := program_target) (program_when_accept := program_always_reject) (program_when_reject := program_always_accept); intros program_negation H_program_negation.
exists program_negation.
intros.
specialize H_always_accept with input. elim H_always_accept; clear H_always_accept; intros steps_accept H_always_accept.
specialize H_always_reject with input. elim H_always_reject; clear H_always_reject; intros steps_reject H_always_reject.
pose (steps_when := (steps_accept + steps_reject)).
specialize H_program_negation with input steps_target steps_when result_target (compute program_always_reject input steps_when) (compute program_always_accept input steps_when).
mp_cancel.
mp_cancel_reflexivity.
elim H_program_negation; clear H_program_negation; intros steps_negation H_program_negation.
exists (steps_negation).
rewrite H_program_negation; clear H_program_negation.
replace (compute program_always_reject input steps_when) with REJECT; symmetry.
replace (compute program_always_accept input steps_when) with ACCEPT; symmetry.
unfold result_compose_conditional.
unfold result_negation.
reflexivity.
assert (T := (compute_narrowing program_always_accept input steps_accept steps_when)).
assert (steps_when >= steps_accept).
unfold steps_when.
omega.
mp_cancel.
unfold narrowing in T.
rewrite H_always_accept in T.
assumption.
assert (T := (compute_narrowing program_always_reject input steps_reject steps_when)).
assert (steps_when >= steps_reject).
unfold steps_when.
omega.
mp_cancel.
unfold narrowing in T.
rewrite H_always_reject in T.
assumption.
Qed.
EDIT#2：我有点理解你希望能够在 Coq 中对结构进行编程，但我还没有弄清楚如何在我之前编辑的时间。在下面的片段中，它是使用公理 exists_program_of_procedure 完成的，它断言存在一个 nat 表示一个程序，该程序与任何给定过程具有相同的行为（至少对于 "narrowing" 在他们的计算中）。包括明斯基证明的直接形式化。您的方法肯定有更清晰的公理，并且由于使用 modulus 来 oracle-ify 稳定步骤而不是处理 narrowing，可能会导致更短的证明。最有趣的是您的方法是否可以在不使用 Classical 的情况下执行。 更新： 您的公理似乎引入了矛盾，因为 modulus 不应该是可计算的 (?)。
Require Import List.
Require Import Arith.
Require Import Omega.
Ltac mp_cancel :=
repeat match goal with
| [ H2 : ?P -> ?Q , H1 : ?P |- _ ] => specialize (H2 H1)
end.
Ltac mp_cancel_reflexivity :=
repeat match goal with
| [ H1 : ?P = ?P -> ?Q |- _ ] => assert (H_mp_cancel_reflexivity : P = P) by reflexivity; specialize (H1 H_mp_cancel_reflexivity); clear H_mp_cancel_reflexivity
end.
Parameter encode_pair: (nat * nat) -> nat.
Parameter decode_pair: nat -> (nat * nat).
Axiom decode_encode: forall a b, (decode_pair (encode_pair (a, b))) = (a, b).
Inductive result :=
| ACCEPT : result
| REJECT : result
| NOTYET : result.
Definition result_narrowing (a : result) (b : result) : Prop :=
(match a with
| ACCEPT => b = ACCEPT
| REJECT => b = REJECT
| NOTYET => True
end).
Lemma result_narrowing_trans: forall a b c, result_narrowing a b -> result_narrowing b c -> result_narrowing a c.
intros until 0.
destruct a; destruct b; destruct c;
unfold result_narrowing;
intros;
try discriminate;
reflexivity.
Qed.
Parameter compute: nat (* program *) -> nat (* input *) -> nat (* steps *) -> result.
Axiom compute_narrowing:
forall program input steps steps',
(steps' >= steps) -> (result_narrowing (compute program input steps) (compute program input steps')).
Require Import Classical.
Lemma compute_non_divergent:
forall program input steps steps',
(compute program input steps) = ACCEPT ->
(compute program input steps') = REJECT ->
False.
intros.
assert (T := (classic (steps' >= steps))).
destruct T.
assert (T := (compute_narrowing program input steps steps')).
mp_cancel.
rewrite H, H0 in T.
unfold result_narrowing in T.
discriminate T.
unfold not in H1.
assert (T := (classic (steps' = steps))).
destruct T.
rewrite H2 in H0.
rewrite H in H0.
discriminate.
assert (steps >= steps').
omega.
assert (T := (compute_narrowing program input steps' steps)).
mp_cancel.
rewrite H, H0 in T.
unfold result_narrowing in T.
discriminate.
Qed.
Definition procedure_type := nat (* input *) -> nat (* depth *) -> result.
Definition procedure_narrowing (procedure : procedure_type) : Prop :=
forall input depth depth',
(depth' >= depth) -> (result_narrowing (procedure input depth) (procedure input depth')).
Axiom exists_program_of_procedure:
forall procedure : procedure_type,
(procedure_narrowing procedure) ->
exists program,
forall input,
(
forall depth,
exists steps,
(result_narrowing (procedure input depth) (compute program input steps))
) /\
(
forall steps,
exists depth,
(result_narrowing (compute program input steps) (procedure input depth))
).
Definition program_halts_on_input (program : nat) (input : nat) : Prop :=
(exists steps, (compute program input steps) <> NOTYET).
Definition program_is_decider (program : nat) : Prop :=
forall input,
exists steps,
(compute program input steps) <> NOTYET.
Definition program_solves_halting_problem_partially (program : nat) : Prop :=
forall input,
forall steps,
(
((compute program input steps) = ACCEPT)
-> (match (decode_pair input) with | (target_program, target_input) => ( (program_halts_on_input target_program target_input)) end)
) /\
(
((compute program input steps) = REJECT)
-> (match (decode_pair input) with | (target_program, target_input) => (~ (program_halts_on_input target_program target_input)) end)
).
Lemma minsky: (~ (exists halts, (program_is_decider halts) /\ (program_solves_halting_problem_partially halts))).
unfold not.
intros H_ph.
elim H_ph; clear H_ph; intros invocation_halts [H_ph_d H_ph_b].
pose
(procedure_modified := (fun (input : nat) (depth : nat) =>
(match (compute invocation_halts input depth) with
| ACCEPT => NOTYET
| REJECT => REJECT
| NOTYET => NOTYET
end))).
pose
(procedure_wrapper := (fun (input : nat) (depth : nat) =>
(procedure_modified (encode_pair (input, input)) depth))).
unfold procedure_modified in procedure_wrapper.
clear procedure_modified.
assert (T1 := (exists_program_of_procedure procedure_wrapper)).
assert (T2 : (procedure_narrowing procedure_wrapper)).
{
clear T1.
unfold procedure_narrowing, procedure_wrapper.
intros.
unfold result_narrowing.
case_eq (compute invocation_halts (encode_pair (input, input)) depth); try intuition.
assert (T := (compute_narrowing invocation_halts (encode_pair (input, input)) depth depth')).
mp_cancel.
rewrite H0 in T.
unfold result_narrowing in T.
rewrite T.
reflexivity.
}
mp_cancel.
clear T2.
elim T1; clear T1; intros program_wrapper H_pw.
unfold procedure_wrapper in H_pw.
clear procedure_wrapper.
specialize (H_pw program_wrapper).
destruct H_pw as [H_pw_fwd H_pw_rev].
unfold program_is_decider in H_ph_d.
specialize (H_ph_d (encode_pair (program_wrapper, program_wrapper))).
elim H_ph_d; clear H_ph_d; intros steps_inner H_ph_d.
unfold program_solves_halting_problem_partially in H_ph_b.
specialize (H_ph_b (encode_pair (program_wrapper, program_wrapper)) steps_inner).
destruct H_ph_b as [H_ph_b_1 H_ph_b_2].
case_eq (compute invocation_halts (encode_pair (program_wrapper, program_wrapper)) steps_inner).
{
intros.
rewrite H in *.
mp_cancel_reflexivity.
unfold program_halts_on_input in H_ph_b_1.
rewrite decode_encode in H_ph_b_1.
elim H_ph_b_1; clear H_ph_b_1; intros steps_outer H_ph_b_1.
specialize (H_pw_rev steps_outer).
case_eq (compute program_wrapper program_wrapper steps_outer).
{
intros.
rewrite H0 in *.
unfold result_narrowing in H_pw_rev.
elim H_pw_rev; clear H_pw_rev; intros depth H_pw_rev.
case_eq (compute invocation_halts (encode_pair (program_wrapper, program_wrapper)) depth); intros Hx; rewrite Hx in *; try discriminate.
}
{
intros.
rewrite H0 in *.
unfold result_narrowing in H_pw_rev.
elim H_pw_rev; clear H_pw_rev; intros depth H_pw_rev.
case_eq (compute invocation_halts (encode_pair (program_wrapper, program_wrapper)) depth); intros Hx; rewrite Hx in *; try discriminate.
assert (T := (compute_non_divergent invocation_halts (encode_pair (program_wrapper, program_wrapper)) steps_inner depth)).
mp_cancel.
assumption.
}
{
intros.
intuition.
}
}
{
intros.
rewrite H in *.
mp_cancel_reflexivity.
unfold not, program_halts_on_input in H_ph_b_2.
specialize (H_pw_fwd steps_inner).
rewrite H in H_pw_fwd.
unfold result_narrowing in H_pw_fwd.
elim H_pw_fwd; intros.
rewrite decode_encode in H_ph_b_2.
contradict H_ph_b_2.
exists x.
unfold not.
intros.
rewrite H0 in H1.
discriminate.
}
{
intros.
unfold not in H_ph_d.
mp_cancel.
assumption.
}
Qed.
首先，澄清一下：
Functions that Coq thinks to be computable (i.e., definable functions of type nat -> nat)
严格来说，Coq 不认为函数是可计算的。 Coq 的逻辑断言可以定义某些函数，并且您可以用它们做某些事情，但就 Coq 而言，任意函数是一个黑盒子。特别是，假设存在一个不可计算的函数是一致的。
现在，进入实际问题。这是或多或少遵循 Atsby's answer 的解决方案。我们将用 nat -> nat -> option bool 类型的 Coq 函数表示图灵机函数。这个想法是第一个参数是输入，第二个参数是我们将 运行 的最大步数。如果我们未能生成答案，则输出为 None，如果计算以生成 b 作为答案而终止，则输出为 Some 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 与图灵机相关——例如，您可以将上述定理解释为 oracle 图灵机无法解决 oracle 图灵机的停机问题机器。最后，使这些结果彼此不同的是底层计算模型的形式化，这正是您想要避免的。
至于你试图开始的模板，假设 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 关系 解决了这个问题。
至于 oracles，让 oracle 成为 nat -> bool 类型的函数确实有意义，但您需要确保这样做不会违反证明中的其他假设。例如，你可以假设所有 nat -> nat 函数都是可计算的，通过公理化你有一个像你的 Phi 的函数，但这意味着你的 oracle 也是可计算的。使用像上面的 code 这样的关系可以让你两全其美。
最后，关于相对论的结果，很大程度上取决于你想证明什么。例如，如果你只是想证明可以编写 oracle 上的某些函数，你可以编写一个参数函数并在 oracle 具有特定行为时显示它具有特定的 属性，而不需要依赖类型.例如
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]. *)
最后，这里有一个有趣的 link 讨论 Church 在依赖类型理论中的论文，您可能会觉得有趣：https://existentialtype.wordpress.com/2012/08/09/churchs-law/
我想我会添加一个新的答案来充实我在对 OP post 关于预言机处理的评论中提出的方案的细节。
我不确定 DeAmorim 处理预言机的方案是否也能正常工作。这里的哲学是应该避免 post 引用 具有各种属性的构造的存在，而只是简单地定义它们（例如，作为 Coq 函数）并证明它们具有必需的属性。因为我们不想将图灵机的实际描述处理到状态机级别，所以使用的 hack 是 post 制定从 Coq 函数到程序的映射。当假设 Coq 函数可以映射到程序时，当以 Coq 函数 的形式引入不可计算的预言机 时，逻辑必然会变得不一致（即使显然不会提供一个建设性的定义）。虽然不太可能在手动证明中利用这种出现的逻辑不一致，但完全避免不一致的逻辑更令人放心。
（但是，尚不清楚提议的策略是否实现了这一点。DeAmorim 的回答中链接的文章说 "The claim is that Church’s Law, stated as a type (proposition) within ETT, is false, which is to say that it entails a contradiction." 这背后的数学似乎比我的水平高出很多；不清楚我是否适用。）
这里考虑的示例问题是解决 H_TM 假设我们有 A_TM 的 oracle。 H_TM 告诉我们图灵机 ("program") 停止 特定输入，而 A_TM 告诉我们图灵机 接受一个特定的输入。
显然，拥有 H_TM 的 oracle 并试图解决 A_TM 的相反情况是完全微不足道的。只需查询 oracle 以确定程序是否停止，如果是，则程序可以 运行 终止以确定是否接受。
稍微不那么琐碎的是，如果我们得到 A_TM 的预言，就可以决定 H_TM。显然，如果机器接受输入，则 oracle 查询可以确定这一点。现在的诀窍是构建一个与原始程序相反的修改后的程序（交换 ACCEPT 和 REJECT），并且对这个修改后的程序的 oracle 查询现在确定原始程序是否会 reject输入。如果 oracle 拒绝了这两种情况，则原始程序在给定输入上循环，我们拒绝（在其他情况下我们接受）。
此处实现的 "machinery" 允许定义 nat (* query *) -> nat (* wisdom *) -> bool (* advice *) 类型的 oracle verifiers。对应于验证者的真实预言机将输出真当且仅当存在一个智慧的值导致验证者输出真。聪明的一点是，不可计算的神谕可以从可计算的验证者中生成，并且单个存在量词足以生成相当强大的神谕。
A "procedure with oracle" (pwo) 必须根据循环状态来实现，因为不能简单地使用函数应用程序来调用此设置中的 oracle。
归纳 pwo_entails 基本上定义了 pwo 的求值，类似于软件基础中 ceval 定义的 Imp 程序的求值方式。
A_TMorv_atm的oracle验证器只是执行wisdom步的程序来判断是否接受，而pwo_hfa弥补到两个 oracle 调用来决定 H_TM。引理 H_from_A 表明这是可行的。
与之前涉及停机问题的答案相比，一个很大的变化是允许将 Coq 函数转换为可以传递给 compute 的程序的基本公理得到了加强，现在假设一个可计算函数存在以执行此类转换。以前，只有相应程序的存在是 post 计算出来的。此更改是必需的，因为 pwo_hfa 需要生成程序 "programmatically".
Require Import List.
Require Import Arith.
Require Import Omega.
Ltac mp_cancel :=
repeat match goal with
| [ H2 : ?P -> ?Q , H1 : ?P |- _ ] => specialize (H2 H1)
end.
Ltac mp_cancel_reflexivity :=
repeat match goal with
| [ H1 : ?P = ?P -> ?Q |- _ ] => assert (H_mp_cancel_reflexivity : P = P) by reflexivity; specialize (H1 H_mp_cancel_reflexivity); clear H_mp_cancel_reflexivity
end.
Parameter encode_pair: (nat * nat) -> nat.
Parameter decode_pair: nat -> (nat * nat).
Axiom decode_encode: forall a b, (decode_pair (encode_pair (a, b))) = (a, b).
Axiom encode_decode: forall x, (encode_pair (decode_pair x)) = x.
Inductive result :=
| ACCEPT : result
| REJECT : result
| NOTYET : result.
Definition result_narrowing (a : result) (b : result) : Prop :=
(match a with
| ACCEPT => b = ACCEPT
| REJECT => b = REJECT
| NOTYET => True
end).
Lemma result_narrowing_trans: forall a b c, result_narrowing a b -> result_narrowing b c -> result_narrowing a c.
intros until 0.
destruct a; destruct b; destruct c;
unfold result_narrowing;
intros;
try discriminate;
reflexivity.
Qed.
Lemma result_push_accept: forall x, result_narrowing ACCEPT x -> x = ACCEPT.
unfold result_narrowing.
intuition.
Qed.
Lemma result_push_reject: forall x, result_narrowing REJECT x -> x = REJECT.
unfold result_narrowing.
intuition.
Qed.
Parameter compute: nat (* program *) -> nat (* input *) -> nat (* steps *) -> result.
Axiom compute_narrowing:
forall program input steps steps',
(steps' >= steps) -> (result_narrowing (compute program input steps) (compute program input steps')).
Require Import Classical.
Lemma compute_non_divergent:
forall program input steps steps',
(compute program input steps) = ACCEPT ->
(compute program input steps') = REJECT ->
False.
intros.
assert (T := (classic (steps' >= steps))).
destruct T.
assert (T := (compute_narrowing program input steps steps')).
mp_cancel.
rewrite H, H0 in T.
unfold result_narrowing in T.
discriminate T.
unfold not in H1.
assert (T := (classic (steps' = steps))).
destruct T.
rewrite H2 in H0.
rewrite H in H0.
discriminate.
assert (steps >= steps').
omega.
assert (T := (compute_narrowing program input steps' steps)).
mp_cancel.
rewrite H, H0 in T.
unfold result_narrowing in T.
discriminate.
Qed.
Definition procedure_type := nat (* input *) -> nat (* depth *) -> result.
Definition procedure_narrowing (procedure : procedure_type) : Prop :=
forall input depth depth',
(depth' >= depth) -> (result_narrowing (procedure input depth) (procedure input depth')).
Parameter program_of_procedure: procedure_type (* procedure *) -> nat (* program *).
Axiom program_of_procedure_behavior:
forall procedure : procedure_type,
(procedure_narrowing procedure) ->
forall input,
(
forall depth,
exists steps,
(result_narrowing (procedure input depth) (compute (program_of_procedure procedure) input steps))
) /\
(
forall steps,
exists depth,
(result_narrowing (compute (program_of_procedure procedure) input steps) (procedure input depth))
).
Definition program_halts_on_input (program : nat) (input : nat) : Prop :=
(exists steps, (compute program input steps) <> NOTYET).
(* orv = oracle verifier *)
Definition orv_type := nat (* query *) -> nat (* wisdom *) -> bool (* advice *).
Definition oracle_accepts (oracle : orv_type) (query : nat) :=
exists wisdom, (oracle query wisdom) = true.
Definition oracle_rejects (orv : orv_type) (inp : nat) := (~ (oracle_accepts orv inp)).
(* pwo = procedure with oracle *)
Inductive pwo_out :=
| PWO_RESULT : bool (* result *) -> pwo_out
| PWO_ORACLE : nat (* state *) -> nat (* query *) -> pwo_out
.
Definition pwo_type := nat (* input *) -> nat (* state *) -> bool (* advice *) -> pwo_out.
Inductive pwo_entails: orv_type (* oracle *) -> pwo_type (* procedure *) -> nat (* input *) -> nat (* state *) -> bool (* advice *) -> bool (* result *) -> Prop :=
| PwoEntailsResult:
forall oracle procedure input state advice result,
(procedure input state advice) = (PWO_RESULT result) ->
(pwo_entails oracle procedure input state advice result)
| PwoEntailsOracleAccept:
forall oracle procedure input state advice result state' query,
(procedure input state advice) = (PWO_ORACLE state' query) ->
(oracle_accepts oracle query) ->
(pwo_entails oracle procedure input state' true result) ->
(pwo_entails oracle procedure input state advice result)
| PwoEntailsOracleReject:
forall oracle procedure input state advice result state' query,
(procedure input state advice) = (PWO_ORACLE state' query) ->
(oracle_rejects oracle query) ->
(pwo_entails oracle procedure input state' false result) ->
(pwo_entails oracle procedure input state advice result)
.
Definition pwo_decider_relative (orv : orv_type) (pwo : pwo_type) :=
forall input,
(pwo_entails orv pwo input 0 false false) \/
(pwo_entails orv pwo input 0 false true).
(* define oracle for A_TM (turing machine accepts a particular input) *)
Definition orv_atm (pair_program_input : nat) (wisdom : nat) : bool :=
(match (decode_pair pair_program_input) with
| (target_program, target_input) =>
(match (compute target_program target_input wisdom) with
| ACCEPT => true
| _ => false
end)
end).
(* define procedure for H_TM (turing machine halts on a particular input) relative to an oracle for A_TM *)
Definition pwo_hfa_construction (target_program : nat) :=
(fun input depth =>
(match (compute target_program input depth) with
| ACCEPT => REJECT
| REJECT => ACCEPT
| NOTYET => NOTYET
end)).
Lemma pwo_hfa_construction_narrowing: forall target_program, (procedure_narrowing (pwo_hfa_construction target_program)).
intros.
unfold procedure_narrowing, result_narrowing, pwo_hfa_construction.
intros.
case_eq (compute target_program input depth); intro; try
(
case_eq (compute target_program input depth'); intro; try reflexivity; try
(
assert (T := (compute_narrowing target_program input depth depth'));
mp_cancel;
unfold result_narrowing in T;
rewrite H0 in T;
rewrite H1 in T;
discriminate
)
).
Qed.
Definition pwo_hfa (input : nat) (state : nat) (advice : bool) : pwo_out :=
(match (decode_pair input) with
| (target_program, target_input) =>
(match state with
| O =>
(PWO_ORACLE 1 (encode_pair (target_program, target_input)))
| (S O) =>
(if advice
then (PWO_RESULT true)
else (PWO_ORACLE 2 (encode_pair ((program_of_procedure (pwo_hfa_construction target_program)), target_input))))
| _ =>
(PWO_RESULT advice)
end)
end).
Lemma H_from_A:
exists pwo_hfa,
(pwo_decider_relative orv_atm pwo_hfa) /\
(
forall input,
(pwo_entails orv_atm pwo_hfa input 0 false true ->
(match (decode_pair input) with | (target_program, target_input) => ( (program_halts_on_input target_program target_input)) end)) /\
(pwo_entails orv_atm pwo_hfa input 0 false false ->
(match (decode_pair input) with | (target_program, target_input) => (~ (program_halts_on_input target_program target_input)) end))
)
.
exists pwo_hfa.
split.
{
unfold pwo_decider_relative.
intros.
pose (pair := (decode_pair input)).
case_eq (pair); intros target_program target_input H_pair.
replace input with (encode_pair (target_program, target_input)).
Focus 2.
{
rewrite <- H_pair.
unfold pair.
apply encode_decode.
}
Unfocus.
assert (T1 := (classic (oracle_accepts orv_atm (encode_pair (target_program, target_input))))).
destruct T1 as [T1 | T1].
{
right.
eapply PwoEntailsOracleAccept.
Focus 2.
eexact T1.
unfold pwo_hfa.
rewrite decode_encode.
instantiate (1 := 1).
reflexivity.
apply PwoEntailsResult.
unfold pwo_hfa.
rewrite decode_encode.
reflexivity.
}
{
assert (T2 := (classic (oracle_accepts orv_atm (encode_pair ((program_of_procedure (pwo_hfa_construction target_program)), target_input))))).
destruct T2 as [T2 | T2].
{
right.
eapply PwoEntailsOracleReject.
Focus 2.
unfold oracle_rejects.
eexact T1.
unfold pwo_hfa.
rewrite decode_encode.
instantiate (1 := 1).
reflexivity.
eapply PwoEntailsOracleAccept.
Focus 2.
eexact T2.
unfold pwo_hfa.
rewrite decode_encode.
instantiate (1 := 2).
reflexivity.
apply PwoEntailsResult.
unfold pwo_hfa.
rewrite decode_encode.
reflexivity.
}
{
left.
eapply PwoEntailsOracleReject.
Focus 2.
unfold oracle_rejects.
eexact T1.
unfold pwo_hfa.
rewrite decode_encode.
instantiate (1 := 1).
reflexivity.
eapply PwoEntailsOracleReject.
Focus 2.
eexact T2.
unfold pwo_hfa.
rewrite decode_encode.
instantiate (1 := 2).
reflexivity.
apply PwoEntailsResult.
unfold pwo_hfa.
rewrite decode_encode.
reflexivity.
}
}
}
{
intros.
case_eq (decode_pair input); intros target_program target_input H_input.
replace input with (encode_pair (target_program, target_input)).
Focus 2.
{
rewrite <- H_input.
rewrite encode_decode.
reflexivity.
}
Unfocus.
clear H_input.
split.
{
intros.
inversion H; subst.
{
unfold pwo_hfa in H0.
rewrite decode_encode in H0.
discriminate H0.
}
{
unfold pwo_hfa in H0.
rewrite decode_encode in H0.
injection H0.
intros.
rewrite <- H3 in H1.
unfold oracle_accepts in H1.
unfold program_halts_on_input.
elim H1; intros.
exists x.
unfold orv_atm in H5.
rewrite decode_encode in H5.
destruct (compute target_program target_input x); try intuition; try discriminate.
}
{
unfold pwo_hfa in H0.
rewrite decode_encode in H0.
injection H0.
intros.
rewrite <- H4 in *.
inversion H2; subst.
{
unfold pwo_hfa in H5.
rewrite decode_encode in H5.
discriminate.
}
{
unfold pwo_hfa in H5.
rewrite decode_encode in H5.
injection H5; intros.
subst.
unfold oracle_accepts in H6.
unfold program_halts_on_input.
elim H6; intros.
unfold orv_atm in H3.
rewrite decode_encode in H3.
case_eq (compute (program_of_procedure (pwo_hfa_construction target_program)) target_input x); intros; rewrite H4 in H3; try discriminate.
assert
(T :=
(program_of_procedure_behavior
(pwo_hfa_construction target_program)
(pwo_hfa_construction_narrowing target_program)
target_input
)).
destruct T.
specialize H9 with x.
elim H9; intros.
assert ((pwo_hfa_construction target_program target_input x0) = ACCEPT).
eapply result_push_accept.
rewrite <- H4.
assumption.
unfold pwo_hfa_construction in H11.
case_eq (compute target_program target_input x0); intros; rewrite H12 in H11; try discriminate.
exists x0.
unfold not.
intros.
rewrite H12 in H13.
discriminate.
}
{
unfold pwo_hfa in H5.
rewrite decode_encode in H5.
injection H5; intros.
subst.
inversion H7.
unfold pwo_hfa in H3.
rewrite decode_encode in H3.
discriminate H3.
unfold pwo_hfa in H3.
rewrite decode_encode in H3.
discriminate H3.
unfold pwo_hfa in H3.
rewrite decode_encode in H3.
discriminate H3.
}
}
}
{
intros.
unfold not.
intros.
inversion H; subst; unfold pwo_hfa in H1; rewrite decode_encode in H1; try discriminate; injection H1; intros; subst.
{
inversion H3; subst; unfold pwo_hfa in H4; rewrite decode_encode in H4; try discriminate; injection H4; intros; subst.
}
{
inversion H3; subst; unfold pwo_hfa in H4; rewrite decode_encode in H4; try discriminate; injection H4; intros; subst.
{
inversion H6; subst; unfold pwo_hfa in H7; rewrite decode_encode in H7; try discriminate.
}
{
(* oracle rejected both on a program that halts *)
clear H H3 H1 H6 H4.
unfold program_halts_on_input in H0.
elim H0; clear H0; intros.
unfold not in H.
case_eq (compute target_program target_input x); intros; try ( solve [ intuition ] ).
{
rename H2 into HH.
unfold oracle_rejects, not in HH.
apply HH.
clear HH.
unfold oracle_accepts.
exists x.
unfold orv_atm.
rewrite decode_encode.
rewrite H0.
reflexivity.
}
{
rename H5 into HH.
unfold oracle_rejects, not in HH.
apply HH.
clear HH.
unfold oracle_accepts.
assert
(T :=
(program_of_procedure_behavior
(pwo_hfa_construction target_program)
(pwo_hfa_construction_narrowing target_program)
target_input
)).
destruct T.
assert ((pwo_hfa_construction target_program target_input x) = ACCEPT).
unfold pwo_hfa_construction.
rewrite H0.
reflexivity.
specialize H1 with x.
elim H1; intros.
rewrite H4 in H5.
unfold result_narrowing in H5.
exists x0.
unfold orv_atm.
rewrite decode_encode.
rewrite H5.
reflexivity.
}
}
}
}
}
Qed.