Theory TuringComputable
section ‹Turing Computable Functions›
theory TuringComputable
imports
"HaltingProblems_K_H"
begin
subsection ‹Definition of Partial Turing Computability›
text ‹We present two variants for a definition of Partial Turing Computability,
which we prove to be equivalent, later on.›
subsubsection ‹Definition Variant 1›
definition turing_computable_partial :: "(nat list ⇒ nat option) ⇒ bool"
where "turing_computable_partial f ≡ (∃tm. ∀ns n.
(f ns = Some n ⟶ (∃stp k l. (steps0 (1, ([], <ns::nat list>)) tm stp) = (0, Bk ↑ k, <n::nat> @ Bk ↑ l))) ∧
(f ns = None ⟶ ¬⦃ λtap. tap = ([], <ns>) ⦄ tm ⦃ λtap. (∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)) ⦄))"
lemma turing_computable_partial_unfolded_into_TMC_yields_TMC_has_conditions:
"turing_computable_partial f ≡ (∃tm. ∀ns n.
(f ns = Some n ⟶ TMC_yields_num_res tm ns n) ∧
(f ns = None ⟶ ¬ TMC_has_num_res tm ns ) )"
unfolding TMC_yields_num_res_def TMC_has_num_res_def
by (simp add: turing_computable_partial_def)
lemma turing_computable_partial_unfolded_into_Hoare_halt_conditions:
"turing_computable_partial f ⟷ (∃tm. ∀ns n.
(f ns = Some n ⟶ ⦃ λtap. tap = ([], <ns::nat list>) ⦄ tm ⦃ λtap. ∃k l. tap = (Bk ↑ k, <n::nat> @ Bk↑ l) ⦄ ) ∧
(f ns = None ⟶ ¬⦃ λtap. tap = ([], <ns::nat list>) ⦄ tm ⦃ λtap. ∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l) ⦄))"
unfolding turing_computable_partial_def
proof
assume "∃tm. ∀ns n. (f ns = Some n ⟶ (∃stp k l. steps0 (1, [], <ns::nat list>) tm stp = (0, Bk ↑ k, <n::nat> @ Bk ↑ l))) ∧
(f ns = None ⟶ ¬ ⦃ λtap. tap = ([], <ns::nat list>) ⦄ tm ⦃ λtap. ∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l) ⦄)"
then obtain tm where
w_tm1:"∀ns n. (f ns = Some n ⟶ (∃stp k l. steps0 (1, [], <ns::nat list>) tm stp = (0, Bk ↑ k, <n::nat> @ Bk ↑ l))) ∧
(f ns = None ⟶ ¬ ⦃ λtap. tap = ([], <ns::nat list>) ⦄ tm ⦃ λtap. ∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l) ⦄)"
by blast
have "∀ns n. (f ns = Some n ⟶ ⦃λtap. tap = ([], <ns::nat list>)⦄ tm ⦃λtap. ∃k l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)⦄) ∧
(f ns = None ⟶ ¬ ⦃ λtap. tap = ([], <ns::nat list>) ⦄ tm ⦃ λtap. ∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l) ⦄)"
apply (safe)
proof -
show "⋀ns n. f ns = Some n ⟹ ⦃λtap. tap = ([], <ns>)⦄ tm ⦃λtap. ∃k l. tap = (Bk ↑ k, <n> @ Bk ↑ l)⦄"
proof -
fix ns n
assume "f ns = Some n"
with w_tm1 have F1: "∃stp k l. steps0 (1, [], <ns::nat list>) tm stp = (0, Bk ↑ k, <n::nat> @ Bk ↑ l)" by auto
show "⦃λtap. tap = ([], <ns::nat list>)⦄ tm ⦃λtap. ∃k l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)⦄"
proof (rule Hoare_haltI)
fix l r
assume "(l, r) = ([]::cell list, <ns::nat list>)"
then show "∃stp. is_final (steps0 (1, l, r) tm stp) ∧ (λtap. ∃k l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)) holds_for steps0 (1, l, r) tm stp"
by (metis (mono_tags, lifting) F1 holds_for.simps is_finalI)
qed
qed
next
show "⋀ns n. ⟦f ns = None; ⦃λtap. tap = ([], <ns>)⦄ tm ⦃λtap. ∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)⦄ ⟧ ⟹ False"
proof -
fix ns n
assume "f ns = None" and "⦃λtap. tap = ([], <ns>)⦄ tm ⦃λtap. ∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)⦄"
with w_tm1 show False
by simp
qed
qed
then show "∃tm. ∀ns n. (f ns = Some n ⟶ ⦃λtap. tap = ([], <ns>)⦄ tm ⦃λtap. ∃k l. tap = (Bk ↑ k, <n> @ Bk ↑ l)⦄) ∧
(f ns = None ⟶ ¬ ⦃λtap. tap = ([], <ns>)⦄ tm ⦃λtap. ∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)⦄)"
by auto
next
assume "∃tm. ∀ns n. (f ns = Some n ⟶ ⦃λtap. tap = ([], <ns::nat list>)⦄ tm ⦃λtap. ∃k l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)⦄) ∧
(f ns = None ⟶ ¬ ⦃λtap. tap = ([], <ns>)⦄ tm ⦃λtap. ∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)⦄)"
then obtain tm where
w_tm2: "∀ns n. (f ns = Some n ⟶ ⦃λtap. tap = ([], <ns::nat list>)⦄ tm ⦃λtap. ∃k l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)⦄) ∧
(f ns = None ⟶ ¬ ⦃λtap. tap = ([], <ns>)⦄ tm ⦃λtap. ∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)⦄)"
by blast
have "∀ns n. (f ns = Some n ⟶ (∃stp k l. steps0 (1, [], <ns::nat list>) tm stp = (0, Bk ↑ k, <n::nat> @ Bk ↑ l))) ∧
(f ns = None ⟶ ¬ ⦃λtap. tap = ([], <ns>)⦄ tm ⦃λtap. ∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)⦄)"
apply (safe)
proof -
show "⋀ns n . f ns = Some n ⟹ ∃stp k l. steps0 (1, [], <ns>) tm stp = (0, Bk ↑ k, <n> @ Bk ↑ l)"
proof -
fix ns n z
assume "f ns = Some n"
with w_tm2 have "⦃λtap. tap = ([], <ns::nat list>)⦄ tm ⦃λtap. ∃k l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)⦄" by blast
then show "∃stp k l. steps0 (1, [], <ns::nat list>) tm stp = (0, Bk ↑ k, <n::nat> @ Bk ↑ l)"
by (smt (verit) Hoare_halt_def holds_for.elims(2) is_final.elims(2) snd_conv)
qed
next
show "⋀ns n. ⟦f ns = None; ⦃λtap. tap = ([], <ns>)⦄ tm ⦃λtap. ∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)⦄⟧ ⟹ False"
proof -
fix ns n
assume "f ns = None" and "⦃λtap. tap = ([], <ns>)⦄ tm ⦃λtap. ∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)⦄"
with w_tm2 show False
by simp
qed
qed
then
show "∃tm. ∀ns n. (f ns = Some n ⟶ (∃stp k l. steps0 (1, [], <ns::nat list>) tm stp = (0, Bk ↑ k, <n::nat> @ Bk ↑ l))) ∧
(f ns = None ⟶ ¬ ⦃λtap. tap = ([], <ns>)⦄ tm ⦃λtap. ∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)⦄)"
by blast
qed
subsubsection ‹Characteristic Functions of Sets›
definition chi_fun :: "(nat list) set ⇒ (nat list ⇒ nat option)"
where
"chi_fun nls = (λnl. if nl ∈ nls then Some 1 else Some 0)"
lemma chi_fun_0_iff: "nl ∉ nls ⟷ chi_fun nls nl = Some 0"
unfolding chi_fun_def by auto
lemma chi_fun_1_iff: "nl ∈ nls ⟷ chi_fun nls nl = Some 1"
unfolding chi_fun_def by auto
lemma chi_fun_0_I: "nl ∉ nls ⟹ chi_fun nls nl = Some 0"
unfolding chi_fun_def by auto
lemma chi_fun_0_E: "(chi_fun nls nl = Some 0 ⟹ P) ⟹ nl ∉ nls ⟹ P"
unfolding chi_fun_def by auto
lemma chi_fun_1_I: "nl ∈ nls ⟹ chi_fun nls nl = Some 1"
unfolding chi_fun_def by auto
lemma chi_fun_1_E: "(chi_fun nls nl = Some 1 ⟹ P) ⟹ nl ∈ nls ⟹ P"
unfolding chi_fun_def by auto
subsubsection ‹Relation between Partial Turing Computability and Turing Decidability›
text ‹If a set A is Turing Decidable its characteristic function is Turing Computable partial and vice versa.
Please note, that although the characteristic function has an option type it will always yield Some value.
›
theorem turing_decidable_imp_turing_computable_partial:
"turing_decidable A ⟹ turing_computable_partial (chi_fun A)"
proof -
assume "turing_decidable A"
then have
"(∃D. (∀nl.
(nl ∈ A ⟶ ⦃(λtap. tap = ([], <nl>))⦄ D ⦃(λtap. ∃k l. tap = (Bk ↑ k, <1::nat> @ Bk↑ l))⦄)
∧ (nl ∉ A ⟶ ⦃(λtap. tap = ([], <nl>))⦄ D ⦃(λtap. ∃k l. tap = (Bk ↑ k, <0::nat> @ Bk↑ l))⦄)
))"
unfolding turing_decidable_def by auto
then obtain D where w_D:
"(∀nl.
(nl ∈ A ⟶ ⦃(λtap. tap = ([], <nl>))⦄ D ⦃(λtap. ∃k l. tap = (Bk ↑ k, <1::nat> @ Bk↑ l))⦄)
∧ (nl ∉ A ⟶ ⦃(λtap. tap = ([], <nl>))⦄ D ⦃(λtap. ∃k l. tap = (Bk ↑ k, <0::nat> @ Bk↑ l))⦄)
)" by blast
then have F1:
"(∀nl.
(chi_fun A nl = Some 1 ⟶ ⦃(λtap. tap = ([], <nl>))⦄ D ⦃(λtap. ∃k l. tap = (Bk ↑ k, <1::nat> @ Bk↑ l))⦄)
∧ (chi_fun A nl = Some 0 ⟶ ⦃(λtap. tap = ([], <nl>))⦄ D ⦃(λtap. ∃k l. tap = (Bk ↑ k, <0::nat> @ Bk↑ l))⦄)
)" using chi_fun_def by force
have F2: "∀nl. (chi_fun A nl = Some 1 ∨ chi_fun A nl = Some 0)" using chi_fun_def
by simp
show ?thesis
proof (rule turing_computable_partial_unfolded_into_Hoare_halt_conditions[THEN iffD2])
have "∀ns n. (chi_fun A ns = Some n ⟶ ⦃λtap. tap = ([], <ns>)⦄ D ⦃λtap. ∃k l. tap = (Bk ↑ k, <n> @ Bk ↑ l)⦄) ∧
(chi_fun A ns = None ⟶ ¬ ⦃λtap. tap = ([], <ns>)⦄ D ⦃λtap. ∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)⦄)"
apply (safe)
proof -
show "⋀ns n. chi_fun A ns = Some n ⟹ ⦃λtap. tap = ([], <ns>)⦄ D ⦃λtap. ∃k l. tap = (Bk ↑ k, <n> @ Bk ↑ l)⦄"
proof -
fix ns :: "nat list" and n :: nat
assume "chi_fun A ns = Some n"
then have "Some n = Some 1 ∨ Some n = Some 0"
by (metis F2)
then show "⦃λtap. tap = ([], <ns>)⦄ D ⦃λtap. ∃k l. tap = (Bk ↑ k, <n> @ Bk ↑ l)⦄"
using ‹chi_fun A ns = Some n› F1 by blast
qed
next
show " ⋀ns n. ⟦chi_fun A ns = None; ⦃λtap. tap = ([], <ns>)⦄ D ⦃λtap. ∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)⦄ ⟧ ⟹ False"
by (metis F2 option.distinct(1))
qed
then show "∃tm. ∀ns n.
(chi_fun A ns = Some n ⟶ ⦃λtap. tap = ([], <ns>)⦄ tm ⦃λtap. ∃k l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)⦄) ∧
(chi_fun A ns = None ⟶ ¬ ⦃λtap. tap = ([], <ns>)⦄ tm ⦃λtap. ∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)⦄)"
using F2 option.simps(3) by blast
qed
qed
theorem turing_computable_partial_imp_turing_decidable:
"turing_computable_partial (chi_fun A) ⟹ turing_decidable A"
proof -
assume "turing_computable_partial (chi_fun A)"
then have "∃tm. ∀ns n.
(chi_fun A ns = Some n ⟶ ⦃λtap. tap = ([], <ns::nat list>)⦄ tm ⦃λtap. ∃k l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)⦄) ∧
(chi_fun A ns = None ⟶ ¬ ⦃ λtap. tap = ([], <ns>) ⦄ tm ⦃ λtap. (∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)) ⦄ )"
using turing_computable_partial_unfolded_into_Hoare_halt_conditions[THEN iffD1] by auto
then obtain tm where w_tm: "∀ns n.
(chi_fun A ns = Some n ⟶ ⦃λtap. tap = ([], <ns::nat list>)⦄ tm ⦃λtap. ∃k l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)⦄) ∧
(chi_fun A ns = None ⟶ ¬ ⦃ λtap. tap = ([], <ns>) ⦄ tm ⦃ λtap. (∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)) ⦄)"
by auto
then have "∀ns.
(ns ∈ A ⟶ ⦃λtap. tap = ([], <ns::nat list>)⦄ tm ⦃λtap. ∃k l. tap = (Bk ↑ k, <1::nat> @ Bk ↑ l)⦄) ∧
(ns ∉ A ⟶ ⦃λtap. tap = ([], <ns::nat list>)⦄ tm ⦃λtap. ∃k l. tap = (Bk ↑ k, <0::nat> @ Bk ↑ l)⦄)"
by (blast intro: chi_fun_0_I chi_fun_1_I)
then have "(∃D.(∀ns.
(ns ∈ A ⟶ ⦃λtap. tap = ([], <ns::nat list>)⦄ tm ⦃λtap. ∃k l. tap = (Bk ↑ k, <1::nat> @ Bk ↑ l)⦄) ∧
(ns ∉ A ⟶ ⦃λtap. tap = ([], <ns::nat list>)⦄ tm ⦃λtap. ∃k l. tap = (Bk ↑ k, <0::nat> @ Bk ↑ l)⦄) ))"
by auto
then show ?thesis using turing_decidable_def by auto
qed
corollary turing_computable_partial_iff_turing_decidable:
"turing_decidable A ⟷ turing_computable_partial (chi_fun A)"
by (auto simp add: turing_computable_partial_imp_turing_decidable turing_decidable_imp_turing_computable_partial)
subsubsection ‹Examples for uncomputable functions›
text ‹Now, we prove that the characteristic functions of the undecidable sets K1 and H1 are both uncomputable.›
context hpk
begin
theorem "¬(turing_computable_partial (chi_fun K1))"
using not_Turing_decidable_K1 turing_computable_partial_imp_turing_decidable by blast
theorem "¬(turing_computable_partial (chi_fun H1))"
using not_Turing_decidable_H1 turing_computable_partial_imp_turing_decidable by blast
end
subsubsection ‹The Function associated with a Turing Machine›
text ‹With every Turing machine, we can associate a function.›
definition fun_of_tm :: "tprog0 ⇒ (nat list ⇒ nat option)"
where "fun_of_tm tm ns ≡
(if ⦃ λtap. tap = ([], <ns>) ⦄ tm ⦃ λtap. (∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)) ⦄
then
let result =
(THE n. ∃stp k l. (steps0 (1, ([], <ns>)) tm stp) = (0, Bk ↑ k, <n::nat> @ Bk ↑ l))
in Some result
else None)"
text ‹Some immediate consequences of the definition.›
lemma fun_of_tm_unfolded_into_TMC_yields_TMC_has_conditions:
"fun_of_tm tm ≡
(λns. (if TMC_has_num_res tm ns
then
let result = (THE n. TMC_yields_num_res tm ns n)
in Some result
else None)
)"
unfolding TMC_yields_num_res_def TMC_has_num_res_def
using fun_of_tm_def by presburger
lemma fun_of_tm_is_None:
assumes "¬(⦃ λtap. tap = ([], <ns>) ⦄ tm ⦃ λtap. (∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)) ⦄)"
shows "fun_of_tm tm ns = None"
proof -
from assms show "fun_of_tm tm ns = None" by (auto simp add: fun_of_tm_def)
qed
lemma fun_of_tm_is_None_rev:
assumes "fun_of_tm tm ns = None"
shows "¬(⦃ λtap. tap = ([], <ns>) ⦄ tm ⦃ λtap. (∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)) ⦄)"
using assms fun_of_tm_def by auto
corollary fun_of_tm_is_None_iff: "fun_of_tm tm ns = None ⟷ ¬(⦃ λtap. tap = ([], <ns>) ⦄ tm ⦃ λtap. (∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)) ⦄)"
by (auto simp add: fun_of_tm_is_None fun_of_tm_is_None_rev)
corollary fun_of_tm_is_None_iff': "fun_of_tm tm ns = None ⟷ ¬ TMC_has_num_res tm ns"
unfolding TMC_has_num_res_def
by (auto simp add: fun_of_tm_is_None fun_of_tm_is_None_rev )
lemma fun_of_tm_ex_Some_n':
assumes "⦃ λtap. tap = ([], <ns>) ⦄ tm ⦃ λtap. (∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)) ⦄"
shows "∃n. fun_of_tm tm ns = Some n"
using assms fun_of_tm_def by auto
lemma fun_of_tm_ex_Some_n'_rev:
assumes "∃n. fun_of_tm tm ns = Some n"
shows "⦃ λtap. tap = ([], <ns>) ⦄ tm ⦃ λtap. (∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)) ⦄"
using assms fun_of_tm_is_None by fastforce
corollary fun_of_tm_ex_Some_n'_iff:
"(∃n. fun_of_tm tm ns = Some n)
⟷
⦃ λtap. tap = ([], <ns>) ⦄ tm ⦃ λtap. (∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)) ⦄"
by (auto simp add: fun_of_tm_ex_Some_n' fun_of_tm_ex_Some_n'_rev)
subsubsection ‹Stronger results about uniqueness of results›
corollary Hoare_halt_on_numeral_list_yields_unique_list_result_iff:
"⦃λtap. tap = ([], <nl::nat list>)⦄ p ⦃λtap. ∃kr ml lr. tap = (Bk ↑ kr, <ml::nat list> @ Bk ↑ lr)⦄
⟷
(∃!ml. ∃stp k l. steps0 (1,[], <nl::nat list>) p stp = (0, Bk ↑ k, <ml::nat list> @ Bk ↑ l))"
proof
assume A: "⦃λtap. tap = ([], <nl::nat list>)⦄ p ⦃λtap. ∃kr ml lr. tap = (Bk ↑ kr, <ml::nat list> @ Bk ↑ lr)⦄"
show "∃!ml. ∃stp k l. steps0 (1, [], <nl::nat list>) p stp = (0, Bk ↑ k, <ml::nat list> @ Bk ↑ l)"
proof (rule ex_ex1I)
show "∃ml stp k l. steps0 (1, [], <nl::nat list>) p stp = (0, Bk ↑ k, <ml::nat list> @ Bk ↑ l)"
using A
using Hoare_halt_iff by auto
next
show "⋀ml y. ⟦∃stp k l. steps0 (1, [], <nl::nat list>) p stp = (0, Bk ↑ k, <ml::nat list> @ Bk ↑ l);
∃stp k l. steps0 (1, [], <nl::nat list>) p stp = (0, Bk ↑ k, <y::nat list> @ Bk ↑ l)⟧ ⟹ ml = y"
by (metis nat_le_linear prod.inject prod.inject stable_config_after_final_ge' unique_Bk_postfix_numeral_list)
qed
next
assume "(∃!ml. ∃stp k l. steps0 (1,[], <nl::nat list>) p stp = (0, Bk ↑ k, <ml::nat list> @ Bk ↑ l))"
then show "⦃λtap. tap = ([], <nl::nat list>)⦄ p ⦃λtap. ∃kr ml lr. tap = (Bk ↑ kr, <ml::nat list> @ Bk ↑ lr)⦄"
using Hoare_halt_on_numeral_imp_list_result_rev by blast
qed
corollary Hoare_halt_on_numeral_yields_unique_result_iff:
"⦃(λtap. tap = ([], <ns::nat list>))⦄ p ⦃(λtap. (∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)))⦄
⟷
(∃!n. ∃stp k l. steps0 (1,[], <ns::nat list>) p stp = (0, Bk ↑ k, <n::nat> @ Bk ↑ l))"
proof
assume A: "⦃λtap. tap = ([], <ns::nat list>)⦄ p ⦃λtap. ∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)⦄"
show "∃!n. ∃stp k l. steps0 (1, [], <ns::nat list>) p stp = (0, Bk ↑ k, <n::nat> @ Bk ↑ l)"
proof (rule ex_ex1I)
show "∃n stp k l. steps0 (1, [], <ns::nat list>) p stp = (0, Bk ↑ k, <n::nat> @ Bk ↑ l)"
using A
using Hoare_halt_on_numeral_imp_result by blast
next
show "⋀n y. ⟦∃stp k l. steps0 (1, [], <ns::nat list>) p stp = (0, Bk ↑ k, <n::nat> @ Bk ↑ l);
∃stp k l. steps0 (1, [], <ns>) p stp = (0, Bk ↑ k, <y> @ Bk ↑ l)⟧ ⟹ n = y"
by (smt (verit) before_final is_final_eq le_less least_steps less_Suc_eq not_less_iff_gr_or_eq snd_conv unique_decomp_std_tap)
qed
next
assume "∃!n. ∃stp k l. steps0 (1, [], <ns::nat list>) p stp = (0, Bk ↑ k, <n::nat> @ Bk ↑ l)"
then show "⦃λtap. tap = ([], <ns::nat list>)⦄ p ⦃λtap. ∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)⦄"
using Hoare_halt_on_numeral_imp_result_rev by blast
qed
lemma fun_of_tm_is_Some_unique_value:
assumes "steps0 (1, ([], <ns>)) tm stp = (0, Bk ↑ k1, <n::nat> @ Bk ↑ l1)"
shows "fun_of_tm tm ns = Some n"
proof -
from assms have F0: "TMC_has_num_res tm ns"
using Hoare_halt_on_numeral_imp_result_rev TMC_has_num_res_def by blast
then have
"fun_of_tm tm ns = (
let result =
(THE n. ∃stp k l. (steps0 (1, ([], <ns>)) tm stp) = (0, Bk ↑ k, <n::nat> @ Bk ↑ l))
in Some result)"
by (simp add: F0 TMC_has_num_res_def fun_of_tm_def fun_of_tm_ex_Some_n' )
then have F1: "fun_of_tm tm ns =
Some (THE n. ∃stp k l. (steps0 (1, ([], <ns>)) tm stp) = (0, Bk ↑ k, <n::nat> @ Bk ↑ l))"
by auto
have "(THE n. ∃stp k l. (steps0 (1, ([], <ns>)) tm stp) = (0, Bk ↑ k, <n::nat> @ Bk ↑ l)) = n"
proof (rule the1I2)
from F0
have F2: "(∃!n.∃stp k l. (steps0 (1, ([], <ns>)) tm stp) = (0, Bk ↑ k, <n::nat> @ Bk ↑ l))"
using Hoare_halt_on_numeral_imp_result_rev Hoare_halt_on_numeral_yields_unique_result_iff assms by blast
then
show "∃!n. ∃stp k l. steps0 (1, [], <ns::nat list>) tm stp = (0, Bk ↑ k, <n::nat> @ Bk ↑ l)"
by auto
next
show "⋀x. ∃stp k l. steps0 (1, [], <ns>) tm stp = (0, Bk ↑ k, <x> @ Bk ↑ l) ⟹ x = n"
using Hoare_halt_on_numeral_imp_result_rev Hoare_halt_on_numeral_yields_unique_result_iff assms by blast
qed
then show ?thesis
using F1 by blast
qed
lemma fun_of_tm_ex_Some_n:
assumes "⦃ λtap. tap = ([], <ns::nat list>) ⦄ tm ⦃ λtap. (∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)) ⦄"
shows "∃stp k n l. (steps0 (1, ([], <ns::nat list>)) tm stp) = (0, Bk ↑ k, <n::nat> @ Bk ↑ l) ∧
fun_of_tm tm ns = Some (n::nat)"
using Hoare_halt_on_numeral_imp_result assms fun_of_tm_is_Some_unique_value by blast
lemma fun_of_tm_ex_Some_n_rev:
assumes "∃stp k n l. (steps0 (1, ([], <ns::nat list>)) tm stp) = (0, Bk ↑ k, <n::nat> @ Bk ↑ l) ∧
fun_of_tm tm ns = Some n"
shows "⦃ λtap. tap = ([], <ns::nat list>) ⦄ tm ⦃ λtap. (∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)) ⦄"
proof -
from assms have "∃stp k n l. steps0 (1, [], <ns::nat list>) tm stp = (0, Bk ↑ k, <n::nat> @ Bk ↑ l)"
by blast
then show ?thesis
using Hoare_haltE Hoare_haltI assms fun_of_tm_ex_Some_n'_rev steps.simps(1)
by auto
qed
corollary fun_of_tm_ex_Some_n_iff:
"(∃stp k n l. (steps0 (1, ([], <ns>)) tm stp) = (0, Bk ↑ k, <n::nat> @ Bk ↑ l) ∧
fun_of_tm tm ns = Some n)
⟷
⦃ λtap. tap = ([], <ns::nat list>) ⦄ tm ⦃ λtap. (∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)) ⦄"
using fun_of_tm_ex_Some_n fun_of_tm_ex_Some_n_rev
by blast
lemma fun_of_tm_eq_Some_n_imp_same_numeral_result:
assumes "fun_of_tm tm ns = Some n"
shows "∃stp k l. steps0 (1, [], <ns::nat list>) tm stp = (0, Bk ↑ k, <n::nat> @ Bk ↑ l)"
by (metis (no_types, lifting) assms assms fun_of_tm_def fun_of_tm_ex_Some_n_iff fun_of_tm_is_None option.inject option.simps(3))
lemma numeral_result_n_imp_fun_of_tm_eq_n:
assumes "∃stp k l. steps0 (1, [], <ns::nat list>) tm stp = (0, Bk ↑ k, <n::nat> @ Bk ↑ l)"
shows "fun_of_tm tm ns = Some n"
using assms fun_of_tm_is_Some_unique_value by blast
corollary numeral_result_n_iff_fun_of_tm_eq_n:
"fun_of_tm tm ns = Some n
⟷
(∃stp k l. steps0 (1, [], <ns::nat list>) tm stp = (0, Bk ↑ k, <n::nat> @ Bk ↑ l))"
using fun_of_tm_eq_Some_n_imp_same_numeral_result numeral_result_n_imp_fun_of_tm_eq_n
by blast
corollary numeral_result_n_iff_fun_of_tm_eq_n':
"fun_of_tm tm ns = Some n ⟷ TMC_yields_num_res tm ns n"
using fun_of_tm_eq_Some_n_imp_same_numeral_result numeral_result_n_imp_fun_of_tm_eq_n
unfolding TMC_yields_num_res_def
by blast
subsubsection ‹Definition of Turing computability Variant 2›
definition turing_computable_partial' :: "(nat list ⇒ nat option) ⇒ bool"
where "turing_computable_partial' f ≡ ∃tm. fun_of_tm tm = f"
lemma turing_computable_partial'I:
"(⋀ns. fun_of_tm tm ns = f ns) ⟹ turing_computable_partial' f"
unfolding turing_computable_partial'_def
proof -
assume "(⋀ns. fun_of_tm tm ns = f ns)"
then have "fun_of_tm tm = f" by (rule ext)
then show "∃tm. fun_of_tm tm = f" by auto
qed
subsubsection ‹Definitional Variants 1 and 2 of Partial Turing Computability are equivalent›
text ‹Now, we prove the equivalence of the two definitions of Partial Turing Computability.›
lemma turing_computable_partial'_imp_turing_computable_partial:
"turing_computable_partial' f ⟶ turing_computable_partial f"
unfolding turing_computable_partial'_def turing_computable_partial_def
proof
assume "∃tm. fun_of_tm tm = f"
then obtain tm where w_tm: "fun_of_tm tm = f" by blast
show "∃tm. ∀ns n. (f ns = Some n ⟶ (∃stp k l. steps0 (1, [], <ns>) tm stp = (0, Bk ↑ k, <n::nat> @ Bk ↑ l))) ∧
(f ns = None ⟶ ¬ ⦃ λtap. tap = ([], <ns::nat list>) ⦄ tm ⦃ λtap. (∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)) ⦄)"
proof
show "∀ns n. (f ns = Some n ⟶ (∃stp k l. steps0 (1, [], <ns>) tm stp = (0, Bk ↑ k, <n::nat> @ Bk ↑ l))) ∧
(f ns = None ⟶ ¬ ⦃ λtap. tap = ([], <ns::nat list>) ⦄ tm ⦃ λtap. (∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)) ⦄)"
proof
fix ns
show "∀n. (f ns = Some n ⟶ (∃stp k l. steps0 (1, [], <ns>) tm stp = (0, Bk ↑ k, <n::nat> @ Bk ↑ l))) ∧
(f ns = None ⟶ ¬ ⦃ λtap. tap = ([], <ns::nat list>) ⦄ tm ⦃ λtap. (∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)) ⦄)"
proof
fix n::nat
show "(f ns = Some n ⟶ (∃stp k l. steps0 (1, [], <ns>) tm stp = (0, Bk ↑ k, <n> @ Bk ↑ l))) ∧
(f ns = None ⟶ ¬ ⦃ λtap. tap = ([], <ns::nat list>) ⦄ tm ⦃ λtap. (∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)) ⦄)"
proof
show "f ns = Some n ⟶ (∃stp k l. steps0 (1, [], <ns>) tm stp = (0, Bk ↑ k, <n> @ Bk ↑ l))"
proof
assume "f ns = Some n"
with w_tm have A: "fun_of_tm tm ns = Some n" by auto
then have "⦃ λtap. tap = ([], <ns::nat list>) ⦄ tm ⦃ λtap. (∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)) ⦄" using fun_of_tm_ex_Some_n'_rev by auto
then have "∃stp k m l. (steps0 (1, ([], <ns>)) tm stp) = (0, Bk ↑ k, <m::nat> @ Bk ↑ l) ∧
fun_of_tm tm ns = Some m"
by (rule fun_of_tm_ex_Some_n)
with A show "∃stp k l. steps0 (1, [], <ns>) tm stp = (0, Bk ↑ k, <n::nat> @ Bk ↑ l)" by auto
qed
next
show "f ns = None ⟶ ¬ ⦃ λtap. tap = ([], <ns::nat list>) ⦄ tm ⦃ λtap. (∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)) ⦄"
proof
assume "f ns = None"
with w_tm have A: "fun_of_tm tm ns = None" by auto
then show "¬(⦃ λtap. tap = ([], <ns::nat list>) ⦄ tm ⦃ λtap. (∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)) ⦄)" by (rule fun_of_tm_is_None_rev)
qed
qed
qed
qed
qed
qed
lemma turing_computable_partial_imp_turing_computable_partial':
"turing_computable_partial f ⟶ turing_computable_partial' f"
unfolding turing_computable_partial_def
proof
assume major: "∃tm. ∀ns n.
(f ns = Some n ⟶ (∃stp k l. steps0 (1, [], <ns>) tm stp = (0, Bk ↑ k, <n::nat> @ Bk ↑ l))) ∧
(f ns = None ⟶ ¬ ⦃ λtap. tap = ([], <ns::nat list>) ⦄ tm ⦃ λtap. (∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)) ⦄)"
show "turing_computable_partial' f"
proof -
from major obtain tm where w_tm:
"∀ns n. (f ns = Some n ⟶ (∃stp k l. steps0 (1, [], <ns>) tm stp = (0, Bk ↑ k, <n::nat> @ Bk ↑ l))) ∧
(f ns = None ⟶ ¬ ⦃ λtap. tap = ([], <ns::nat list>) ⦄ tm ⦃ λtap. (∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)) ⦄)" by blast
show "turing_computable_partial' f"
proof (rule turing_computable_partial'I)
show "⋀ns. fun_of_tm tm ns = f ns"
proof -
fix ns
show "fun_of_tm tm ns = f ns"
proof (cases "f ns")
case None
then have "f ns = None" .
with w_tm have "¬ ⦃ λtap. tap = ([], <ns::nat list>) ⦄ tm ⦃ λtap. (∃k n l. tap = (Bk ↑ k, <n::nat> @ Bk ↑ l)) ⦄" by auto
then have "fun_of_tm tm ns = None" by (rule fun_of_tm_is_None)
with ‹f ns = None› show ?thesis by auto
next
case (Some m)
then have "f ns = Some m" .
with w_tm have B: "(∃stp k l. steps0 (1, [], <ns>) tm stp = (0, Bk ↑ k, <m::nat> @ Bk ↑ l))" by auto
then obtain stp k l where w_stp_k_l: "steps0 (1, [], <ns>) tm stp = (0, Bk ↑ k, <m::nat> @ Bk ↑ l)" by blast
then have "∃stp k n l. (steps0 (1, ([], <ns>)) tm stp) = (0, Bk ↑ k, <n::nat> @ Bk ↑ l)" by blast
from this and w_stp_k_l have "fun_of_tm tm ns = Some m"
by (simp add: w_stp_k_l fun_of_tm_is_Some_unique_value)
with ‹f ns = Some m› show ?thesis by auto
qed
qed
qed
qed
qed
corollary turing_computable_partial'_turing_computable_partial_iff:
"turing_computable_partial' f ⟷ turing_computable_partial f"
by (auto simp add: turing_computable_partial'_imp_turing_computable_partial
turing_computable_partial_imp_turing_computable_partial')
text ‹As a now trivial consequence we obtain:›
corollary "turing_computable_partial f ≡ ∃tm. fun_of_tm tm = f"
using turing_computable_partial'_turing_computable_partial_iff turing_computable_partial'_def
by auto
subsection ‹Definition of Total Turing Computability›
definition turing_computable_total :: "(nat list ⇒ nat option) ⇒ bool"
where "turing_computable_total f ≡ (∃tm. ∀ns. ∃n.
f ns = Some n ∧
(∃stp k l. (steps0 (1, ([], <ns::nat list>)) tm stp) = (0, Bk ↑ k, <n::nat> @ Bk ↑ l)) )"
lemma turing_computable_total_unfolded_into_TMC_yields_condition:
"turing_computable_total f ≡ (∃tm. ∀ns. ∃n. f ns = Some n ∧ TMC_yields_num_res tm ns n )"
unfolding TMC_yields_num_res_def
by (simp add: turing_computable_total_def)
lemma turing_computable_total_imp_turing_computable_partial:
"turing_computable_total f ⟹ turing_computable_partial f"
unfolding turing_computable_total_def turing_computable_partial_def
by (metis option.inject option.simps(3))
corollary turing_decidable_imp_turing_computable_total_chi_fun:
"turing_decidable A ⟹ turing_computable_total (chi_fun A)"
unfolding turing_computable_total_unfolded_into_TMC_yields_condition
proof -
assume "turing_decidable A"
then have "∃D. (∀nl.
(nl ∈ A ⟶ TMC_yields_num_res D nl (1::nat) )
∧ (nl ∉ A ⟶ TMC_yields_num_res D nl (0::nat) ) )"
unfolding turing_decidable_unfolded_into_TMC_yields_conditions
by auto
then obtain D where
w_D: "∀nl. (nl ∈ A ⟶ TMC_yields_num_res D nl (1::nat) ) ∧
(nl ∉ A ⟶ TMC_yields_num_res D nl (0::nat) )"
by blast
then have "∀ns. ∃n. chi_fun A ns = Some n ∧ TMC_yields_num_res D ns n"
by (simp add: w_D chi_fun_0_E chi_fun_def)
then show "∃tm. ∀ns. ∃n. chi_fun A ns = Some n ∧ TMC_yields_num_res tm ns n"
by auto
qed
definition turing_computable_total' :: "(nat list ⇒ nat option) ⇒ bool"
where "turing_computable_total' f ≡ (∃tm. ∀ns. ∃n. f ns = Some n ∧ fun_of_tm tm = f)"
theorem turing_computable_total'_eq_turing_computable_total:
"turing_computable_total' f = turing_computable_total f"
proof
show "turing_computable_total' f ⟹ turing_computable_total f"
unfolding turing_computable_total_def unfolding turing_computable_total'_def
using fun_of_tm_eq_Some_n_imp_same_numeral_result by blast
next
show "turing_computable_total f ⟹ turing_computable_total' f"
unfolding turing_computable_total_def unfolding turing_computable_total'_def
by (metis numeral_result_n_imp_fun_of_tm_eq_n tape_of_list_def turing_computable_partial'I turing_computable_partial'_def)
qed
definition turing_computable_total'' :: "(nat list ⇒ nat option) ⇒ bool"
where "turing_computable_total'' f ≡ (∃tm. fun_of_tm tm = f ∧ (∀ns. ∃n. f ns = Some n))"
theorem turing_computable_total''_eq_turing_computable_total:
"turing_computable_total'' f = turing_computable_total f"
proof
show "turing_computable_total'' f ⟹ turing_computable_total f"
unfolding turing_computable_total_def unfolding turing_computable_total''_def
by (meson fun_of_tm_eq_Some_n_imp_same_numeral_result)
next
show "turing_computable_total f ⟹ turing_computable_total'' f"
unfolding turing_computable_total_def unfolding turing_computable_total''_def
by (metis numeral_result_n_imp_fun_of_tm_eq_n tape_of_list_def turing_computable_partial'I turing_computable_partial'_def)
qed
definition turing_computable_total_on :: "(nat list ⇒ nat option) ⇒ (nat list) set ⇒ bool"
where "turing_computable_total_on f A ≡ (∃tm. ∀ns.
ns ∈ A ⟶
(∃n. f ns = Some n ∧
(∃stp k l. (steps0 (1, ([], <ns::nat list>)) tm stp) = (0, Bk ↑ k, <n::nat> @ Bk ↑ l))) )"
lemma turing_computable_total_on_unfolded_into_TMC_yields_condition:
"turing_computable_total_on f A ≡ (∃tm. ∀ns. ns ∈ A ⟶ (∃n. f ns = Some n ∧ TMC_yields_num_res tm ns n ))"
unfolding TMC_yields_num_res_def
by (simp add: turing_computable_total_on_def)
lemma turing_computable_total_on_UNIV_imp_turing_computable_total:
"turing_computable_total_on f UNIV ⟹ turing_computable_total f"
by (simp add: turing_computable_total_on_unfolded_into_TMC_yields_condition
turing_computable_total_unfolded_into_TMC_yields_condition)
end