Theory Turing_Busy_Beaver

theory Turing_Busy_Beaver
  imports
    Busy_Beaver_Base
    "Universal_Turing_Machine.TuringComputable"
begin

section ‹Busy Beaver Upper Bounds for Universal Turing Machines›

text ‹
  This theory connects the abstract Busy Beaver upper-bound principle to the
  Turing machines from AFP's Universal Turing Machine entry \<^cite>‹Xu13›.  We
  use halting with a numeric result, the halting predicate that occurs in AFP's
  formalization of the special halting problems.  The first instantiation is a
  direct Turing-program Busy Beaver function.  Inside AFP's ‹hpk› locale we
  also define code-indexed variants for the one-argument problem ‹K1› and the
  two-argument problem ‹H1›.  Finally, using AFP's Turing-computability
  interface, we make the noncomputability consequence explicit for the
  characteristic functions of the induced ‹H1› decider sets.
›

text ‹
  Three related Busy Beaver notions appear below.  The theory
  ‹Busy_Beaver_Base› supplies the model-parametric function
  ‹BB_time›, whose objects are abstract programs run on input ‹0›.  The
  first concrete interpretation instantiates this as ‹Turing_BB_time› for
  AFP Turing programs, still using a direct program-size measure.  The
  code-indexed interpretations are introduced for the halting problems in the
  Universal Turing Machine entry: the diagonal code-indexed function decides
  ‹K1›, while the pair-indexed function folds a machine code and input into a
  single Busy Beaver object so that upper bounds decide ‹H1›.
›


subsection ‹Exact halting times for numeric results›

definition has_num_result_at :: "tprog0 ⇒ nat list ⇒ nat ⇒ bool" where
  "has_num_result_at tm ns t ⟷
    is_final (steps0 (1, [], <ns>) tm t) ∧
    (∃k n l. steps0 (1, [], <ns>) tm t = (0, Bk ↑ k, <n::nat> @ Bk ↑ l))"

definition tm_num_halts_in :: "tprog0 ⇒ nat ⇒ nat ⇒ bool" where
  "tm_num_halts_in tm input t ⟷
    has_num_result_at tm [input] t ∧ (∀u<t. ¬ has_num_result_at tm [input] u)"

lemma tm_num_halts_in_unique:
  assumes "tm_num_halts_in tm input t"
    and "tm_num_halts_in tm input u"
  shows "t = u"
  by (meson assms nat_neq_iff tm_num_halts_in_def)

lemma TMC_has_num_res_iff_tm_num_halts:
  "TMC_has_num_res tm [input] ⟷ (∃t. tm_num_halts_in tm input t)"
proof
  assume "TMC_has_num_res tm [input]"
  then obtain t k n l where
    final: "is_final (steps0 (1, [], <[input]>) tm t)" and
    result: "steps0 (1, [], <[input]>) tm t = (0, Bk ↑ k, <n::nat> @ Bk ↑ l)"
    unfolding TMC_has_num_res_iff by blast
  have t: "has_num_result_at tm [input] t"
    unfolding has_num_result_at_def using final result by blast
  let ?t = "LEAST u. has_num_result_at tm [input] u"
  have ex: "∃u. has_num_result_at tm [input] u"
    using t by blast
  have least: "has_num_result_at tm [input] ?t"
    using ex by (rule LeastI_ex)
  have none_before: "∀u<?t. ¬ has_num_result_at tm [input] u"
    by (meson not_less_Least)
  have "tm_num_halts_in tm input ?t"
    using least not_less_Least tm_num_halts_in_def by auto
  then show "∃t. tm_num_halts_in tm input t"
    by blast
next
  assume "∃t. tm_num_halts_in tm input t"
  then obtain t where "tm_num_halts_in tm input t"
    by blast
  then have "has_num_result_at tm [input] t"
    unfolding tm_num_halts_in_def by blast
  then show "TMC_has_num_res tm [input]"
    unfolding TMC_has_num_res_iff
    using has_num_result_at_def by auto
qed


subsection ‹A finite size measure for Turing programs›

fun action_rank :: "action ⇒ nat" where
  "action_rank WB = 0"
| "action_rank WO = 1"
| "action_rank L = 2"
| "action_rank R = 3"
| "action_rank Nop = 4"

definition instr_size :: "instr ⇒ nat" where
  "instr_size i = Suc (action_rank (fst i) + snd i)"

definition tm_size :: "tprog0 ⇒ nat" where
  "tm_size tm = length tm + sum_list (map instr_size tm)"

lemma finite_instr_size_le: "finite {i::instr. instr_size i ≤ n}"
proof -
  have subset: "{i::instr. instr_size i ≤ n} ⊆ (UNIV::action set) × {s. s ≤ n}"
    by (auto simp: instr_size_def)
  have "finite (UNIV::action set)"
  proof -
    have eq: "(UNIV::action set) = {WB, WO, L, R, Nop}"
      by (auto intro: action.exhaust)
    have "finite ({WB, WO, L, R, Nop} :: action set)"
      by simp
    then show ?thesis
      using eq by simp
  qed
  have fin: "finite ((UNIV::action set) × {s. s ≤ n})"
    by (simp add: ‹finite (UNIV::action set)›)
  show ?thesis
    by (rule finite_subset[OF subset fin])
qed

lemma length_le_tm_size:
  "length tm ≤ tm_size tm"
  by (simp add: tm_size_def)

lemma instr_size_le_tm_size:
  assumes "i ∈ set tm"
  shows "instr_size i ≤ tm_size tm"
proof -
  have "instr_size i ∈ set (map instr_size tm)"
    using assms by auto
  then have "instr_size i ≤ sum_list (map instr_size tm)"
    by (simp add: member_le_sum_list)
  also have "… ≤ tm_size tm"
    by (simp add: tm_size_def)
  finally show ?thesis .
qed

lemma finite_tm_size_le: "finite {tm::tprog0. tm_size tm ≤ n}"
proof -
  let ?I = "{i::instr. instr_size i ≤ n}"
  have subset: "{tm::tprog0. tm_size tm ≤ n}
      ⊆ {tm. set tm ⊆ ?I ∧ length tm ≤ n}"
  proof
    fix tm :: tprog0
    assume tm: "tm ∈ {tm. tm_size tm ≤ n}"
    then have len: "length tm ≤ n"
      using length_le_tm_size[of tm] by simp
    have "set tm ⊆ ?I"
      using instr_size_le_tm_size mem_Collect_eq order_trans subset_code(1) tm
      by fastforce
    then show "tm ∈ {tm. set tm ⊆ ?I ∧ length tm ≤ n}"
      using len by simp
  qed
  have fin: "finite {tm::tprog0. set tm ⊆ ?I ∧ length tm ≤ n}"
    using finite_instr_size_le by (rule finite_lists_length_le)
  show ?thesis
    by (rule finite_subset[OF subset fin])
qed

interpretation turing_busy_beaver: busy_beaver_base tm_size tm_num_halts_in
proof
  fix n
  show "finite {p. tm_size p ≤ n}"
    by (rule finite_tm_size_le)
next
  fix p x t u
  assume "tm_num_halts_in p x t" and "tm_num_halts_in p x u"
  then show "t = u"
    by (rule tm_num_halts_in_unique)
qed

abbreviation Turing_BB_time :: "nat ⇒ nat" where
  "Turing_BB_time ≡ turing_busy_beaver.BB_time"

theorem Turing_BB_time_ge:
  assumes "tm_size tm ≤ n"
    and "tm_num_halts_in tm 0 t"
  shows "t ≤ Turing_BB_time n"
  using turing_busy_beaver.BB_time_ge_time assms by blast


subsection ‹The code-indexed Busy Beaver function and AFP's special halting problem›

context hpk
begin

text ‹
  The next predicate is deliberately diagonal: the formal locale input is not
  used because the special halting problem ‹K1› asks whether the machine coded
  by ‹c› halts on input ‹c›.
›

definition coded_diagonal_num_halts_in :: "nat ⇒ nat ⇒ nat ⇒ bool" where
  "coded_diagonal_num_halts_in c input t ⟷ tm_num_halts_in (c2t c) c t"

interpretation coded_busy_beaver: busy_beaver_base "λc::nat. c" coded_diagonal_num_halts_in
proof
  fix n
  show "finite {p::nat. p ≤ n}"
    by simp
next
  fix p x t u
  assume "coded_diagonal_num_halts_in p x t" and "coded_diagonal_num_halts_in p x u"
  then show "t = u"
    by (auto simp: coded_diagonal_num_halts_in_def dest: tm_num_halts_in_unique)
qed

abbreviation Coded_BB_time :: "nat ⇒ nat" where
  "Coded_BB_time ≡ coded_busy_beaver.BB_time"

lemma coded_halts_iff_K1:
  "coded_busy_beaver.halts c 0 ⟷ [c] ∈ K1"
proof
  assume "coded_busy_beaver.halts c 0"
  then have "∃t. tm_num_halts_in (c2t c) c t"
    unfolding coded_busy_beaver.halts_def coded_diagonal_num_halts_in_def by blast
  then have "TMC_has_num_res (c2t c) [c]"
    using TMC_has_num_res_iff_tm_num_halts by blast
  then show "[c] ∈ K1"
    unfolding K1_def by blast
next
  assume "[c] ∈ K1"
  then have "TMC_has_num_res (c2t c) [c]"
    unfolding K1_def by auto
  then have "∃t. tm_num_halts_in (c2t c) c t"
    using TMC_has_num_res_iff_tm_num_halts by blast
  then show "coded_busy_beaver.halts c 0"
    unfolding coded_busy_beaver.halts_def coded_diagonal_num_halts_in_def by blast
qed

theorem coded_BB_upper_bound_decides_K1:
  assumes "coded_busy_beaver.upper_bound_for_BB b"
  shows "coded_busy_beaver.halting_decider_from b c 0 ⟷ [c] ∈ K1"
  using coded_busy_beaver.halting_decider_from_correct_0[OF assms, of c]
  by (simp add: coded_halts_iff_K1)

corollary K1_not_turing_decidable_again: "¬ turing_decidable K1"
  by (rule not_Turing_decidable_K1)


subsection ‹A code-indexed Busy Beaver function for the two-argument halting problem›

text ‹
  The previous code-indexed function targets the diagonal/special problem
  ‹K1›.  To cover AFP's two-argument halting problem ‹H1›, we fold the input
  into the Busy Beaver object itself: an object is a pair ‹(c, m)› consisting
  of a machine code and an input.  The size measure ‹c + m› has finite bounded
  classes, and an upper bound for the resulting Busy Beaver function decides
  membership in ‹H1›.
›

definition coded_pair_num_halts_in :: "(nat × nat) ⇒ nat ⇒ nat ⇒ bool" where
  "coded_pair_num_halts_in cm input t ⟷
    tm_num_halts_in (c2t (fst cm)) (snd cm) t"

definition coded_pair_size :: "nat × nat ⇒ nat" where
  "coded_pair_size cm = fst cm + snd cm"

lemma finite_coded_pair_size_le:
  "finite {cm::nat × nat. coded_pair_size cm ≤ n}"
proof -
  have subset:
    "{cm::nat × nat. coded_pair_size cm ≤ n} ⊆ {c. c ≤ n} × {m. m ≤ n}"
    by (auto simp: coded_pair_size_def)
  have fin: "finite ({c. c ≤ n} × {m. m ≤ n})"
    by simp
  show ?thesis
    by (rule finite_subset[OF subset fin])
qed

interpretation pair_busy_beaver: busy_beaver_base coded_pair_size coded_pair_num_halts_in
proof
  fix n
  show "finite {p. coded_pair_size p ≤ n}"
    by (rule finite_coded_pair_size_le)
next
  fix p x t u
  assume "coded_pair_num_halts_in p x t" and "coded_pair_num_halts_in p x u"
  then show "t = u"
    by (auto simp: coded_pair_num_halts_in_def dest: tm_num_halts_in_unique)
qed

abbreviation Pair_BB_time :: "nat ⇒ nat" where
  "Pair_BB_time ≡ pair_busy_beaver.BB_time"

lemma coded_pair_halts_iff_H1:
  "pair_busy_beaver.halts (c, m) 0 ⟷ [c, m] ∈ H1"
proof
  assume "pair_busy_beaver.halts (c, m) 0"
  then have "∃t. tm_num_halts_in (c2t c) m t"
    unfolding pair_busy_beaver.halts_def coded_pair_num_halts_in_def by simp
  then have "TMC_has_num_res (c2t c) [m]"
    using TMC_has_num_res_iff_tm_num_halts by blast
  then show "[c, m] ∈ H1"
    unfolding H1_def by blast
next
  assume "[c, m] ∈ H1"
  then have "TMC_has_num_res (c2t c) [m]"
    unfolding H1_def by auto
  then have "∃t. tm_num_halts_in (c2t c) m t"
    using TMC_has_num_res_iff_tm_num_halts by blast
  then show "pair_busy_beaver.halts (c, m) 0"
    unfolding pair_busy_beaver.halts_def coded_pair_num_halts_in_def by simp
qed

theorem pair_BB_upper_bound_decides_H1_pair:
  assumes "pair_busy_beaver.upper_bound_for_BB b"
  shows "pair_busy_beaver.halting_decider_from b (c, m) 0 ⟷ [c, m] ∈ H1"
  using pair_busy_beaver.halting_decider_from_correct_0[OF assms, of "(c, m)"]
  by (simp add: coded_pair_halts_iff_H1)

definition H1_decider_from :: "(nat ⇒ nat) ⇒ nat list ⇒ bool" where
  "H1_decider_from b nl ⟷
    (case nl of
      [c, m] ⇒ pair_busy_beaver.halting_decider_from b (c, m) 0
    | _ ⇒ False)"

theorem H1_decider_from_correct:
  assumes "pair_busy_beaver.upper_bound_for_BB b"
  shows "H1_decider_from b nl ⟷ nl ∈ H1"
proof (cases nl)
  case Nil
  then show ?thesis
    by (simp add: H1_decider_from_def H1_def)
next
  case (Cons c xs)
  note nl_Cons = Cons
  then show ?thesis
  proof (cases xs)
    case Nil
    then show ?thesis
      using nl_Cons by (simp add: H1_decider_from_def H1_def)
  next
    case (Cons m ys)
    note xs_Cons = Cons
    then show ?thesis
    proof (cases ys)
      case Nil
      have nl_eq: "nl = [c, m]"
        using nl_Cons xs_Cons Nil by simp
      then show ?thesis
        using pair_BB_upper_bound_decides_H1_pair[OF assms, of c m] nl_eq
        by (simp add: H1_decider_from_def)
    next
      case (Cons k zs)
      then show ?thesis
        using nl_Cons xs_Cons by (auto simp: H1_decider_from_def H1_def)
    qed
  qed
qed

corollary H1_not_turing_decidable_again: "¬ turing_decidable H1"
  by (rule not_Turing_decidable_H1)

text ‹
  For every upper bound, the Boolean decider above defines the same set as
  ‹H1›.  Hence AFP's existing undecidability theorem for ‹H1› immediately
  yields a concrete noncomputability consequence: the characteristic function of
  any such upper-bound-induced decider set is not Turing-computable, even in the
  total sense.  In particular, this applies to the decider induced by
  ‹Pair_BB_time› itself.
›

definition H1_decider_set_from :: "(nat ⇒ nat) ⇒ nat list set" where
  "H1_decider_set_from b = {nl. H1_decider_from b nl}"

lemma H1_decider_set_from_eq_H1:
  assumes "pair_busy_beaver.upper_bound_for_BB b"
  shows "H1_decider_set_from b = H1"
  using H1_decider_from_correct[OF assms]
  by (auto simp: H1_decider_set_from_def)

theorem no_turing_decidable_H1_decider_set_from:
  assumes "pair_busy_beaver.upper_bound_for_BB b"
  shows "¬ turing_decidable (H1_decider_set_from b)"
  using H1_decider_set_from_eq_H1[OF assms] not_Turing_decidable_H1
  by simp

theorem no_turing_computable_partial_H1_decider_from:
  assumes "pair_busy_beaver.upper_bound_for_BB b"
  shows "¬ turing_computable_partial (chi_fun (H1_decider_set_from b))"
  using no_turing_decidable_H1_decider_set_from[OF assms]
    turing_computable_partial_imp_turing_decidable
  by blast

theorem no_turing_computable_total_H1_decider_from:
  assumes "pair_busy_beaver.upper_bound_for_BB b"
  shows "¬ turing_computable_total (chi_fun (H1_decider_set_from b))"
  using no_turing_computable_partial_H1_decider_from[OF assms]
    turing_computable_total_imp_turing_computable_partial
  by blast

theorem no_turing_computable_total_H1_deciding_upper_bound:
  "¬ (∃b. pair_busy_beaver.upper_bound_for_BB b ∧
      turing_computable_total (chi_fun (H1_decider_set_from b)))"
  using no_turing_computable_total_H1_decider_from by blast

corollary no_turing_computable_total_Pair_BB_time_decider:
  "¬ turing_computable_total (chi_fun (H1_decider_set_from Pair_BB_time))"
  using no_turing_computable_total_H1_decider_from
    pair_busy_beaver.BB_time_is_upper_bound
  by blast

end

end