Theory Multitape_Time_Convention
theory Multitape_Time_Convention
imports Multitape_Finite_Patch
begin
section ‹Time-bound class predicates and cleanup›
text ‹Shared vocabulary for the linear-speedup consumers. An
∗‹eventual› bound holds for all long enough inputs in the language; a
∗‹convention› bound is the Hopcroft--Ullman
\<^cite>‹‹p.~291› in "Hopcroft1979:introduction"› ‹max(n+1, ...)› form on
the substrate, where the floor is ‹n + 2› (the substrate reads the
left endmarker before the first input symbol).›
definition time_bounded_ev :: "('q, 'a) mttm ⇒ (nat ⇒ nat) ⇒ bool" where
"time_bounded_ev M g ⟷
(∃N. ∀w∈Lang_mttm M. N ≤ length w
⟶ accepts_in_time_mttm M w (g (length w)))"
definition time_bounded_conv :: "('q, 'a) mttm ⇒ (nat ⇒ nat) ⇒ bool" where
"time_bounded_conv M g ⟷
(∀w∈Lang_mttm M.
accepts_in_time_mttm M w (max (length w + 2) (g (length w))))"
text ‹The cleanup corollary: an eventual bound is upgraded to a
convention bound on ∗‹all› inputs, at the cost of the finite-control
overhead ‹c0 = 2 * N + 4›, with language, tape count, and determinism
preserved. Instantiates @{const finite_patch} with the (finite, hence
unconditionally available) table ‹w ∈ Lang_mttm M›.
Hypotheses are the weakest the proof uses --- @{const valid_mttm} and
‹bl_tm M ≠ le_tm M›, matching the @{const finite_patch} contract
lemmas it composes (‹finite_patch_language› / ‹_det› /
‹fp_short_time› / ‹fp_long_time›). In particular it does ∗‹not›
require @{const le_unique} or the state distinctness of
@{const well_formed_mttm}, so it applies to machines (e.g. the
encoding wrap) whose ‹le›-uniqueness is not separately established.›
theorem time_cleanup:
assumes vM: "valid_mttm M" and blle: "bl_tm M ≠ le_tm M"
and ev: "time_bounded_ev M g"
obtains N where
"Lang_mttm (finite_patch M (λw. w ∈ Lang_mttm M) N) = Lang_mttm M"
and "k_tm (finite_patch M (λw. w ∈ Lang_mttm M) N) = k_tm M"
and "det_mttm M ⟶ det_mttm (finite_patch M (λw. w ∈ Lang_mttm M) N)"
and "time_bounded_conv (finite_patch M (λw. w ∈ Lang_mttm M) N)
(λn. g n + (2 * N + 4))"
proof -
from ev obtain N where evN: "∀w∈Lang_mttm M. N ≤ length w
⟶ accepts_in_time_mttm M w (g (length w))"
unfolding time_bounded_ev_def by blast
let ?M' = "finite_patch M (λw. w ∈ Lang_mttm M) N"
have lang: "Lang_mttm ?M' = Lang_mttm M"
proof -
have "Lang_mttm ?M' = {w. set w ⊆ Sigma_tm M
∧ (if length w ≤ N then w ∈ Lang_mttm M else w ∈ Lang_mttm M)}"
by (rule finite_patch_language[OF vM blle])
also have "… = {w. set w ⊆ Sigma_tm M ∧ w ∈ Lang_mttm M}" by simp
also have "… = Lang_mttm M" unfolding Lang_mttm_def by auto
finally show ?thesis .
qed
have kpres: "k_tm ?M' = k_tm M" by (rule finite_patch_k_tm)
have detpres: "det_mttm M ⟶ det_mttm ?M'"
using finite_patch_det[OF vM blle] by blast
have conv: "time_bounded_conv ?M' (λn. g n + (2 * N + 4))"
unfolding time_bounded_conv_def
proof
fix w assume "w ∈ Lang_mttm ?M'"
hence wL: "w ∈ Lang_mttm M" using lang by simp
have wSg: "set w ⊆ Sigma_tm M" using wL unfolding Lang_mttm_def by simp
show "accepts_in_time_mttm ?M' w
(max (length w + 2) ((λn. g n + (2 * N + 4)) (length w)))"
proof (cases "length w ≤ N")
case True
have "accepts_in_time_mttm ?M' w (length w + 2)"
using vM wSg True wL by (rule fp_short_time)
moreover have "length w + 2 ≤ max (length w + 2) (g (length w) + (2 * N + 4))"
by simp
ultimately show ?thesis by (auto elim: accepts_in_time_mttm_mono)
next
case False
hence Nlt: "N < length w" by simp
have "accepts_in_time_mttm M w (g (length w))" using evN wL Nlt by simp
hence "accepts_in_time_mttm ?M' w (g (length w) + (2 * N + 4))"
by (rule fp_long_time[OF vM wSg Nlt])
moreover have "g (length w) + (2 * N + 4)
≤ max (length w + 2) (g (length w) + (2 * N + 4))" by simp
ultimately show ?thesis by (auto elim: accepts_in_time_mttm_mono)
qed
qed
show thesis
proof (rule that[of N])
show "Lang_mttm ?M' = Lang_mttm M" by (rule lang)
show "k_tm ?M' = k_tm M" by (rule kpres)
show "det_mttm M ⟶ det_mttm ?M'" by (rule detpres)
show "time_bounded_conv ?M' (λn. g n + (2 * N + 4))" by (rule conv)
qed
qed
subsection ‹The clean convention form is unattainable in general›
text ‹Why the linear-‹T› speedup theorems are stated with a residual
‹+K› (all inputs) or an explicit threshold (eventual), never as the clean
‹time_bounded_conv M (λn. n + n div q)› on ∗‹all› inputs: that clean form
is not attainable for a machine whose small-input computation exceeds the
convention floor ‹n + 2›. The minimal witness ‹CE› below is a deterministic,
valid machine over the empty input alphabet that accepts the empty input in
exactly ∗‹three› steps (state chain ‹0 → 1 → 2 → 3›, reading and
rewriting the left endmarker in place), one more than the floor
‹length [] + 2 = 2›. So ‹[] ∈ Lang_mttm CE› yet
‹¬ accepts_in_time_mttm CE [] 2›, hence ‹time_bounded_conv CE (λn. n + n div q)›
fails at ‹[]› for every ‹q›. ‹CE› stands in for the encoding wrap, whose
own setup phases (‹W_Init → W_Buf → W_Reset → W_Disp›) likewise exceed the
floor on tiny inputs; closing the small-input band needs the non-effective
finite-exceptions table (an existence-only object; see ‹time_cleanup›),
which is exactly what the clean form would
demand and what the speedup construction does not build.›
definition ce_read :: "nat ⇒ nat" where
"ce_read = (λj. if j = 0 then 1 else 0)"
definition ce_delta ::
"(nat × (nat ⇒ nat) × nat × (nat ⇒ nat) × (nat ⇒ dir)) set" where
"ce_delta = {(0, ce_read, 1, ce_read, λ_. dir.N),
(1, ce_read, 2, ce_read, λ_. dir.N),
(2, ce_read, 3, ce_read, λ_. dir.N)}"
definition CE :: "(nat, nat) mttm" where
"CE = MTTM {0,1,2,3,4} {} {0,1} 0 1 ce_delta 0 3 4 1"
definition ce_tape :: "nat ⇒ nat ⇒ nat" where
"ce_tape = (λi n. if i = 0 ∧ n = 0 then 1 else 0)"
abbreviation ce_cfg :: "nat ⇒ (nat, nat) mt_config" where
"ce_cfg q ≡ Config⇩M q ce_tape (λ_. 0)"
lemma ce_delta_tm: "delta_tm CE = ce_delta" by (simp add: CE_def)
lemma ce_t_tm: "t_tm CE = 3" by (simp add: CE_def)
lemma ce_read_eq: "(λk. ce_tape k ((λ_. 0::nat) k)) = ce_read"
by (simp add: ce_tape_def ce_read_def fun_eq_iff)
lemma ce_valid: "valid_mttm CE"
by (auto simp: CE_def ce_delta_def ce_read_def Pi_iff)
lemma ce_det: "det_mttm CE"
by (auto simp: det_mttm_def ce_delta_tm ce_delta_def)
lemma ce_init: "init_config_mttm CE [] = ce_cfg 0"
by (auto simp: CE_def ce_tape_def fun_eq_iff)
text ‹Forward: each state ‹m ≤ 2› steps deterministically to ‹m + 1›, the
tape and heads unchanged (the endmarker is re-read and re-written in place).›
lemma ce_step_fwd:
assumes "m ≤ 2"
shows "(ce_cfg m, ce_cfg (Suc m)) ∈ mttm_step ce_delta"
proof -
have mem: "(m, ce_read, Suc m, ce_read, λ_. dir.N) ∈ ce_delta"
using assms unfolding ce_delta_def by (cases m; simp; presburger)
have upd: "(λk. (ce_tape k)((λ_. 0::nat) k := ce_read k)) = ce_tape"
by (simp add: ce_tape_def ce_read_def fun_eq_iff)
have mov: "(λk. go_dir ((λ_. dir.N) k) ((λ_. 0::nat) k)) = (λ_. 0)"
by simp
have "(Config⇩M m ce_tape (λ_. 0),
Config⇩M (Suc m) (λk. (ce_tape k)((λ_. 0) k := ce_read k))
(λk. go_dir ((λ_. dir.N) k) ((λ_. 0) k)))
∈ mttm_step ce_delta"
by (rule mttm_step.step) (use mem ce_read_eq in simp)
thus ?thesis by (simp add: upd mov)
qed
text ‹Backward: from state ‹m› the ∗‹only› successor is state ‹m + 1› ---
the single ‹ce_delta› entry with source ‹m›, tape and heads fixed.›
lemma ce_delta_inv:
"(m, ce_read, q', a, dir) ∈ ce_delta ⟹ q' = Suc m ∧ a = ce_read ∧ dir = (λ_. dir.N)"
by (auto simp: ce_delta_def)
lemma ce_step_unique:
"(ce_cfg m, cM) ∈ mttm_step ce_delta ⟹ cM = ce_cfg (Suc m)"
by (auto elim!: mttm_step.cases
simp: ce_delta_def ce_tape_def ce_read_def fun_eq_iff)
text ‹Reachability: in ‹n ≤ 2› steps from the start the machine is in state
‹n ≤ 2 ≠ 3› --- so it cannot have accepted.›
lemma ce_reach:
"(ce_cfg 0, cM) ∈ (mttm_step ce_delta) ^^ n ⟹ n ≤ 2 ⟹ cM = ce_cfg n"
proof (induction n arbitrary: cM)
case 0
then show ?case by simp
next
case (Suc m)
from Suc.prems(1) obtain c where
rm: "(ce_cfg 0, c) ∈ (mttm_step ce_delta) ^^ m" and
st: "(c, cM) ∈ mttm_step ce_delta"
by (auto elim: relpow_Suc_E)
have "m ≤ 2" using Suc.prems(2) by simp
from Suc.IH[OF rm this] have "c = ce_cfg m" .
with st have "(ce_cfg m, cM) ∈ mttm_step ce_delta" by simp
from ce_step_unique[OF this] show ?case .
qed
lemma ce_lang: "[] ∈ Lang_mttm CE"
proof -
have s0: "(ce_cfg 0, ce_cfg (Suc 0)) ∈ mttm_step ce_delta"
by (rule ce_step_fwd) simp
have s1: "(ce_cfg (Suc 0), ce_cfg (Suc (Suc 0))) ∈ mttm_step ce_delta"
by (rule ce_step_fwd) simp
have s2: "(ce_cfg (Suc (Suc 0)), ce_cfg (Suc (Suc (Suc 0)))) ∈ mttm_step ce_delta"
by (rule ce_step_fwd) simp
have "(ce_cfg 0, ce_cfg (Suc (Suc (Suc 0)))) ∈ (mttm_step ce_delta) ^^ (Suc (Suc (Suc 0)))"
by (rule relpow_Suc_I2[OF s0 relpow_Suc_I2[OF s1 relpow_Suc_I2[OF s2 relpow_0_I]]])
hence "(ce_cfg 0, ce_cfg (Suc (Suc (Suc 0)))) ∈ (mttm_step ce_delta)⇧*"
by (rule relpow_imp_rtrancl)
hence "(init_config_mttm CE [], Config⇩M (t_tm CE) ce_tape (λ_. 0))
∈ (mttm_step (delta_tm CE))⇧*"
by (simp add: ce_init ce_delta_tm ce_t_tm numeral_3_eq_3)
thus ?thesis
unfolding Lang_mttm_def by (auto simp: CE_def)
qed
lemma ce_not_accepts: "¬ accepts_in_time_mttm CE [] 2"
proof
assume "accepts_in_time_mttm CE [] 2"
then obtain n cM where nle: "n ≤ 2"
and reach: "(init_config_mttm CE [], cM) ∈ (mttm_step (delta_tm CE)) ^^ n"
and acc: "mt_state cM = t_tm CE"
unfolding accepts_in_time_mttm_def by blast
from reach have "(ce_cfg 0, cM) ∈ (mttm_step ce_delta) ^^ n"
by (simp add: ce_init ce_delta_tm)
from ce_reach[OF this nle] have "mt_state cM = n" by simp
with acc nle show False by (simp add: ce_t_tm)
qed
theorem clean_convention_unattainable:
"¬ time_bounded_conv CE (λn. n + n div q)"
proof
assume "time_bounded_conv CE (λn. n + n div q)"
hence "∀w∈Lang_mttm CE.
accepts_in_time_mttm CE w (max (length w + 2) (length w + length w div q))"
by (simp add: time_bounded_conv_def)
from bspec[OF this ce_lang] have "accepts_in_time_mttm CE [] 2"
by (simp add: numeral_2_eq_2)
with ce_not_accepts show False by simp
qed
end