Writing a prefix before a probabilistic computation

A deterministic preparation restores the input head and blank work tapes after writing a prefix. Shared-tape sequencing then runs the probabilistic source on its original input. Both phases actually halt within the sum of their bounds; every instruction of preparation is charged.

Main results

• Turing.MultiTapePTM.eval_runClosedConfigFrom_seq_prependOutput: retain a prepared prefix.
• Turing.MultiTapePTM.seq_prependOutput_halted: add the two actual halting bounds.

References

Adapted from Computability/Probabilistic/Realization/Composition.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using the shared sequencing compiler.

theorem Turing.MultiTapePTM.runClosedConfigFrom_prependOutput {k : ℕ} {Symbol State : Type} {input : List Symbol} (machine : MultiTapePTM k Symbol State) (fuel : ℕ) (cfg : MultiTapeMachine.Config k Symbol State Empty input) (pre : List Symbol) : machine.runClosedConfigFrom fuel (cfg.prependOutput pre) = (fun (final : MultiTapeMachine.Config k Symbol State Empty input) => final.prependOutput pre) <$> machine.runClosedConfigFrom fuel cfg

An unreadable output prefix preserves the entire closed execution program.

theorem Turing.MultiTapePTM.eval_runClosedConfigFrom_seq_prependOutput {k : ℕ} {Symbol State₀ State₁ : Type} (prepare : MultiTapeTM k Symbol State₀) (source : MultiTapePTM k Symbol State₁) (input pre : List Symbol) (prepareTime runTime : ℕ) (hprepare : MultiTapeTM.runFrom (prepare.initCfg input) prepareTime = wordsCfg input none (fun (x : Fin k) => []) pre) (hsource : ∀ final ∈ (source.runClosedConfigFrom runTime (MultiTapeMachine.initialConfig source input)).eval.support, final.tapes.state = none) : (((ofDeterministic prepare).seq source).runClosedConfigFrom (prepareTime + runTime) (MultiTapeMachine.initialConfig ((ofDeterministic prepare).seq source) input)).eval = PMF.map (fun (final : MultiTapeMachine.Config k Symbol State₁ Empty input) => MultiTapeMachine.Sequential.right (final.prependOutput pre)) (source.runClosedConfigFrom runTime (MultiTapeMachine.initialConfig source input)).eval

A workspace-restoring preparation retains the prefix and the source distribution.

theorem Turing.MultiTapePTM.seq_prependOutput_halted {k : ℕ} {Symbol State₀ State₁ : Type} (prepare : MultiTapeTM k Symbol State₀) (source : MultiTapePTM k Symbol State₁) (input pre : List Symbol) (prepareTime runTime : ℕ) (hprepare : MultiTapeTM.runFrom (prepare.initCfg input) prepareTime = wordsCfg input none (fun (x : Fin k) => []) pre) (hsource : ∀ final ∈ (source.runClosedConfigFrom runTime (MultiTapeMachine.initialConfig source input)).eval.support, final.tapes.state = none) (final : MultiTapeMachine.Config k Symbol (State₀ ⊕ State₁) Empty input) : final ∈ (((ofDeterministic prepare).seq source).runClosedConfigFrom (prepareTime + runTime) (MultiTapeMachine.initialConfig ((ofDeterministic prepare).seq source) input)).eval.support → final.tapes.state = none

The prepared-prefix computation actually halts within the sum of the phase bounds.

theorem Turing.MultiTapePTM.eval_seq_prependOutput {k : ℕ} {Symbol State₀ State₁ : Type} (prepare : MultiTapeTM k Symbol State₀) (source : MultiTapePTM k Symbol State₁) (input pre : List Symbol) (prepareTime runTime : ℕ) (hprepare : MultiTapeTM.runFrom (prepare.initCfg input) prepareTime = wordsCfg input none (fun (x : Fin k) => []) pre) (hsource : ∀ final ∈ (source.runClosedConfigFrom runTime (MultiTapeMachine.initialConfig source input)).eval.support, final.tapes.state = none) : (((ofDeterministic prepare).seq source).runClosed (prepareTime + runTime) input).eval = PMF.map (fun (x : List Symbol) => pre ++ x) (source.runClosed runTime input).eval

The final output consists of the prepared prefix followed by the sampled source output.