Sequential composition after function computation #
TM.compositionTM tmF tmG is an executable deterministic machine that runs
tmF, copies its delimited output onto a fresh virtual-input tape, and then
runs tmG on that output. Work tapes of the two machines occupy disjoint
blocks, and the intermediate raw output may contain arbitrary junk after its
first delimiter.
Main result #
TM.compositionTM_computesInTime— correctness with a monotone coarse time boundTM.compositionTM_decidesInTime— function computation followed by a decider
theorem
Complexity.TM.compositionTM_computesInTime
{nf ng : ℕ}
{tmF : TM nf}
{tmG : TM ng}
{f g : List Bool → List Bool}
{TF TG : ℕ → ℕ}
(hF : tmF.ComputesInTime f TF)
(hG : tmG.ComputesInTime g TG)
(hmono : Monotone TG)
:
(tmF.compositionTM tmG).ComputesInTime (g ∘ f) fun (n : ℕ) => 4 * TF n + 11 + TG (TF n)
Sequential deterministic function composition. The first computation,
two copy/rewind passes, four phase transitions, and the second computation fit
within 4 * TF(n) + 11 + TG(TF(n)) whenever TG is monotone.
theorem
Complexity.TM.compositionTM_decidesInTime
{nf ng : ℕ}
{tmF : TM nf}
{tmG : TM ng}
{f : List Bool → List Bool}
{L : Language}
{TF TG : ℕ → ℕ}
(hF : tmF.ComputesInTime f TF)
(hG : tmG.DecidesInTime L TG)
(hmono : Monotone TG)
:
(tmF.compositionTM tmG).DecidesInTime (f ⁻¹' L) fun (n : ℕ) => 4 * TF n + 11 + TG (TF n)
Sequential deterministic preprocessing followed by a language decider. The composite decides the preimage language with the same coarse monotone time bound as function composition.