Theory Wrap_Convention
theory Wrap_Convention
imports Wrap_Speedup "Multitape_TM_Substrate.Multitape_Time_Convention"
begin
section ‹The linear-speedup headlines in Hopcroft--Ullman's
time-complexity convention›
text ‹The @{theory Multitape_Alphabet_Enlargement.Wrap_Speedup} headlines
‹linear_speedup_HU_12_3› / ‹linear_speedup_HU_12_4› prove a ∗‹raw›
bound: a per-run additive constant ‹K› (and for 12.3 a bare length
threshold ‹N0›), gated on the input run itself completing within
‹T›. Hopcroft and Ullman state 12.3 / 12.4 in a ∗‹time-complexity
convention› \<^cite>‹‹p.~291› in "Hopcroft1979:introduction"›: a machine
``runs in time ‹cT(n)›'' means it accepts every
word of its language within @{text ‹max(n + 1, ceil(cT(n)))›} steps, the
@{text ‹n + 1›} floor being the cost of reading the input. On our
substrate the floor is @{text ‹n + 2›} (the left endmarker is read
before the first input symbol); this is exactly the
@{const time_bounded_conv} predicate of
@{theory Multitape_TM_Substrate.Multitape_Time_Convention}.
This theory restates the two headlines in that convention. The
wrapped machine is a genuine @{type mttm}, and its user-facing
language / timing (@{const Lang_user_wrap} / @{const
accepts_in_time_user_wrap}) are the @{const Lang_mttm} / @{const
accepts_in_time_mttm} of the wrap read through @{const Raw}, so
@{const time_bounded_conv} applied to the wrap ∗‹is› the user-level
convention statement (‹Lang_mttm_encoding_wrap_ex_Raw› below is the
bridge). The two cases diverge:
▪ ❙‹12.4 (linear ‹T›).› The raw bound @{text ‹|w| + |w| div q + K›}
already holds for ∗‹all› lengths, so the convention statement is the
max-floored restatement, provided ‹M› runs in time ‹T› on its
language. The additive ‹K› cannot be folded into a smaller
@{text ‹eps = 1 / q›} on all inputs: the clean form
@{term ‹time_bounded_conv M (λn. n + n div q)›} is provably
∗‹unattainable› in general (the counterexample
‹clean_convention_unattainable› in
@{theory Multitape_TM_Substrate.Multitape_Time_Convention} --- a valid machine can
accept its language yet exceed the floor ‹n + 2› on its shortest input,
as the wrap's own setup phases do at ‹n = 0›). The obstruction is the
finite-prefix ∗‹band›: an outer @{const finite_patch} cleanup scans
proportionally to its cutoff, so its overhead never drops below
‹eps›, and shaving the rewind only narrows the band. It is
∗‹not› the origin rewind of
the faithful ‹k›-tape construction (a distinct obstruction). So
‹K› is kept explicit.
▪ ❙‹12.3 (superlinear ‹T›).› Here superlinear growth dominates any
linear-in-cutoff cost, so the @{const finite_patch} small-input
cleanup (‹time_cleanup› on the table @{term ‹λw. w ∈ Lang_mttm M›})
and the additive constant both wash out into a slightly larger
multiplicative constant --- a clean @{text ‹ceil(c T(n))›} convention
bound with no residual constant.
The raw @{text ‹+ K›} theorems remain the explicit-constant corollaries
(nothing is lost).›
subsection ‹Bridge: an accepted word of the wrap is @{const Raw}-encoded›
text ‹Every word of @{const Lang_mttm} of an @{const encoding_wrap} is
@{term ‹map Raw w›} for a user word ‹w›, because the wrap's input
alphabet is @{term ‹Raw ` Σu›}. This lets a @{const time_bounded_conv}
goal over the wrap's @{const Lang_mttm} be discharged through the
user-level @{const accepts_in_time_user_wrap} bound the raw headlines
supply, and conversely.›
lemma Lang_mttm_encoding_wrap_ex_Raw:
assumes "v ∈ Lang_mttm (encoding_wrap M pack c Σu)"
shows "∃w. v = map Raw w ∧ w ∈ Lang_user_wrap (encoding_wrap M pack c Σu)"
proof -
let ?W = "encoding_wrap M pack c Σu"
have sv: "set v ⊆ Raw ` Σu"
using assms unfolding Lang_mttm_def by simp
have "∀x∈set v. ∃y. x = Raw y" using sv by auto
then obtain w where vw: "v = map Raw w" by (metis ex_map_conv)
have "map Raw w ∈ Lang_mttm ?W" using assms vw by simp
hence "w ∈ Lang_user_wrap ?W" unfolding Lang_user_wrap_def by simp
thus ?thesis using vw by blast
qed
subsection ‹Arithmetic core of the superlinear absorption›
text ‹The one inequality that makes 12.3 clean where 12.4 is not: a
constant ‹C› is absorbed by dropping the speedup denominator from
‹q + 1› to ‹q›, provided the numerator ‹a› is at least
‹q (q + 1) C›. In use ‹a = T n›, and the superlinear growth of ‹T›
makes the premise hold for all large ‹n› --- including ‹C = K + 2 N1
+ 4› where ‹N1› is the finite-control cutoff, because the numerator
grows superlinearly in ‹n› while ‹C› grows only linearly in ‹N1›.›
lemma div_absorb_step:
fixes a q C :: nat
assumes q_pos: "0 < q" and big: "q * (q + 1) * C ≤ a"
shows "a div (q + 1) + C ≤ a div q"
proof -
have qne: "q ≠ 0" using q_pos by simp
have q1ne: "q + 1 ≠ 0" by simp
have qC: "q * C ≤ a div (q + 1)"
proof -
have "(q + 1) * (q * C) ≤ a" using big by (simp add: algebra_simps)
hence "((q + 1) * (q * C)) div (q + 1) ≤ a div (q + 1)" by (rule div_le_mono)
moreover have "((q + 1) * (q * C)) div (q + 1) = q * C"
by (metis nonzero_mult_div_cancel_left q1ne)
ultimately show ?thesis by simp
qed
have "q * (a div (q + 1) + C) = q * (a div (q + 1)) + q * C"
by (simp add: algebra_simps)
also have "… ≤ q * (a div (q + 1)) + a div (q + 1)" using qC by simp
also have "… = (q + 1) * (a div (q + 1))" by (simp add: algebra_simps)
also have "… ≤ a" by (metis mult.commute div_times_less_eq_dividend)
finally have le_a: "q * (a div (q + 1) + C) ≤ a" .
hence "(q * (a div (q + 1) + C)) div q ≤ a div q" by (rule div_le_mono)
moreover have "(q * (a div (q + 1) + C)) div q = a div (q + 1) + C"
by (metis nonzero_mult_div_cancel_left qne)
ultimately show ?thesis by simp
qed
subsection ‹HU 12.4 in the convention (linear ‹T›)›
text ‹The nondeterministic linear-‹T› headline, restated as a
@{const time_bounded_conv} bound. The extra hypothesis over the raw
@{thm[source] linear_speedup_HU_12_4_nae} is ‹Mtime›: ‹M› accepts every
word of its language within ‹T› --- i.e. ‹L(M)› ∗‹is› a ‹T›-time
language, the textbook premise. The bound @{term ‹λn. n + n div q + K›}
is the raw @{text ‹+ K›} constant read in the @{text ‹max(n + 2, ...)›}
convention.›
theorem linear_speedup_HU_12_4_nae_conv:
fixes M :: "('q, 'a) mttm"
and T :: "nat ⇒ nat"
and d_0 b q :: nat
assumes wf: "well_formed_mttm M"
and Mtime: "⋀w. w ∈ Lang_mttm M ⟹ accepts_in_time_mttm M w (T (length w))"
and T_linear: "∀n. T n ≤ d_0 * n + b"
and q_pos: "0 < q"
and c_pos: "0 < (card (UNIV :: ('c :: enum) set))"
and k2: "2 ≤ k_tm M"
shows "valid_mttm
(encoding_wrap
(alphabet_enlarge M
:: ('q × ('a, 'c) ae_stage, 'c ⇒ 'a) mttm)
(ae_pack (bl_tm M) :: 'a list ⇒ ('c ⇒ 'a))
(card (UNIV :: 'c set))
(Sigma_tm M))"
and "Lang_user_wrap
(encoding_wrap
(alphabet_enlarge M
:: ('q × ('a, 'c) ae_stage, 'c ⇒ 'a) mttm)
(ae_pack (bl_tm M) :: 'a list ⇒ ('c ⇒ 'a))
(card (UNIV :: 'c set))
(Sigma_tm M))
= Lang_mttm M"
and "q * (3 + 8 * d_0) ≤ card (UNIV :: 'c set)
⟶ time_bounded_conv
(encoding_wrap
(alphabet_enlarge M
:: ('q × ('a, 'c) ae_stage, 'c ⇒ 'a) mttm)
(ae_pack (bl_tm M) :: 'a list ⇒ ('c ⇒ 'a))
(card (UNIV :: 'c set))
(Sigma_tm M))
(λn. n + n div q + (28 + 8 * d_0 + 8 * b))"
proof -
let ?W = "encoding_wrap
(alphabet_enlarge M
:: ('q × ('a, 'c) ae_stage, 'c ⇒ 'a) mttm)
(ae_pack (bl_tm M) :: 'a list ⇒ ('c ⇒ 'a))
(card (UNIV :: 'c set))
(Sigma_tm M)"
obtain α K :: nat where alpha2: "α = (2::nat)"
and Kdef: "K = 28 + 8 * d_0 + 8 * b" by blast
have V: "valid_mttm ?W"
and L: "Lang_user_wrap ?W = Lang_mttm M"
and Tb': "q * (3 + 8 * d_0) ≤ card (UNIV :: 'c set)
⟶ (∀w. set w ⊆ Sigma_tm M
⟶ accepts_in_time_mttm M w (T (length w))
⟶ accepts_in_time_user_wrap ?W w
(length w + length w div q + (28 + 8 * d_0 + 8 * b)))"
by (rule linear_speedup_HU_12_4_nae[OF wf T_linear q_pos c_pos k2])+
have e: "(1::nat) + α + 8 * d_0 = 3 + 8 * d_0" using alpha2 by simp
have Tb: "q * (1 + α + 8 * d_0) ≤ card (UNIV :: 'c set)
⟶ (∀w. set w ⊆ Sigma_tm M
⟶ accepts_in_time_mttm M w (T (length w))
⟶ accepts_in_time_user_wrap ?W w
(length w + length w div q + K))"
unfolding e Kdef by (rule Tb')
have conv: "q * (1 + α + 8 * d_0) ≤ card (UNIV :: 'c set)
⟶ time_bounded_conv ?W (λn. n + n div q + K)"
proof
assume cL: "q * (1 + α + 8 * d_0) ≤ card (UNIV :: 'c set)"
show "time_bounded_conv ?W (λn. n + n div q + K)"
unfolding time_bounded_conv_def
proof
fix v assume vW: "v ∈ Lang_mttm ?W"
then obtain w where vmap: "v = map Raw w" and wU: "w ∈ Lang_user_wrap ?W"
using Lang_mttm_encoding_wrap_ex_Raw by blast
from wU L have wM: "w ∈ Lang_mttm M" by simp
hence wSg: "set w ⊆ Sigma_tm M" unfolding Lang_mttm_def by simp
from wM have accM: "accepts_in_time_mttm M w (T (length w))" by (rule Mtime)
have "accepts_in_time_user_wrap ?W w (length w + length w div q + K)"
using Tb cL wSg accM by blast
hence "accepts_in_time_mttm ?W v (length w + length w div q + K)"
using vmap unfolding accepts_in_time_user_wrap_def by simp
hence "accepts_in_time_mttm ?W v (length v + length v div q + K)"
using vmap by simp
thus "accepts_in_time_mttm ?W v
(max (length v + 2) ((λn. n + n div q + K) (length v)))"
by (auto elim: accepts_in_time_mttm_mono)
qed
qed
show "valid_mttm ?W" by (rule V)
show "Lang_user_wrap ?W = Lang_mttm M" by (rule L)
show "q * (3 + 8 * d_0) ≤ card (UNIV :: 'c set)
⟶ time_bounded_conv ?W (λn. n + n div q + (28 + 8 * d_0 + 8 * b))"
proof -
have s0: "(3::nat) + 8 * d_0 = 1 + α + 8 * d_0" using alpha2 by simp
show ?thesis unfolding s0 Kdef[symmetric] by (rule conv)
qed
qed
text ‹The nondeterministic linear-‹T› headline in the ∗‹eventual›,
constant-free form: past an explicit input-length threshold the wrap runs
in ‹n + n div q› exactly --- the additive ‹K› of
@{thm[source] linear_speedup_HU_12_4_nae_conv} is gone, at the cost of a
hypothesis ‹q⋅(q+1)⋅K ≤ length v› instead of the convention
floor. This is the honest ‹(1+ε)⋅n› shape (with
‹ε = 1/q›): clean coefficient, no residual constant, but only
for long enough inputs --- the small-input band is not covered (it cannot
be, without the non-effective finite-exceptions table; see the counterexample
‹clean_convention_unattainable›).
Proof: run @{thm[source] linear_speedup_HU_12_4_nae} one denominator tighter
(at ‹q+1›), then absorb ‹K› into the extra ‹div›-slack via
@{thm[source] div_absorb_step} once ‹q⋅(q+1)⋅K ≤ length v› ---
the same inequality that makes the superlinear 12.3 constant-free, here read
in the linear regime as an explicit threshold rather than an absorbed
constant. With ‹K› now the literal ‹28 + 8 d_0 + 8 b›, the crossover
threshold is the closed formula ‹q⋅(q+1)⋅(28 + 8 d_0 + 8 b)› ---
quadratic in ‹q› (i.e. ‹O(1/ε⇧2)›), and linear in the input
machine's time-bound constants ‹d_0, b›.›
theorem linear_speedup_HU_12_4_nae_eventual:
fixes M :: "('q, 'a) mttm"
and T :: "nat ⇒ nat"
and d_0 b q :: nat
assumes wf: "well_formed_mttm M"
and Mtime: "⋀w. w ∈ Lang_mttm M ⟹ accepts_in_time_mttm M w (T (length w))"
and T_linear: "∀n. T n ≤ d_0 * n + b"
and q_pos: "0 < q"
and c_pos: "0 < (card (UNIV :: ('c :: enum) set))"
and k2: "2 ≤ k_tm M"
shows "valid_mttm
(encoding_wrap
(alphabet_enlarge M
:: ('q × ('a, 'c) ae_stage, 'c ⇒ 'a) mttm)
(ae_pack (bl_tm M) :: 'a list ⇒ ('c ⇒ 'a))
(card (UNIV :: 'c set))
(Sigma_tm M))"
and "Lang_user_wrap
(encoding_wrap
(alphabet_enlarge M
:: ('q × ('a, 'c) ae_stage, 'c ⇒ 'a) mttm)
(ae_pack (bl_tm M) :: 'a list ⇒ ('c ⇒ 'a))
(card (UNIV :: 'c set))
(Sigma_tm M))
= Lang_mttm M"
and "(q + 1) * (3 + 8 * d_0) ≤ card (UNIV :: 'c set)
⟶ (∀v ∈ Lang_mttm
(encoding_wrap
(alphabet_enlarge M
:: ('q × ('a, 'c) ae_stage, 'c ⇒ 'a) mttm)
(ae_pack (bl_tm M) :: 'a list ⇒ ('c ⇒ 'a))
(card (UNIV :: 'c set))
(Sigma_tm M)).
q * (q + 1) * (28 + 8 * d_0 + 8 * b) ≤ length v
⟶ accepts_in_time_mttm
(encoding_wrap
(alphabet_enlarge M
:: ('q × ('a, 'c) ae_stage, 'c ⇒ 'a) mttm)
(ae_pack (bl_tm M) :: 'a list ⇒ ('c ⇒ 'a))
(card (UNIV :: 'c set))
(Sigma_tm M))
v
(length v + length v div q))"
proof -
let ?W = "encoding_wrap
(alphabet_enlarge M
:: ('q × ('a, 'c) ae_stage, 'c ⇒ 'a) mttm)
(ae_pack (bl_tm M) :: 'a list ⇒ ('c ⇒ 'a))
(card (UNIV :: 'c set))
(Sigma_tm M)"
have q1_pos: "0 < q + 1" by simp
obtain α K :: nat where alpha2: "α = (2::nat)"
and Kdef: "K = 28 + 8 * d_0 + 8 * b" by blast
have V: "valid_mttm ?W"
and L: "Lang_user_wrap ?W = Lang_mttm M"
and Tb': "(q + 1) * (3 + 8 * d_0) ≤ card (UNIV :: 'c set)
⟶ (∀w. set w ⊆ Sigma_tm M
⟶ accepts_in_time_mttm M w (T (length w))
⟶ accepts_in_time_user_wrap ?W w
(length w + length w div (q + 1) + (28 + 8 * d_0 + 8 * b)))"
by (rule linear_speedup_HU_12_4_nae[where q = "q + 1", OF wf T_linear q1_pos c_pos k2])+
have e: "(1::nat) + α + 8 * d_0 = 3 + 8 * d_0" using alpha2 by simp
have Tb: "(q + 1) * (1 + α + 8 * d_0) ≤ card (UNIV :: 'c set)
⟶ (∀w. set w ⊆ Sigma_tm M
⟶ accepts_in_time_mttm M w (T (length w))
⟶ accepts_in_time_user_wrap ?W w
(length w + length w div (q + 1) + K))"
unfolding e Kdef by (rule Tb')
have ev: "(q + 1) * (1 + α + 8 * d_0) ≤ card (UNIV :: 'c set)
⟶ (∀v ∈ Lang_mttm ?W. q * (q + 1) * K ≤ length v
⟶ accepts_in_time_mttm ?W v (length v + length v div q))"
proof
assume cL: "(q + 1) * (1 + α + 8 * d_0) ≤ card (UNIV :: 'c set)"
show "∀v ∈ Lang_mttm ?W. q * (q + 1) * K ≤ length v
⟶ accepts_in_time_mttm ?W v (length v + length v div q)"
proof
fix v assume vW: "v ∈ Lang_mttm ?W"
show "q * (q + 1) * K ≤ length v
⟶ accepts_in_time_mttm ?W v (length v + length v div q)"
proof
assume lv: "q * (q + 1) * K ≤ length v"
from vW obtain w where vmap: "v = map Raw w"
and wU: "w ∈ Lang_user_wrap ?W"
using Lang_mttm_encoding_wrap_ex_Raw by blast
from wU L have wM: "w ∈ Lang_mttm M" by simp
hence wSg: "set w ⊆ Sigma_tm M" unfolding Lang_mttm_def by simp
from wM have accM: "accepts_in_time_mttm M w (T (length w))" by (rule Mtime)
have lenwv: "length w = length v" using vmap by simp
have raw: "accepts_in_time_user_wrap ?W w
(length w + length w div (q + 1) + K)"
using Tb cL wSg accM by blast
have absorb: "length w div (q + 1) + K ≤ length w div q"
by (rule div_absorb_step[OF q_pos]) (use lv lenwv in simp)
hence le: "length w + length w div (q + 1) + K
≤ length w + length w div q" by simp
have "accepts_in_time_mttm ?W (map Raw w)
(length w + length w div (q + 1) + K)"
using raw unfolding accepts_in_time_user_wrap_def by simp
hence "accepts_in_time_mttm ?W (map Raw w) (length w + length w div q)"
using le by (auto elim: accepts_in_time_mttm_mono)
thus "accepts_in_time_mttm ?W v (length v + length v div q)"
by (simp only: vmap length_map)
qed
qed
qed
show "valid_mttm ?W" by (rule V)
show "Lang_user_wrap ?W = Lang_mttm M" by (rule L)
show "(q + 1) * (3 + 8 * d_0) ≤ card (UNIV :: 'c set)
⟶ (∀v ∈ Lang_mttm ?W. q * (q + 1) * (28 + 8 * d_0 + 8 * b) ≤ length v
⟶ accepts_in_time_mttm ?W v (length v + length v div q))"
proof -
have s0: "(3::nat) + 8 * d_0 = 1 + α + 8 * d_0" using alpha2 by simp
show ?thesis unfolding s0 Kdef[symmetric] by (rule ev)
qed
qed
text ‹The deterministic specialisation: adds the ‹det› hypothesis on
‹M› and the determinism-preservation conjunct on the wrap, on top of
@{thm[source] linear_speedup_HU_12_4_nae_conv}.›
theorem linear_speedup_HU_12_4_dae_conv:
fixes M :: "('q, 'a) mttm"
and T :: "nat ⇒ nat"
and d_0 b q :: nat
assumes wf: "well_formed_mttm M"
and det: "det_mttm M"
and Mtime: "⋀w. w ∈ Lang_mttm M ⟹ accepts_in_time_mttm M w (T (length w))"
and T_linear: "∀n. T n ≤ d_0 * n + b"
and q_pos: "0 < q"
and c_pos: "0 < (card (UNIV :: ('c :: enum) set))"
and k2: "2 ≤ k_tm M"
shows "valid_mttm
(encoding_wrap
(alphabet_enlarge M
:: ('q × ('a, 'c) ae_stage, 'c ⇒ 'a) mttm)
(ae_pack (bl_tm M) :: 'a list ⇒ ('c ⇒ 'a))
(card (UNIV :: 'c set))
(Sigma_tm M))"
and "det_mttm
(encoding_wrap
(alphabet_enlarge M
:: ('q × ('a, 'c) ae_stage, 'c ⇒ 'a) mttm)
(ae_pack (bl_tm M) :: 'a list ⇒ ('c ⇒ 'a))
(card (UNIV :: 'c set))
(Sigma_tm M))"
and "Lang_user_wrap
(encoding_wrap
(alphabet_enlarge M
:: ('q × ('a, 'c) ae_stage, 'c ⇒ 'a) mttm)
(ae_pack (bl_tm M) :: 'a list ⇒ ('c ⇒ 'a))
(card (UNIV :: 'c set))
(Sigma_tm M))
= Lang_mttm M"
and "q * (3 + 8 * d_0) ≤ card (UNIV :: 'c set)
⟶ time_bounded_conv
(encoding_wrap
(alphabet_enlarge M
:: ('q × ('a, 'c) ae_stage, 'c ⇒ 'a) mttm)
(ae_pack (bl_tm M) :: 'a list ⇒ ('c ⇒ 'a))
(card (UNIV :: 'c set))
(Sigma_tm M))
(λn. n + n div q + (28 + 8 * d_0 + 8 * b))"
proof -
let ?W = "encoding_wrap
(alphabet_enlarge M
:: ('q × ('a, 'c) ae_stage, 'c ⇒ 'a) mttm)
(ae_pack (bl_tm M) :: 'a list ⇒ ('c ⇒ 'a))
(card (UNIV :: 'c set))
(Sigma_tm M)"
obtain α K :: nat where alpha2: "α = (2::nat)"
and Kdef: "K = 28 + 8 * d_0 + 8 * b" by blast
have V: "valid_mttm ?W"
and D: "det_mttm ?W"
and L: "Lang_user_wrap ?W = Lang_mttm M"
and Tb': "q * (3 + 8 * d_0) ≤ card (UNIV :: 'c set)
⟶ (∀w. set w ⊆ Sigma_tm M
⟶ accepts_in_time_mttm M w (T (length w))
⟶ accepts_in_time_user_wrap ?W w
(length w + length w div q + (28 + 8 * d_0 + 8 * b)))"
by (rule linear_speedup_HU_12_4_dae[OF wf det T_linear q_pos c_pos k2])+
have e: "(1::nat) + α + 8 * d_0 = 3 + 8 * d_0" using alpha2 by simp
have Tb: "q * (1 + α + 8 * d_0) ≤ card (UNIV :: 'c set)
⟶ (∀w. set w ⊆ Sigma_tm M
⟶ accepts_in_time_mttm M w (T (length w))
⟶ accepts_in_time_user_wrap ?W w
(length w + length w div q + K))"
unfolding e Kdef by (rule Tb')
have conv: "q * (1 + α + 8 * d_0) ≤ card (UNIV :: 'c set)
⟶ time_bounded_conv ?W (λn. n + n div q + K)"
proof
assume cL: "q * (1 + α + 8 * d_0) ≤ card (UNIV :: 'c set)"
show "time_bounded_conv ?W (λn. n + n div q + K)"
unfolding time_bounded_conv_def
proof
fix v assume vW: "v ∈ Lang_mttm ?W"
then obtain w where vmap: "v = map Raw w" and wU: "w ∈ Lang_user_wrap ?W"
using Lang_mttm_encoding_wrap_ex_Raw by blast
from wU L have wM: "w ∈ Lang_mttm M" by simp
hence wSg: "set w ⊆ Sigma_tm M" unfolding Lang_mttm_def by simp
from wM have accM: "accepts_in_time_mttm M w (T (length w))" by (rule Mtime)
have "accepts_in_time_user_wrap ?W w (length w + length w div q + K)"
using Tb cL wSg accM by blast
hence "accepts_in_time_mttm ?W v (length w + length w div q + K)"
using vmap unfolding accepts_in_time_user_wrap_def by simp
hence "accepts_in_time_mttm ?W v (length v + length v div q + K)"
using vmap by simp
thus "accepts_in_time_mttm ?W v
(max (length v + 2) ((λn. n + n div q + K) (length v)))"
by (auto elim: accepts_in_time_mttm_mono)
qed
qed
show "valid_mttm ?W" by (rule V)
show "det_mttm ?W" by (rule D)
show "Lang_user_wrap ?W = Lang_mttm M" by (rule L)
show "q * (3 + 8 * d_0) ≤ card (UNIV :: 'c set)
⟶ time_bounded_conv ?W (λn. n + n div q + (28 + 8 * d_0 + 8 * b))"
proof -
have s0: "(3::nat) + 8 * d_0 = 1 + α + 8 * d_0" using alpha2 by simp
show ?thesis unfolding s0 Kdef[symmetric] by (rule conv)
qed
qed
text ‹The determinism-preserving eventual form: @{thm[source]
linear_speedup_HU_12_4_nae_eventual} with the ‹det› hypothesis and the
determinism-preservation conjunct, over @{thm[source]
linear_speedup_HU_12_4_dae}.›
theorem linear_speedup_HU_12_4_dae_eventual:
fixes M :: "('q, 'a) mttm"
and T :: "nat ⇒ nat"
and d_0 b q :: nat
assumes wf: "well_formed_mttm M"
and det: "det_mttm M"
and Mtime: "⋀w. w ∈ Lang_mttm M ⟹ accepts_in_time_mttm M w (T (length w))"
and T_linear: "∀n. T n ≤ d_0 * n + b"
and q_pos: "0 < q"
and c_pos: "0 < (card (UNIV :: ('c :: enum) set))"
and k2: "2 ≤ k_tm M"
shows "valid_mttm
(encoding_wrap
(alphabet_enlarge M
:: ('q × ('a, 'c) ae_stage, 'c ⇒ 'a) mttm)
(ae_pack (bl_tm M) :: 'a list ⇒ ('c ⇒ 'a))
(card (UNIV :: 'c set))
(Sigma_tm M))"
and "det_mttm
(encoding_wrap
(alphabet_enlarge M
:: ('q × ('a, 'c) ae_stage, 'c ⇒ 'a) mttm)
(ae_pack (bl_tm M) :: 'a list ⇒ ('c ⇒ 'a))
(card (UNIV :: 'c set))
(Sigma_tm M))"
and "Lang_user_wrap
(encoding_wrap
(alphabet_enlarge M
:: ('q × ('a, 'c) ae_stage, 'c ⇒ 'a) mttm)
(ae_pack (bl_tm M) :: 'a list ⇒ ('c ⇒ 'a))
(card (UNIV :: 'c set))
(Sigma_tm M))
= Lang_mttm M"
and "(q + 1) * (3 + 8 * d_0) ≤ card (UNIV :: 'c set)
⟶ (∀v ∈ Lang_mttm
(encoding_wrap
(alphabet_enlarge M
:: ('q × ('a, 'c) ae_stage, 'c ⇒ 'a) mttm)
(ae_pack (bl_tm M) :: 'a list ⇒ ('c ⇒ 'a))
(card (UNIV :: 'c set))
(Sigma_tm M)).
q * (q + 1) * (28 + 8 * d_0 + 8 * b) ≤ length v
⟶ accepts_in_time_mttm
(encoding_wrap
(alphabet_enlarge M
:: ('q × ('a, 'c) ae_stage, 'c ⇒ 'a) mttm)
(ae_pack (bl_tm M) :: 'a list ⇒ ('c ⇒ 'a))
(card (UNIV :: 'c set))
(Sigma_tm M))
v
(length v + length v div q))"
proof -
let ?W = "encoding_wrap
(alphabet_enlarge M
:: ('q × ('a, 'c) ae_stage, 'c ⇒ 'a) mttm)
(ae_pack (bl_tm M) :: 'a list ⇒ ('c ⇒ 'a))
(card (UNIV :: 'c set))
(Sigma_tm M)"
have q1_pos: "0 < q + 1" by simp
obtain α K :: nat where alpha2: "α = (2::nat)"
and Kdef: "K = 28 + 8 * d_0 + 8 * b" by blast
have V: "valid_mttm ?W"
and D: "det_mttm ?W"
and L: "Lang_user_wrap ?W = Lang_mttm M"
and Tb': "(q + 1) * (3 + 8 * d_0) ≤ card (UNIV :: 'c set)
⟶ (∀w. set w ⊆ Sigma_tm M
⟶ accepts_in_time_mttm M w (T (length w))
⟶ accepts_in_time_user_wrap ?W w
(length w + length w div (q + 1) + (28 + 8 * d_0 + 8 * b)))"
by (rule linear_speedup_HU_12_4_dae[where q = "q + 1", OF wf det T_linear q1_pos c_pos k2])+
have e: "(1::nat) + α + 8 * d_0 = 3 + 8 * d_0" using alpha2 by simp
have Tb: "(q + 1) * (1 + α + 8 * d_0) ≤ card (UNIV :: 'c set)
⟶ (∀w. set w ⊆ Sigma_tm M
⟶ accepts_in_time_mttm M w (T (length w))
⟶ accepts_in_time_user_wrap ?W w
(length w + length w div (q + 1) + K))"
unfolding e Kdef by (rule Tb')
have ev: "(q + 1) * (1 + α + 8 * d_0) ≤ card (UNIV :: 'c set)
⟶ (∀v ∈ Lang_mttm ?W. q * (q + 1) * K ≤ length v
⟶ accepts_in_time_mttm ?W v (length v + length v div q))"
proof
assume cL: "(q + 1) * (1 + α + 8 * d_0) ≤ card (UNIV :: 'c set)"
show "∀v ∈ Lang_mttm ?W. q * (q + 1) * K ≤ length v
⟶ accepts_in_time_mttm ?W v (length v + length v div q)"
proof
fix v assume vW: "v ∈ Lang_mttm ?W"
show "q * (q + 1) * K ≤ length v
⟶ accepts_in_time_mttm ?W v (length v + length v div q)"
proof
assume lv: "q * (q + 1) * K ≤ length v"
from vW obtain w where vmap: "v = map Raw w"
and wU: "w ∈ Lang_user_wrap ?W"
using Lang_mttm_encoding_wrap_ex_Raw by blast
from wU L have wM: "w ∈ Lang_mttm M" by simp
hence wSg: "set w ⊆ Sigma_tm M" unfolding Lang_mttm_def by simp
from wM have accM: "accepts_in_time_mttm M w (T (length w))" by (rule Mtime)
have lenwv: "length w = length v" using vmap by simp
have raw: "accepts_in_time_user_wrap ?W w
(length w + length w div (q + 1) + K)"
using Tb cL wSg accM by blast
have absorb: "length w div (q + 1) + K ≤ length w div q"
by (rule div_absorb_step[OF q_pos]) (use lv lenwv in simp)
hence le: "length w + length w div (q + 1) + K
≤ length w + length w div q" by simp
have "accepts_in_time_mttm ?W (map Raw w)
(length w + length w div (q + 1) + K)"
using raw unfolding accepts_in_time_user_wrap_def by simp
hence "accepts_in_time_mttm ?W (map Raw w) (length w + length w div q)"
using le by (auto elim: accepts_in_time_mttm_mono)
thus "accepts_in_time_mttm ?W v (length v + length v div q)"
by (simp only: vmap length_map)
qed
qed
qed
show "valid_mttm ?W" by (rule V)
show "det_mttm ?W" by (rule D)
show "Lang_user_wrap ?W = Lang_mttm M" by (rule L)
show "(q + 1) * (3 + 8 * d_0) ≤ card (UNIV :: 'c set)
⟶ (∀v ∈ Lang_mttm ?W. q * (q + 1) * (28 + 8 * d_0 + 8 * b) ≤ length v
⟶ accepts_in_time_mttm ?W v (length v + length v div q))"
proof -
have s0: "(3::nat) + 8 * d_0 = 1 + α + 8 * d_0" using alpha2 by simp
show ?thesis unfolding s0 Kdef[symmetric] by (rule ev)
qed
qed
subsection ‹HU 12.3 in the convention (superlinear ‹T›): the clean bound›
text ‹The nondeterministic superlinear-‹T› headline, restated as a
∗‹constant-free› @{const time_bounded_conv} bound @{term ‹λn. T n div q›}.
Unlike 12.4, no additive constant survives: the raw simulation
constant ‹K› ∗‹and› the finite-control overhead ‹2 N1 + 4› are both
absorbed into a slightly smaller speedup denominator (the raw
construction is run at ‹q + 1›, the headline states ‹q›), because
superlinear ‹T› makes @{thm[source] div_absorb_step}'s premise
‹q (q + 1) C ≤ T n› hold for all long ‹n› with ‹C = K + 2 N1 + 4›.
The machine is @{const finite_patch} of the wrap under the table
‹u ∈ Lang_mttm› of the wrap --- the wrap with the finite-control
small-input cleanup planted on top (short inputs decided by table
lookup in ‹n + 2›, long inputs run the wrap after the O(1) rewind).
The extra hypothesis over the raw
@{thm[source] linear_speedup_HU_12_3_nae} is again ‹Mtime›, and the
cardinality side condition tightens from ‹16 q› to ‹16 (q + 1)› (the
faster inner run).›
theorem linear_speedup_HU_12_3_nae_conv:
fixes M :: "('q, 'a) mttm"
and T :: "nat ⇒ nat"
and q :: nat
assumes wf: "well_formed_mttm M"
and Mtime: "⋀w. w ∈ Lang_mttm M ⟹ accepts_in_time_mttm M w (T (length w))"
and growth: "∀d. ∃N. ∀n. N ≤ n ⟶ d * n ≤ T n"
and q_pos: "0 < q"
and c_large: "16 * (q + 1) ≤ card (UNIV :: ('c :: enum) set)"
and k2: "2 ≤ k_tm M"
obtains W' :: "((('q × ('a, 'c::enum) ae_stage, 'a, 'c ⇒ 'a) wrap_state,
('a, 'c ⇒ 'a) wrap_alphabet) fp_state,
('a, 'c ⇒ 'a) wrap_alphabet) mttm"
where "valid_mttm W'"
and "Lang_user_wrap W' = Lang_mttm M"
and "time_bounded_conv W' (λn. T n div q)"
proof -
let ?W = "encoding_wrap
(alphabet_enlarge M
:: ('q × ('a, 'c) ae_stage, 'c ⇒ 'a) mttm)
(ae_pack (bl_tm M) :: 'a list ⇒ ('c ⇒ 'a))
(card (UNIV :: 'c set))
(Sigma_tm M)"
have q1pos: "0 < q + 1" by simp
obtain K N0 where
Vraw: "valid_mttm ?W" and
Lraw: "Lang_user_wrap ?W = Lang_mttm M" and
Traw: "∀w. set w ⊆ Sigma_tm M
⟶ N0 ≤ length w
⟶ accepts_in_time_mttm M w (T (length w))
⟶ accepts_in_time_user_wrap ?W w (T (length w) div (q + 1) + K)"
by (rule linear_speedup_HU_12_3_nae[OF wf growth q1pos c_large k2])
have blle: "bl_tm ?W ≠ le_tm ?W"
proof -
have le_neq_bl: "le_tm M ≠ bl_tm M" using wf by auto
have "bl_tm (alphabet_enlarge M :: ('q × ('a, 'c) ae_stage, 'c ⇒ 'a) mttm)
≠ le_tm (alphabet_enlarge M :: ('q × ('a, 'c) ae_stage, 'c ⇒ 'a) mttm)"
unfolding bl_tm_alphabet_enlarge le_tm_alphabet_enlarge
using le_neq_bl by (simp add: bl_block_def LE_block_def fun_eq_iff)
thus ?thesis by simp
qed
from growth obtain Nd where
growthN: "∀n. Nd ≤ n ⟶ 3 * q * (q + 1) * n ≤ T n" by blast
define N1 where "N1 = max N0 (max Nd (K + 4))"
have N1_N0: "N0 ≤ N1" and N1_Nd: "Nd ≤ N1" and N1_K: "K + 4 ≤ N1"
unfolding N1_def by auto
let ?W' = "finite_patch ?W (λu. u ∈ Lang_mttm ?W) N1"
have lang': "Lang_mttm ?W' = Lang_mttm ?W"
proof -
have "Lang_mttm ?W' = {u. set u ⊆ Sigma_tm ?W ∧ u ∈ Lang_mttm ?W}"
using finite_patch_language[OF Vraw blle] by simp
also have "… = Lang_mttm ?W" unfolding Lang_mttm_def by auto
finally show ?thesis .
qed
have valid': "valid_mttm ?W'" by (rule finite_patch_valid[OF Vraw])
have Luser': "Lang_user_wrap ?W' = Lang_mttm M"
using lang' Lraw unfolding Lang_user_wrap_def by simp
have conv': "time_bounded_conv ?W' (λn. T n div q)"
unfolding time_bounded_conv_def
proof
fix v assume vW': "v ∈ Lang_mttm ?W'"
hence vW: "v ∈ Lang_mttm ?W" using lang' by simp
hence vSg: "set v ⊆ Sigma_tm ?W" unfolding Lang_mttm_def by simp
show "accepts_in_time_mttm ?W' v (max (length v + 2) ((λn. T n div q) (length v)))"
proof (cases "length v ≤ N1")
case True
have "accepts_in_time_mttm ?W' v (length v + 2)"
using Vraw vSg True vW by (rule fp_short_time)
thus ?thesis by (auto elim: accepts_in_time_mttm_mono)
next
case False
hence N1lt: "N1 < length v" by simp
obtain w where vmap: "v = map Raw w" and wU: "w ∈ Lang_user_wrap ?W"
using vW Lang_mttm_encoding_wrap_ex_Raw by blast
from wU Lraw have wM: "w ∈ Lang_mttm M" by simp
hence wSgM: "set w ⊆ Sigma_tm M" unfolding Lang_mttm_def by simp
from wM have accM: "accepts_in_time_mttm M w (T (length w))" by (rule Mtime)
have lenwv: "length w = length v" using vmap by simp
have N0w: "N0 ≤ length w" using N1lt lenwv N1_N0 by simp
have "accepts_in_time_user_wrap ?W w (T (length w) div (q + 1) + K)"
using Traw wSgM N0w accM by blast
hence accW: "accepts_in_time_mttm ?W v (T (length v) div (q + 1) + K)"
by (simp only: accepts_in_time_user_wrap_def vmap[symmetric] lenwv)
have "accepts_in_time_mttm ?W' v ((T (length v) div (q + 1) + K) + (2 * N1 + 4))"
using Vraw vSg N1lt accW by (rule fp_long_time)
moreover have "(T (length v) div (q + 1) + K) + (2 * N1 + 4) ≤ T (length v) div q"
proof -
have Ndlv: "Nd ≤ length v" using N1_Nd N1lt by simp
have TN: "3 * q * (q + 1) * length v ≤ T (length v)"
using growthN Ndlv by blast
have "K + 2 * N1 + 4 ≤ 3 * length v"
proof -
have "K + 2 * N1 + 4 ≤ 3 * N1" using N1_K by linarith
also have "… ≤ 3 * length v" using N1lt by linarith
finally show ?thesis .
qed
hence "q * (q + 1) * (K + 2 * N1 + 4) ≤ q * (q + 1) * (3 * length v)"
by (rule mult_le_mono2)
also have "q * (q + 1) * (3 * length v) = 3 * q * (q + 1) * length v"
by (simp add: algebra_simps)
also note TN
finally have big: "q * (q + 1) * (K + 2 * N1 + 4) ≤ T (length v)" .
have "T (length v) div (q + 1) + (K + 2 * N1 + 4) ≤ T (length v) div q"
using q_pos big by (rule div_absorb_step)
thus ?thesis by simp
qed
ultimately have "accepts_in_time_mttm ?W' v (T (length v) div q)"
by (auto elim: accepts_in_time_mttm_mono)
thus ?thesis by (auto elim: accepts_in_time_mttm_mono)
qed
qed
show thesis
proof (rule that[of ?W'])
show "valid_mttm ?W'" by (rule valid')
show "Lang_user_wrap ?W' = Lang_mttm M" by (rule Luser')
show "time_bounded_conv ?W' (λn. T n div q)" by (rule conv')
qed
qed
text ‹The deterministic specialisation of
@{thm[source] linear_speedup_HU_12_3_nae_conv}: adds the ‹det›
hypothesis on ‹M› and the determinism-preservation conjunct on the
cleaned machine (via @{thm[source] finite_patch_det}).›
theorem linear_speedup_HU_12_3_dae_conv:
fixes M :: "('q, 'a) mttm"
and T :: "nat ⇒ nat"
and q :: nat
assumes wf: "well_formed_mttm M"
and det: "det_mttm M"
and Mtime: "⋀w. w ∈ Lang_mttm M ⟹ accepts_in_time_mttm M w (T (length w))"
and growth: "∀d. ∃N. ∀n. N ≤ n ⟶ d * n ≤ T n"
and q_pos: "0 < q"
and c_large: "16 * (q + 1) ≤ card (UNIV :: ('c :: enum) set)"
and k2: "2 ≤ k_tm M"
obtains W' :: "((('q × ('a, 'c::enum) ae_stage, 'a, 'c ⇒ 'a) wrap_state,
('a, 'c ⇒ 'a) wrap_alphabet) fp_state,
('a, 'c ⇒ 'a) wrap_alphabet) mttm"
where "valid_mttm W'"
and "det_mttm W'"
and "Lang_user_wrap W' = Lang_mttm M"
and "time_bounded_conv W' (λn. T n div q)"
proof -
let ?W = "encoding_wrap
(alphabet_enlarge M
:: ('q × ('a, 'c) ae_stage, 'c ⇒ 'a) mttm)
(ae_pack (bl_tm M) :: 'a list ⇒ ('c ⇒ 'a))
(card (UNIV :: 'c set))
(Sigma_tm M)"
have q1pos: "0 < q + 1" by simp
obtain K N0 where
Vraw: "valid_mttm ?W" and
Draw: "det_mttm ?W" and
Lraw: "Lang_user_wrap ?W = Lang_mttm M" and
Traw: "∀w. set w ⊆ Sigma_tm M
⟶ N0 ≤ length w
⟶ accepts_in_time_mttm M w (T (length w))
⟶ accepts_in_time_user_wrap ?W w (T (length w) div (q + 1) + K)"
by (rule linear_speedup_HU_12_3_dae[OF wf det growth q1pos c_large k2])
have blle: "bl_tm ?W ≠ le_tm ?W"
proof -
have le_neq_bl: "le_tm M ≠ bl_tm M" using wf by auto
have "bl_tm (alphabet_enlarge M :: ('q × ('a, 'c) ae_stage, 'c ⇒ 'a) mttm)
≠ le_tm (alphabet_enlarge M :: ('q × ('a, 'c) ae_stage, 'c ⇒ 'a) mttm)"
unfolding bl_tm_alphabet_enlarge le_tm_alphabet_enlarge
using le_neq_bl by (simp add: bl_block_def LE_block_def fun_eq_iff)
thus ?thesis by simp
qed
from growth obtain Nd where
growthN: "∀n. Nd ≤ n ⟶ 3 * q * (q + 1) * n ≤ T n" by blast
define N1 where "N1 = max N0 (max Nd (K + 4))"
have N1_N0: "N0 ≤ N1" and N1_Nd: "Nd ≤ N1" and N1_K: "K + 4 ≤ N1"
unfolding N1_def by auto
let ?W' = "finite_patch ?W (λu. u ∈ Lang_mttm ?W) N1"
have lang': "Lang_mttm ?W' = Lang_mttm ?W"
proof -
have "Lang_mttm ?W' = {u. set u ⊆ Sigma_tm ?W ∧ u ∈ Lang_mttm ?W}"
using finite_patch_language[OF Vraw blle] by simp
also have "… = Lang_mttm ?W" unfolding Lang_mttm_def by auto
finally show ?thesis .
qed
have valid': "valid_mttm ?W'" by (rule finite_patch_valid[OF Vraw])
have det': "det_mttm ?W'" by (rule finite_patch_det[OF Vraw blle Draw])
have Luser': "Lang_user_wrap ?W' = Lang_mttm M"
using lang' Lraw unfolding Lang_user_wrap_def by simp
have conv': "time_bounded_conv ?W' (λn. T n div q)"
unfolding time_bounded_conv_def
proof
fix v assume vW': "v ∈ Lang_mttm ?W'"
hence vW: "v ∈ Lang_mttm ?W" using lang' by simp
hence vSg: "set v ⊆ Sigma_tm ?W" unfolding Lang_mttm_def by simp
show "accepts_in_time_mttm ?W' v (max (length v + 2) ((λn. T n div q) (length v)))"
proof (cases "length v ≤ N1")
case True
have "accepts_in_time_mttm ?W' v (length v + 2)"
using Vraw vSg True vW by (rule fp_short_time)
thus ?thesis by (auto elim: accepts_in_time_mttm_mono)
next
case False
hence N1lt: "N1 < length v" by simp
obtain w where vmap: "v = map Raw w" and wU: "w ∈ Lang_user_wrap ?W"
using vW Lang_mttm_encoding_wrap_ex_Raw by blast
from wU Lraw have wM: "w ∈ Lang_mttm M" by simp
hence wSgM: "set w ⊆ Sigma_tm M" unfolding Lang_mttm_def by simp
from wM have accM: "accepts_in_time_mttm M w (T (length w))" by (rule Mtime)
have lenwv: "length w = length v" using vmap by simp
have N0w: "N0 ≤ length w" using N1lt lenwv N1_N0 by simp
have "accepts_in_time_user_wrap ?W w (T (length w) div (q + 1) + K)"
using Traw wSgM N0w accM by blast
hence accW: "accepts_in_time_mttm ?W v (T (length v) div (q + 1) + K)"
by (simp only: accepts_in_time_user_wrap_def vmap[symmetric] lenwv)
have "accepts_in_time_mttm ?W' v ((T (length v) div (q + 1) + K) + (2 * N1 + 4))"
using Vraw vSg N1lt accW by (rule fp_long_time)
moreover have "(T (length v) div (q + 1) + K) + (2 * N1 + 4) ≤ T (length v) div q"
proof -
have Ndlv: "Nd ≤ length v" using N1_Nd N1lt by simp
have TN: "3 * q * (q + 1) * length v ≤ T (length v)"
using growthN Ndlv by blast
have "K + 2 * N1 + 4 ≤ 3 * length v"
proof -
have "K + 2 * N1 + 4 ≤ 3 * N1" using N1_K by linarith
also have "… ≤ 3 * length v" using N1lt by linarith
finally show ?thesis .
qed
hence "q * (q + 1) * (K + 2 * N1 + 4) ≤ q * (q + 1) * (3 * length v)"
by (rule mult_le_mono2)
also have "q * (q + 1) * (3 * length v) = 3 * q * (q + 1) * length v"
by (simp add: algebra_simps)
also note TN
finally have big: "q * (q + 1) * (K + 2 * N1 + 4) ≤ T (length v)" .
have "T (length v) div (q + 1) + (K + 2 * N1 + 4) ≤ T (length v) div q"
using q_pos big by (rule div_absorb_step)
thus ?thesis by simp
qed
ultimately have "accepts_in_time_mttm ?W' v (T (length v) div q)"
by (auto elim: accepts_in_time_mttm_mono)
thus ?thesis by (auto elim: accepts_in_time_mttm_mono)
qed
qed
show thesis
proof (rule that[of ?W'])
show "valid_mttm ?W'" by (rule valid')
show "det_mttm ?W'" by (rule det')
show "Lang_user_wrap ?W' = Lang_mttm M" by (rule Luser')
show "time_bounded_conv ?W' (λn. T n div q)" by (rule conv')
qed
qed
end