Theory Multitape_Alphabet_Enlargement.AlphabetEnlargement
theory AlphabetEnlargement
imports AlphabetEnlargement_Acceptance
begin
text ‹The three top-level theorems characterising
‹alphabet_enlarge›, at the end of the forward-simulation
chain that begins in
‹AlphabetEnlargement_ComputeCorrect›: the linear time
bound ‹alphabet_enlarge_time›, well-formedness
preservation ‹alphabet_enlarge_wf›, and forward language
preservation ‹alphabet_enlarge_language_forward›. The
reverse direction of the language biconditional
(‹alphabet_enlarge_language›) and the nondeterministic
corollary live in ‹AlphabetEnlargement_Reverse›.›
subsection ‹Top-level theorems›
text ‹Time bound (Form 2 / encoded form): ‹M' = alphabet_enlarge M›
on input ‹encode_input (bl_tm M) w› runs in time
‹α ⋅ ⌈n/c⌉ + 8 ⋅ ⌈T(n) / c⌉ + f› for structural
additive constants ‹α, f› independent of ‹M›, where
‹c = card (UNIV :: 'c set)› is the grouping factor and ‹n› is
‹M›'s input length ‹length w›. ‹M'›'s input is the
consolidated block-encoding ‹encode_input (bl_tm M) w› of
length ‹⌈n/c⌉›.
This is the linear-speedup theorem in **encoded form** (Form 2):
the input bijection
‹encode_input› is exposed externally; ‹M'›'s job is to
validate the encoded input's shape and simulate ‹M›. The
classical same-alphabet statement (Form 1 --- Hartmanis and Stearns
\<^cite>‹‹Theorem 2› in "Hartmanis1965:computational"›, modernised as
Hopcroft and Ullman \<^cite>‹‹Theorem 12.3› in "Hopcroft1979:introduction"›)
follows as a corollary by
composing this with a generic substrate-level wrap combinator
that prepends an inline encoder pass.
Cost breakdown:
▪ ‹α ⋅ ⌈n/c⌉›: validation-phase pass over the
encoded input of length ‹⌈n/c⌉› (forward scan + return
scan; ‹α = 2›).
▪ ‹8 ⋅ ⌈T(n) / c⌉›: 8 ‹M'›-substeps per simulated
‹c›-fold ‹M›-step group; ‹⌈T(n)/c⌉› such groups suffice
to cover ‹M›'s ‹T(n)›-step accepting path.
▪ ‹f›: validation-phase setup additive (‹f_v›).
The ‹T(n)› argument (not ‹T(c ⋅ n)›) reflects that
‹M›'s and ‹M'›'s input represent the same problem instance
of size ‹n›; ‹M'›'s tape just compresses it by a factor
of ‹c›.
**Weak acceptance shape.** Hypothesis and conclusion both at
‹accepts_in_time_mttm› (the existential accepting-path
predicate). The constants ‹α›, ‹f›
depend only on ‹M› (and the type-level ‹'c›), not
on ‹w›; the universal-‹w› form inside ‹obtains› encodes
this.
**Form 1 follows as a corollary** by composing with the
inline-encoder wrap combinator (‹encoding_wrap› in
‹Wrap_Defs.thy›). Theorem 12.3's setup-phase
cost ‹n + ⌈n/m⌉› appears in the wrapped form as the
inline encoder's cost (‹O(n)›) plus this lemma's
‹⌈n/c⌉› validation cost. Together with the speedup
factor ‹1/c› applied to ‹T(n)›, this gives the textbook
bound ‹c_0 ⋅ T(n)› for any ‹c_0 > 0› when
‹inf T(n)/n = ∞› (Theorem 12.3); the companion
\<^cite>‹‹Theorem 12.4› in "Hopcroft1979:introduction"› patches the
linear case ‹T(n) = Θ(n)› via a different choice of ‹c›.›
theorem alphabet_enlarge_time_explicit:
fixes M :: "('q, 'a) mttm"
and T :: "nat ⇒ nat"
assumes wf: "well_formed_mttm M"
shows "∀w. set w ⊆ Sigma_tm M
⟶ accepts_in_time_mttm M w (T (length w))
⟶ accepts_in_time_mttm
(alphabet_enlarge M
:: ('q × ('a, ('c :: enum)) ae_stage,
'c ⇒ 'a) mttm)
(encode_input (bl_tm M) w)
(2 * ((length w + card (UNIV :: 'c set) - 1)
div card (UNIV :: 'c set))
+ 8 * ((T (length w) + card (UNIV :: 'c set) - 1)
div card (UNIV :: 'c set))
+ 4)"
proof -
from wf have vM: "valid_mttm M"
and lu: "le_unique M"
and s_neq_t: "s_tm M ≠ t_tm M"
and s_neq_r: "s_tm M ≠ r_tm M"
and le_neq_bl: "le_tm M ≠ bl_tm M"
by auto
let ?c = "card (UNIV :: 'c set)"
let ?M' = "alphabet_enlarge M
:: ('q × ('a, 'c) ae_stage, 'c ⇒ 'a) mttm"
show "∀w. set w ⊆ Sigma_tm M
⟶ accepts_in_time_mttm M w (T (length w))
⟶ accepts_in_time_mttm ?M' (encode_input (bl_tm M) w)
(2 * ((length w + ?c - 1) div ?c)
+ 8 * ((T (length w) + ?c - 1) div ?c)
+ 4)"
proof (intro allI impI)
fix w :: "'a list"
assume w_sub: "set w ⊆ Sigma_tm M"
assume m_acc: "accepts_in_time_mttm M w (T (length w))"
let ?ew = "encode_input (bl_tm M) w
:: ('c ⇒ 'a) list"
have ew_sub: "set ?ew ⊆ gamma_block (Sigma_tm M ∪ {bl_tm M})"
by (rule encode_input_in_gamma_block[OF w_sub])
have ew_wf: "ae_input_well_formed (bl_tm M) ?ew"
by (rule encode_input_well_formed[OF vM w_sub])
have s_in_Q: "s_tm M ∈ Q_tm M"
by (rule s_tm_in_Q_tm[OF vM])
let ?c1 = "Config⇩M (s_tm M, init_offset,
init_buffer (le_tm M), init_dest, SS1)
(mt_tape (ae_init_config M ?ew))
(λ_ :: nat. 0)
:: ('c ⇒ 'a,
'q × ('a, 'c) ae_stage) mt_config"
have val_chain:
"(ae_init_config M ?ew, ?c1)
∈ mttm_step (alphabet_enlarge_delta M)
^^ (2 * length ?ew + 4)"
by (rule ae_validation_well_formed_to_SS1
[OF vM ew_sub ew_wf s_in_Q s_neq_t s_neq_r le_neq_bl])
have le_anchor: "∀kk<k_tm M. mt_tape ?c1 kk 0 = LE_block (le_tm M)"
proof (intro allI impI)
fix kk assume kk_lt: "kk < k_tm M"
have "mt_tape ?c1 kk 0 = mt_tape (ae_init_config M ?ew) kk 0"
by simp
also have "… = LE_block (le_tm M)"
by (rule ae_init_config_tape_le[OF kk_lt])
finally show "mt_tape ?c1 kk 0 = LE_block (le_tm M)" .
qed
have buf_gamma: "ae_buffer_in_gamma_block M ?c1"
unfolding ae_buffer_in_gamma_block_def init_buffer_def
using LE_block_in_gamma_block[OF valid_mttm_LE_in_Gamma[OF vM]]
by simp
have tape_corr:
"∀k<k_tm M. ae_tape_correspondence (le_tm M)
(mt_tape (init_config_mttm M w) k)
(mt_tape (ae_init_config M ?ew) k)"
by (rule ae_tape_correspondence_init[OF vM w_sub])
have subst_pos_zero:
"∀k. mt_pos (init_config_mttm M w) k = 0"
by (cases M) simp
have c1_pos_zero: "∀k. mt_pos ?c1 k = 0" by simp
have pos_corr_c1:
"∀k. mt_pos (init_config_mttm M w) k
= ae_decode_pos (mt_pos ?c1 k)
((init_offset :: nat ⇒ 'c) k)"
using c1_pos_zero subst_pos_zero
unfolding ae_decode_pos_def by simp
have qM_subst: "mt_state (init_config_mttm M w) = s_tm M"
by (cases M) simp
have c1_state:
"mt_state ?c1 = (s_tm M, init_offset,
init_buffer (le_tm M), init_dest, SS1)"
by simp
have gamma_block_c1: "ae_tape_in_gamma_block M ?c1"
unfolding ae_tape_in_gamma_block_def
proof (intro conjI)
show "∀k p. mt_tape ?c1 k p ∈ gamma_block (Γ_tm M)"
using ae_init_config_in_gamma_block[OF vM ew_sub] by simp
show "∀j≥k_tm M. ∀p. mt_tape ?c1 j p = bl_block (bl_tm M)"
by (simp add: ae_init_config_tape_blank_tail)
qed
have sim: "ae_simulates M (init_config_mttm M w) ?c1"
unfolding ae_simulates_def Let_def c1_state
using qM_subst tape_corr pos_corr_c1 gamma_block_c1
s_neq_t s_neq_r by simp
obtain n_sim c'' where
n_sim_bd:
"n_sim ≤ 8 * ((T (length w) + ?c - 1) div ?c)"
and sim_chain:
"(?c1, c'') ∈ mttm_step (alphabet_enlarge_delta M) ^^ n_sim"
and c''_state: "mt_state c'' = (t_tm M, init_stage (le_tm M))"
using ae_simulation_phase_step_count
[where M = M and T = T and u = w and c' = ?c1,
OF vM lu m_acc w_sub sim buf_gamma le_anchor
s_neq_t s_neq_r le_neq_bl]
by metis
have chain_compose:
"(ae_init_config M ?ew, c'')
∈ mttm_step (alphabet_enlarge_delta M)
^^ ((2 * length ?ew + 4) + n_sim)"
using val_chain sim_chain by (auto simp: relpow_add)
have len_ew: "length ?ew = (length w + ?c - 1) div ?c"
by (rule length_encode_input)
let ?total = "(2 * length ?ew + 4) + n_sim"
let ?target = "2 * ((length w + ?c - 1) div ?c)
+ 8 * ((T (length w) + ?c - 1) div ?c)
+ 4"
have bound: "?total ≤ ?target"
using n_sim_bd len_ew by simp
have init_bridge:
"init_config_mttm ?M' ?ew = ae_init_config M ?ew"
by (rule init_config_alphabet_enlarge)
have t_bridge: "t_tm ?M' = (t_tm M, init_stage (le_tm M))"
by (rule t_tm_alphabet_enlarge)
have delta_bridge:
"delta_tm ?M' = alphabet_enlarge_delta M"
by (rule delta_tm_alphabet_enlarge)
show "accepts_in_time_mttm ?M' ?ew ?target"
unfolding accepts_in_time_mttm_def
proof (intro exI conjI)
show "?total ≤ ?target" using bound .
show "(init_config_mttm ?M' ?ew, c'')
∈ (mttm_step (delta_tm ?M')) ^^ ?total"
using chain_compose init_bridge delta_bridge by simp
show "mt_state c'' = t_tm ?M'"
using c''_state t_bridge by simp
qed
qed
qed
text ‹The classical HU-form of the linear-speedup time bound: the
additive constants ‹α›, ‹f› instantiated at ‹α = 2›, ‹f = 4›
from ‹alphabet_enlarge_time_explicit›. The per-block simulation
constant ‹8› and the speedup divisor ‹card (UNIV :: 'c set)› are already
explicit in the statement.›
theorem alphabet_enlarge_time:
fixes M :: "('q, 'a) mttm"
and T :: "nat ⇒ nat"
assumes wf: "well_formed_mttm M"
obtains α f :: nat
where "∀w. set w ⊆ Sigma_tm M
⟶ accepts_in_time_mttm M w (T (length w))
⟶ accepts_in_time_mttm
(alphabet_enlarge M
:: ('q × ('a, ('c :: enum)) ae_stage,
'c ⇒ 'a) mttm)
(encode_input (bl_tm M) w)
(α * ((length w + card (UNIV :: 'c set) - 1)
div card (UNIV :: 'c set))
+ 8 * ((T (length w) + card (UNIV :: 'c set) - 1)
div card (UNIV :: 'c set))
+ f)"
proof (rule that[of 2 4])
show "∀w. set w ⊆ Sigma_tm M
⟶ accepts_in_time_mttm M w (T (length w))
⟶ accepts_in_time_mttm
(alphabet_enlarge M
:: ('q × ('a, ('c :: enum)) ae_stage,
'c ⇒ 'a) mttm)
(encode_input (bl_tm M) w)
(2 * ((length w + card (UNIV :: 'c set) - 1)
div card (UNIV :: 'c set))
+ 8 * ((T (length w) + card (UNIV :: 'c set) - 1)
div card (UNIV :: 'c set))
+ 4)"
by (rule alphabet_enlarge_time_explicit[OF wf])
qed
text ‹Forward language inclusion modulo input encoding: a word
‹w› with ‹set w ⊆ Σ_M› that is in
‹M›'s language has its canonical block-encoding (using
‹M›'s blank for padding) in
‹M' = alphabet_enlarge M›'s language. This is the
forward leg of the language-equivalence claim; the reverse leg
(‹encode_input w ∈ Lang_mttm M' ⟹ w ∈ Lang_mttm M›)
holds for every well-formed ‹M› --- with no determinism
hypothesis, the original ‹det_mttm M› dependency having been
removed in refactoring --- and lives in
‹AlphabetEnlargement_Reverse.thy› as the biconditional
‹alphabet_enlarge_language›.
Hypotheses align with ‹alphabet_enlarge_time›:
‹s ≠ t›, ‹s ≠ r›, ‹le ≠ bl›. The first
two would be redundant if we manually handled the degenerate
always-accept (‹s = t›) and always-reject (‹s = r›)
cases, but matching the ‹_time› signature keeps the call
sites uniform. ‹le ≠ bl› is genuinely necessary: the
simulation infrastructure requires it (compute substep's buffer-
write composition), and the ‹Sigma_tm› containment for
encoded inputs uses it to exclude ‹LE_block›.
The ‹set w ⊆ Sigma_tm M› antecedent inside the
‹∀w› is required: without it the inclusion fails for
‹w› containing blank symbols (such ‹w› are outside
‹Lang_mttm M› by the substrate's ‹Lang_mttm›
definition, but their encodings can still pass M'-validation
and be M'-accepted).
Strategy: extract an accepting M-path of length ‹n0›;
instantiate ‹alphabet_enlarge_time› with
‹T = (λ_. n0)› to obtain a bounded M'-witness; drop the
bound and conclude.›
theorem alphabet_enlarge_language_forward:
fixes M :: "('q, 'a) mttm"
assumes wf: "well_formed_mttm M"
shows "∀w. set w ⊆ Sigma_tm M
⟶ w ∈ Lang_mttm M
⟶ encode_input (bl_tm M) w ∈ Lang_mttm
(alphabet_enlarge M
:: ('q × ('a, ('c :: enum)) ae_stage,
'c ⇒ 'a) mttm)"
proof -
from wf have vM: "valid_mttm M"
and lu: "le_unique M"
and s_neq_t: "s_tm M ≠ t_tm M"
and s_neq_r: "s_tm M ≠ r_tm M"
and le_neq_bl: "le_tm M ≠ bl_tm M"
by auto
let ?c = "card (UNIV :: 'c set)"
let ?M' = "alphabet_enlarge M
:: ('q × ('a, 'c) ae_stage, 'c ⇒ 'a) mttm"
show ?thesis
proof (intro allI impI)
fix w :: "'a list"
assume w_sub: "set w ⊆ Sigma_tm M"
assume w_in_M: "w ∈ Lang_mttm M"
have enc_in_gamma:
"set (encode_input (bl_tm M) w :: ('c ⇒ 'a) list)
⊆ gamma_block (Sigma_tm M ∪ {bl_tm M})"
by (rule encode_input_in_gamma_block[OF w_sub])
have enc_no_bl:
"bl_block (bl_tm M)
∉ set (encode_input (bl_tm M) w :: ('c ⇒ 'a) list)"
by (rule encode_input_no_bl_block[OF vM w_sub])
have enc_no_LE:
"LE_block (le_tm M)
∉ set (encode_input (bl_tm M) w :: ('c ⇒ 'a) list)"
by (rule encode_input_no_LE_block[OF vM w_sub])
have enc_sub:
"set (encode_input (bl_tm M) w :: ('c ⇒ 'a) list)
⊆ Sigma_tm ?M'"
unfolding Sigma_tm_alphabet_enlarge
using enc_in_gamma enc_no_bl enc_no_LE by blast
from w_in_M obtain wM' nM where
m_path: "(init_config_mttm M w,
Config⇩M (t_tm M) wM' nM)
∈ (mttm_step (delta_tm M))⇧*"
unfolding Lang_mttm_def by blast
obtain n0 where m_pow:
"(init_config_mttm M w, Config⇩M (t_tm M) wM' nM)
∈ (mttm_step (delta_tm M)) ^^ n0"
using m_path rtrancl_imp_relpow by metis
have m_acc: "accepts_in_time_mttm M w n0"
unfolding accepts_in_time_mttm_def
proof (intro exI conjI)
show "(n0 :: nat) ≤ n0" by simp
show "(init_config_mttm M w, Config⇩M (t_tm M) wM' nM)
∈ mttm_step (delta_tm M) ^^ n0"
using m_pow .
show "mt_state (Config⇩M (t_tm M) wM' nM) = t_tm M"
by simp
qed
obtain α f :: nat where AE_time:
"∀w_arg. set w_arg ⊆ Sigma_tm M
⟶ accepts_in_time_mttm M w_arg n0
⟶ accepts_in_time_mttm ?M'
(encode_input (bl_tm M) w_arg)
(α * ((length w_arg + ?c - 1) div ?c)
+ 8 * ((n0 + ?c - 1) div ?c) + f)"
by (rule alphabet_enlarge_time
[where T = "λ_. n0", OF wf])
from AE_time w_sub m_acc have m'_acc:
"accepts_in_time_mttm ?M' (encode_input (bl_tm M) w)
(α * ((length w + ?c - 1) div ?c)
+ 8 * ((n0 + ?c - 1) div ?c) + f)"
by blast
from m'_acc obtain n_m' c_acc where
run: "(init_config_mttm ?M' (encode_input (bl_tm M) w),
c_acc)
∈ (mttm_step (delta_tm ?M')) ^^ n_m'"
and acc: "mt_state c_acc = t_tm ?M'"
unfolding accepts_in_time_mttm_def by blast
obtain wM_acc' nM_acc where c_acc_eq:
"c_acc = Config⇩M (t_tm ?M') wM_acc' nM_acc"
using acc by (cases c_acc) simp
have run_star:
"(init_config_mttm ?M' (encode_input (bl_tm M) w),
Config⇩M (t_tm ?M') wM_acc' nM_acc)
∈ (mttm_step (delta_tm ?M'))⇧*"
using run c_acc_eq relpow_imp_rtrancl by metis
show "encode_input (bl_tm M) w ∈ Lang_mttm ?M'"
unfolding Lang_mttm_def
using enc_sub run_star by blast
qed
qed
end