Word-configuration phases and tidy probabilistic oracle specifications

RunsWords and ComputesTidily express that a probabilistic oracle machine starts from a word configuration with empty query buffers, halts within a strict step bound with empty query buffers, and realizes the exact joint distribution of resulting tape words, emitted output and external oracle state.

Main definitions

• Turing.MultiTapePTM.runOracleConfigFrom: clocked configuration run with fair coins and named word queries.
• Turing.MultiTapePTM.RunsWords: word-configuration phase specification preserving external oracle state and empty query buffers.
• Turing.MultiTapePTM.ComputesTidily: tidy computation from blank work tapes to blank work tapes.

Main results

• Turing.MultiTapePTM.RunsWords.of_transformsTapes: lift deterministic TransformsTapes phases.
• Turing.MultiTapePTM.RunsWords.seq_bind: sequence two RunsWords phases.
• Turing.MultiTapePTM.RunsWords.of_nil_output: an initial output prefix is retained automatically.
• Turing.MultiTapePTM.RunsWords.of_first_step_mapState: lift a RunsWords specification across a deterministic first-step dispatch into a state-mapped submachine.
• Turing.MultiTapePTM.ComputesTidily.length_output_le: any supported output of a tidy run has length at most the step budget.

References

RunsWords and ComputesTidily adapt the deterministic TransformsTapes and tidy-machine notions of cslib's Plumbing/TransformsTapes and Plumbing/Tidy, by Christian Reitwiessner, in the run form of crei:crei/tidy-universal @7f7c0696, to the probabilistic oracle machines of the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8.

theorem Turing.MultiTapePTM.tapeOfList_injective {Symbol : Type} : Function.Injective tapeOfList

tapeOfList is injective on words.

theorem Turing.MultiTapePTM.wordsCfg_injective {k : ℕ} {Symbol State : Type} {input : List Symbol} {q : Option State} {ws₁ ws₂ : Fin k → List Symbol} {out₀ e₁ e₂ : List Symbol} (h : wordsCfg input q ws₁ (out₀ ++ e₁) = wordsCfg input q ws₂ (out₀ ++ e₂)) : ws₁ = ws₂ ∧ e₁ = e₂

A wordsCfg uniquely determines its work-tape words and the suffix appended to out₀.

noncomputable def Turing.MultiTapePTM.runOracleConfigFrom {k : ℕ} {Symbol State Operation : Type} {input : List Symbol} [DecidableEq Operation] (machine : MultiTapePTM k Symbol State Operation) (fuel : ℕ) (cfg : MultiTapeMachine.Config k Symbol State Operation input) : Cslib.ProbOracleComp (fun (x : Operation × List Symbol) => List Symbol) (MultiTapeMachine.Config k Symbol State Operation input)

Retain the complete configuration of an open fair-coin run with external word queries.

theorem Turing.MultiTapePTM.runOracle_eq_map {k : ℕ} {Symbol State Operation : Type} [DecidableEq Operation] (machine : MultiTapePTM k Symbol State Operation) (fuel : ℕ) (input : List Symbol) : machine.runOracle fuel input = (fun (final : MultiTapeMachine.Config k Symbol State Operation input) => final.tapes.output) <$> machine.runOracleConfigFrom fuel (MultiTapeMachine.initialConfig machine input)

runOracle is the output projection of runOracleConfigFrom from the initial configuration.

theorem Turing.MultiTapePTM.run_interpret_sample_uniform_bool {Symbol Operation OracleState : Type} (oracle : Operation × List Symbol → StateT OracleState PMF (List Symbol)) (s : OracleState) : (Cslib.OracleComp.interpret (Cslib.ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (Cslib.ProbComp.unifOracle n)) oracle) (Cslib.ProbOracleComp.sample (Cslib.ProbComp.uniform Bool))).run s = PMF.map (fun (bit : Bool) => (bit, s)) (Cslib.Probability.PMF.uniformOfFintype Bool)

Drawing one fair bit in ProbOracleComp leaves the external oracle state unchanged.

theorem Turing.MultiTapePTM.run_interpret_runOracleConfigFrom_add_of_halted {k : ℕ} {Symbol State Operation OracleState : Type} {input : List Symbol} [DecidableEq Operation] (machine : MultiTapePTM k Symbol State Operation) (oracle : Operation × List Symbol → StateT OracleState PMF (List Symbol)) (cfg : MultiTapeMachine.Config k Symbol State Operation input) (fuel padding : ℕ) (s : OracleState) (hhalt : ∀ final ∈ ((Cslib.OracleComp.interpret (Cslib.ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (Cslib.ProbComp.unifOracle n)) oracle) (machine.runOracleConfigFrom fuel cfg)).run s).support, final.1.tapes.state = none) : (Cslib.OracleComp.interpret (Cslib.ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (Cslib.ProbComp.unifOracle n)) oracle) (machine.runOracleConfigFrom (fuel + padding) cfg)).run s = (Cslib.OracleComp.interpret (Cslib.ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (Cslib.ProbComp.unifOracle n)) oracle) (machine.runOracleConfigFrom fuel cfg)).run s

Padding a halted oracle run preserves the joint configuration and external state distribution.

theorem Turing.MultiTapePTM.run_interpret_runOracleConfigFrom_eq_of_halted {k : ℕ} {Symbol State Operation OracleState : Type} {input : List Symbol} [DecidableEq Operation] (machine : MultiTapePTM k Symbol State Operation) (oracle : Operation × List Symbol → StateT OracleState PMF (List Symbol)) (cfg : MultiTapeMachine.Config k Symbol State Operation input) {fuel larger : ℕ} (hle : fuel ≤ larger) (s : OracleState) (hhalt : ∀ final ∈ ((Cslib.OracleComp.interpret (Cslib.ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (Cslib.ProbComp.unifOracle n)) oracle) (machine.runOracleConfigFrom fuel cfg)).run s).support, final.1.tapes.state = none) : (Cslib.OracleComp.interpret (Cslib.ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (Cslib.ProbComp.unifOracle n)) oracle) (machine.runOracleConfigFrom larger cfg)).run s = (Cslib.OracleComp.interpret (Cslib.ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (Cslib.ProbComp.unifOracle n)) oracle) (machine.runOracleConfigFrom fuel cfg)).run s

Any larger clock gives the same joint configuration and external state distribution after a halting bound.

theorem Turing.MultiTapePTM.run_interpret_runOracleConfigFrom_ofDeterministic {k : ℕ} {Symbol State Operation OracleState : Type} {input : List Symbol} [DecidableEq Operation] (machine : MultiTapeTM k Symbol State) (oracle : Operation × List Symbol → StateT OracleState PMF (List Symbol)) (fuel : ℕ) (cfg : MultiTapeMachine.Config k Symbol State Operation input) (s : OracleState) : (Cslib.OracleComp.interpret (Cslib.ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (Cslib.ProbComp.unifOracle n)) oracle) ((ofDeterministic machine).runOracleConfigFrom fuel cfg)).run s = PMF.pure ({ tapes := MultiTapeTM.runFrom cfg.tapes fuel, channels := cfg.channels }, s)

A deterministic machine embedded in MultiTapePTM preserves channels and external state.

theorem Turing.MultiTapePTM.run_interpret_runOracleConfigFrom_seq {k : ℕ} {Symbol State₀ State₁ Operation OracleState : Type} {input : List Symbol} [DecidableEq Operation] (first : MultiTapePTM k Symbol State₀ Operation) (second : MultiTapePTM k Symbol State₁ Operation) (oracle : Operation × List Symbol → StateT OracleState PMF (List Symbol)) (cfg : MultiTapeMachine.Config k Symbol State₀ Operation input) (t₁ t₂ : ℕ) (s : OracleState) (h₁ : ∀ result ∈ ((Cslib.OracleComp.interpret (Cslib.ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (Cslib.ProbComp.unifOracle n)) oracle) (first.runOracleConfigFrom t₁ cfg)).run s).support, result.1.tapes.state = none) (h₂ : ∀ result ∈ ((Cslib.OracleComp.interpret (Cslib.ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (Cslib.ProbComp.unifOracle n)) oracle) (first.runOracleConfigFrom t₁ cfg)).run s).support, ∀ final ∈ ((Cslib.OracleComp.interpret (Cslib.ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (Cslib.ProbComp.unifOracle n)) oracle) (second.runOracleConfigFrom t₂ (MultiTapeMachine.Sequential.start second result.1))).run result.2).support, final.1.tapes.state = none) : (Cslib.OracleComp.interpret (Cslib.ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (Cslib.ProbComp.unifOracle n)) oracle) ((first.seq second).runOracleConfigFrom (t₁ + t₂) (MultiTapeMachine.Sequential.left second cfg))).run s = ((Cslib.OracleComp.interpret (Cslib.ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (Cslib.ProbComp.unifOracle n)) oracle) (first.runOracleConfigFrom t₁ cfg)).run s).bind fun (result : MultiTapeMachine.Config k Symbol State₀ Operation input × OracleState) => PMF.map (fun (x : MultiTapeMachine.Config k Symbol State₁ Operation input × OracleState) => match x with | (final, s') => (MultiTapeMachine.Sequential.right final, s')) ((Cslib.OracleComp.interpret (Cslib.ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (Cslib.ProbComp.unifOracle n)) oracle) (second.runOracleConfigFrom t₂ (MultiTapeMachine.Sequential.start second result.1))).run result.2)

Sequencing law for runOracleConfigFrom when both phases halt on all supported paths.

theorem Turing.MultiTapePTM.run_interpret_runOracleConfigFrom_succ_step {k : ℕ} {Symbol State Operation OracleState : Type} {input : List Symbol} [DecidableEq Operation] (machine : MultiTapePTM k Symbol State Operation) (oracle : Operation × List Symbol → StateT OracleState PMF (List Symbol)) (fuel : ℕ) (cfg : MultiTapeMachine.Config k Symbol State Operation input) (s : OracleState) {state : State} (hstate : cfg.tapes.state = some state) {action : Action k Symbol State} {symbol : Operation → Option Symbol} {move : Operation → SignType} (htr : ∀ (bit : Bool), machine.tr state cfg.tapes.inputSymbol cfg.tapes.workTapeSymbols cfg.answerSymbols bit = MultiTapeMachine.Action.step action symbol move) : (Cslib.OracleComp.interpret (Cslib.ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (Cslib.ProbComp.unifOracle n)) oracle) (machine.runOracleConfigFrom (fuel + 1) cfg)).run s = (Cslib.OracleComp.interpret (Cslib.ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (Cslib.ProbComp.unifOracle n)) oracle) (machine.runOracleConfigFrom fuel (cfg.step action symbol move))).run s

A live step whose transition does not depend on the coin bit advances the configuration deterministically while preserving the external oracle state.

theorem Turing.MultiTapePTM.run_interpret_runOracleConfigFrom_succ_query {k : ℕ} {Symbol State Operation OracleState : Type} {input : List Symbol} [DecidableEq Operation] (machine : MultiTapePTM k Symbol State Operation) (oracle : Operation × List Symbol → StateT OracleState PMF (List Symbol)) (fuel : ℕ) (cfg : MultiTapeMachine.Config k Symbol State Operation input) (s : OracleState) {state : State} (hstate : cfg.tapes.state = some state) {op : Operation} {next : State} (htr : ∀ (bit : Bool), machine.tr state cfg.tapes.inputSymbol cfg.tapes.workTapeSymbols cfg.answerSymbols bit = MultiTapeMachine.Action.query op next) : (Cslib.OracleComp.interpret (Cslib.ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (Cslib.ProbComp.unifOracle n)) oracle) (machine.runOracleConfigFrom (fuel + 1) cfg)).run s = (oracle (op, (cfg.channels op).queryBuffer) s).bind fun (x : List Symbol × OracleState) => match x with | (answer, s') => (Cslib.OracleComp.interpret (Cslib.ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (Cslib.ProbComp.unifOracle n)) oracle) (machine.runOracleConfigFrom fuel (cfg.receive op next answer))).run s'

A live query step whose transition does not depend on the coin bit submits the accumulated query on op and continues from the updated configuration.

def Turing.MultiTapePTM.RunsWords {k : ℕ} {State Operation : Type} [DecidableEq Operation] (machine : MultiTapePTM k Bool State Operation) (x : List Bool) (ws₀ : Fin k → List Bool) (out₀ : List Bool) (time : ℕ) {α : Type} (program : Cslib.ProbOracleComp (fun (x : Operation × List Bool) => List Bool) α) (ws₁ : α → Fin k → List Bool) (emit : α → List Bool) : Prop

Starting from a wordsCfg with empty query buffers, machine halts within time steps with empty query buffers, realizing program on the work tapes and emitted output while preserving the joint distribution with any external oracle state.

def Turing.MultiTapePTM.ComputesTidily {k : ℕ} {State Operation : Type} [DecidableEq Operation] (machine : MultiTapePTM k Bool State Operation) (x : List Bool) (time : ℕ) (program : Cslib.ProbOracleComp (fun (x : Operation × List Bool) => List Bool) (List Bool)) : Prop

A tidy probabilistic oracle computation starts with blank work tapes and empty query buffers, and halts within time steps with blank work tapes, empty query buffers, the input head back at position 1, and program's output appended to the output tape.

theorem Turing.MultiTapePTM.RunsWords.halted {k : ℕ} {State Operation OracleState : Type} [DecidableEq Operation] {machine : MultiTapePTM k Bool State Operation} {x : List Bool} {ws₀ : Fin k → List Bool} {out₀ : List Bool} {time : ℕ} {α : Type} {program : Cslib.ProbOracleComp (fun (x : Operation × List Bool) => List Bool) α} {ws₁ : α → Fin k → List Bool} {emit : α → List Bool} (h : machine.RunsWords x ws₀ out₀ time program ws₁ emit) (oracle : Operation × List Bool → StateT OracleState PMF (List Bool)) (s : OracleState) (cfg : MultiTapeMachine.Config k Bool State Operation x) (htapes : cfg.tapes = wordsCfg x (some machine.initial) ws₀ out₀) (hbuf : ∀ (op : Operation), (cfg.channels op).queryBuffer = []) (final : MultiTapeMachine.Config k Bool State Operation x × OracleState) : final ∈ ((Cslib.OracleComp.interpret (Cslib.ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (Cslib.ProbComp.unifOracle n)) oracle) (machine.runOracleConfigFrom time cfg)).run s).support → final.1.tapes.state = none

Every supported final configuration of a RunsWords phase has halted.

theorem Turing.MultiTapePTM.RunsWords.mem_support {k : ℕ} {State Operation OracleState : Type} [DecidableEq Operation] {machine : MultiTapePTM k Bool State Operation} {x : List Bool} {ws₀ : Fin k → List Bool} {out₀ : List Bool} {time : ℕ} {α : Type} {program : Cslib.ProbOracleComp (fun (x : Operation × List Bool) => List Bool) α} {ws₁ : α → Fin k → List Bool} {emit : α → List Bool} (h : machine.RunsWords x ws₀ out₀ time program ws₁ emit) (oracle : Operation × List Bool → StateT OracleState PMF (List Bool)) (s : OracleState) (cfg : MultiTapeMachine.Config k Bool State Operation x) (htapes : cfg.tapes = wordsCfg x (some machine.initial) ws₀ out₀) (hbuf : ∀ (op : Operation), (cfg.channels op).queryBuffer = []) {final : MultiTapeMachine.Config k Bool State Operation x} {s' : OracleState} (hfinal : (final, s') ∈ ((Cslib.OracleComp.interpret (Cslib.ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (Cslib.ProbComp.unifOracle n)) oracle) (machine.runOracleConfigFrom time cfg)).run s).support) : (∃ (a : α), (a, s') ∈ ((Cslib.OracleComp.interpret (Cslib.ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (Cslib.ProbComp.unifOracle n)) oracle) program).run s).support ∧ final.tapes = wordsCfg x none (ws₁ a) (out₀ ++ emit a)) ∧ ∀ (op : Operation), (final.channels op).queryBuffer = []

Every supported final configuration of a RunsWords phase has the declared tapes and clean query buffers for some supported value of program.

theorem Turing.MultiTapePTM.RunsWords.mono {k : ℕ} {State Operation : Type} [DecidableEq Operation] {machine : MultiTapePTM k Bool State Operation} {x : List Bool} {ws₀ : Fin k → List Bool} {out₀ : List Bool} {time time' : ℕ} {α : Type} {program : Cslib.ProbOracleComp (fun (x : Operation × List Bool) => List Bool) α} {ws₁ : α → Fin k → List Bool} {emit : α → List Bool} (h : machine.RunsWords x ws₀ out₀ time program ws₁ emit) (hle : time ≤ time') : machine.RunsWords x ws₀ out₀ time' program ws₁ emit

Increasing the step budget preserves RunsWords.

theorem Turing.MultiTapePTM.RunsWords.congr {k : ℕ} {State Operation : Type} [DecidableEq Operation] {machine : MultiTapePTM k Bool State Operation} {x : List Bool} {ws₀ : Fin k → List Bool} {out₀ : List Bool} {time : ℕ} {α : Type} {program program' : Cslib.ProbOracleComp (fun (x : Operation × List Bool) => List Bool) α} {ws₁ : α → Fin k → List Bool} {emit : α → List Bool} (h : machine.RunsWords x ws₀ out₀ time program ws₁ emit) (heq : ∀ (OracleState : Type) (oracle : Operation × List Bool → StateT OracleState PMF (List Bool)) (s : OracleState), (Cslib.OracleComp.interpret (Cslib.ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (Cslib.ProbComp.unifOracle n)) oracle) program).run s = (Cslib.OracleComp.interpret (Cslib.ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (Cslib.ProbComp.unifOracle n)) oracle) program').run s) : machine.RunsWords x ws₀ out₀ time program' ws₁ emit

Replace program by a stateful-distributionally equivalent program.

theorem Turing.MultiTapePTM.RunsWords.of_map {k : ℕ} {State Operation : Type} [DecidableEq Operation] {machine : MultiTapePTM k Bool State Operation} {x : List Bool} {ws₀ : Fin k → List Bool} {out₀ : List Bool} {time : ℕ} {α β : Type} {program : Cslib.ProbOracleComp (fun (x : Operation × List Bool) => List Bool) α} (f : α → β) (ws₁' : β → Fin k → List Bool) (emit' : β → List Bool) (h : machine.RunsWords x ws₀ out₀ time program (fun (a : α) => ws₁' (f a)) fun (a : α) => emit' (f a)) : machine.RunsWords x ws₀ out₀ time (f <$> program) ws₁' emit'

Map a function across the program result when the tape and output maps factor through it.

theorem Turing.MultiTapePTM.RunsWords.of_transformsTapes {k : ℕ} {State Operation : Type} [DecidableEq Operation] {x : List Bool} {ws₀ : Fin k → List Bool} {out₀ : List Bool} {tm : MultiTapeTM k Bool State} {P : List Bool → (Fin k → List Bool) → Prop} {Q : List Bool → (Fin k → List Bool) → (Fin k → List Bool) → List Bool → Prop} {t s : ℕ} (htm : tm.TransformsTapes P Q t s) (hP : P x ws₀) {ws' : Fin k → List Bool} {emitted : List Bool} (hQ : ∀ (ws₁ : Fin k → List Bool) (em : List Bool), Q x ws₀ ws₁ em → ws₁ = ws' ∧ em = emitted) : (ofDeterministic tm).RunsWords x ws₀ out₀ t (pure ()) (fun (x : Unit) => ws') fun (x : Unit) => emitted

Lift a deterministic TransformsTapes specification to ofDeterministic.

theorem Turing.MultiTapePTM.RunsWords.seq_bind {k : ℕ} {State₀ State₁ Operation : Type} [DecidableEq Operation] {x : List Bool} {ws₀ : Fin k → List Bool} {out₀ : List Bool} {α β : Type} {first : MultiTapePTM k Bool State₀ Operation} {second : MultiTapePTM k Bool State₁ Operation} {t₁ t₂ : ℕ} {prog₁ : Cslib.ProbOracleComp (fun (x : Operation × List Bool) => List Bool) α} {prog₂ : α → Cslib.ProbOracleComp (fun (x : Operation × List Bool) => List Bool) β} {ws₁ : α → Fin k → List Bool} {emit₁ : α → List Bool} {ws₂ : α → β → Fin k → List Bool} {emit₂ : α → β → List Bool} (hinj : Function.Injective fun (a : α) => (ws₁ a, emit₁ a)) (h₁ : first.RunsWords x ws₀ out₀ t₁ prog₁ ws₁ emit₁) (h₂ : ∀ (a : α) (OracleState : Type) (oracle : Operation × List Bool → StateT OracleState PMF (List Bool)) (s s' : OracleState), (a, s') ∈ ((Cslib.OracleComp.interpret (Cslib.ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (Cslib.ProbComp.unifOracle n)) oracle) prog₁).run s).support → second.RunsWords x (ws₁ a) (out₀ ++ emit₁ a) t₂ (prog₂ a) (ws₂ a) (emit₂ a)) : (first.seq second).RunsWords x ws₀ out₀ (t₁ + t₂) (do let a ← prog₁ (fun (b : β) => (a, b)) <$> prog₂ a) (fun (p : α × β) => ws₂ p.1 p.2) fun (p : α × β) => emit₁ p.1 ++ emit₂ p.1 p.2

Sequence two RunsWords phases when the first phase's resulting tape/output configuration uniquely identifies its program value.

theorem Turing.MultiTapePTM.RunsWords.seq_pure_left {k : ℕ} {State₀ State₁ Operation : Type} [DecidableEq Operation] {x : List Bool} {ws₀ : Fin k → List Bool} {out₀ : List Bool} {β : Type} {first : MultiTapePTM k Bool State₀ Operation} {second : MultiTapePTM k Bool State₁ Operation} {t₁ t₂ : ℕ} {ws₁ : Fin k → List Bool} {emit₁ : List Bool} {prog₂ : Cslib.ProbOracleComp (fun (x : Operation × List Bool) => List Bool) β} {ws₂ : β → Fin k → List Bool} {emit₂ : β → List Bool} (h₁ : first.RunsWords x ws₀ out₀ t₁ (pure ()) (fun (x : Unit) => ws₁) fun (x : Unit) => emit₁) (h₂ : second.RunsWords x ws₁ (out₀ ++ emit₁) t₂ prog₂ ws₂ emit₂) : (first.seq second).RunsWords x ws₀ out₀ (t₁ + t₂) prog₂ ws₂ fun (b : β) => emit₁ ++ emit₂ b

Sequence a deterministic pure () preparation phase before a RunsWords continuation.

theorem Turing.MultiTapePTM.RunsWords.seq_pure_right {k : ℕ} {State₀ State₁ Operation : Type} [DecidableEq Operation] {x : List Bool} {ws₀ : Fin k → List Bool} {out₀ : List Bool} {α : Type} {first : MultiTapePTM k Bool State₀ Operation} {second : MultiTapePTM k Bool State₁ Operation} {t₁ t₂ : ℕ} {prog₁ : Cslib.ProbOracleComp (fun (x : Operation × List Bool) => List Bool) α} {ws₁ : α → Fin k → List Bool} {emit₁ : α → List Bool} {ws₂ : α → Fin k → List Bool} {emit₂ : α → List Bool} (hinj : Function.Injective fun (a : α) => (ws₁ a, emit₁ a)) (h₁ : first.RunsWords x ws₀ out₀ t₁ prog₁ ws₁ emit₁) (h₂ : ∀ (a : α) (OracleState : Type) (oracle : Operation × List Bool → StateT OracleState PMF (List Bool)) (s s' : OracleState), (a, s') ∈ ((Cslib.OracleComp.interpret (Cslib.ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (Cslib.ProbComp.unifOracle n)) oracle) prog₁).run s).support → second.RunsWords x (ws₁ a) (out₀ ++ emit₁ a) t₂ (pure ()) (fun (x : Unit) => ws₂ a) fun (x : Unit) => emit₂ a) : (first.seq second).RunsWords x ws₀ out₀ (t₁ + t₂) prog₁ ws₂ fun (a : α) => emit₁ a ++ emit₂ a

Sequence a deterministic pure () cleanup phase after a RunsWords phase.

theorem Turing.MultiTapePTM.RunsWords.of_nil_output {k : ℕ} {State Operation : Type} [DecidableEq Operation] {machine : MultiTapePTM k Bool State Operation} {x : List Bool} {ws₀ : Fin k → List Bool} {out₀ : List Bool} {time : ℕ} {α : Type} {program : Cslib.ProbOracleComp (fun (x : Operation × List Bool) => List Bool) α} {ws₁ : α → Fin k → List Bool} {emit : α → List Bool} (h : machine.RunsWords x ws₀ [] time program ws₁ emit) : machine.RunsWords x ws₀ out₀ time program ws₁ emit

RunsWords for arbitrary out₀ follows from the out₀ = [] case by output-prefix invariance (runConfigFrom_prependOutput).

theorem Turing.MultiTapePTM.RunsWords.of_first_step_mapState {k : ℕ} {State Operation : Type} [DecidableEq Operation] {machine : MultiTapePTM k Bool State Operation} {x : List Bool} {ws₀ : Fin k → List Bool} {out₀ : List Bool} {time : ℕ} {α : Type} {program : Cslib.ProbOracleComp (fun (x : Operation × List Bool) => List Bool) α} {ws₁ : α → Fin k → List Bool} {emit : α → List Bool} {S : Type} {tm : MultiTapePTM k Bool S Operation} {f : S → State} (hfirst : ∀ (answer : Operation → Option Bool) (bit : Bool), machine.tr machine.initial (wordsCfg x (some machine.initial) ws₀ out₀).inputSymbol (wordsCfg x (some machine.initial) ws₀ out₀).workTapeSymbols answer bit = MultiTapeMachine.Action.step { inputTape := 0, workTapes := fun (x : Fin k) => (none, 0), output := none, state := some (f tm.initial) } (fun (x : Operation) => none) fun (x : Operation) => 0) (htr : ∀ (q : S) (inp : Option Bool) (work : Fin k → Option Bool) (answer : Operation → Option Bool) (bit : Bool), machine.tr (f q) inp work answer bit = MultiTapeMachine.Action.mapState f (tm.tr q inp work answer bit)) (htm : tm.RunsWords x ws₀ out₀ time program ws₁ emit) : machine.RunsWords x ws₀ out₀ (time + 1) program ws₁ emit

If machine's first step from wordsCfg x (some machine.initial) ws₀ out₀ is a deterministic no-op transition into f tm.initial, and machine thereafter simulates tm via f, then any RunsWords specification of tm lifts to machine in time + 1 steps.

theorem Turing.MultiTapePTM.computesTidily_iff_nil_output {k : ℕ} {State Operation : Type} [DecidableEq Operation] {machine : MultiTapePTM k Bool State Operation} {x : List Bool} {time : ℕ} {program : Cslib.ProbOracleComp (fun (x : Operation × List Bool) => List Bool) (List Bool)} : machine.ComputesTidily x time program ↔ machine.RunsWords x (fun (x : Fin k) => []) [] time program (fun (x : List Bool) (x_1 : Fin k) => []) id

ComputesTidily is equivalent to RunsWords with out₀ = [].

theorem Turing.MultiTapePTM.length_output_le_of_mem_support_runOracleConfigFrom {k : ℕ} {State Operation OracleState : Type} [DecidableEq Operation] {x : List Bool} (machine : MultiTapePTM k Bool State Operation) (oracle : Operation × List Bool → StateT OracleState PMF (List Bool)) (fuel : ℕ) (cfg : MultiTapeMachine.Config k Bool State Operation x) (s : OracleState) {final : MultiTapeMachine.Config k Bool State Operation x} {s' : OracleState} (hfinal : (final, s') ∈ ((Cslib.OracleComp.interpret (Cslib.ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (Cslib.ProbComp.unifOracle n)) oracle) (machine.runOracleConfigFrom fuel cfg)).run s).support) : final.tapes.output.length ≤ cfg.tapes.output.length + fuel

Over fuel steps of runOracleConfigFrom, the output tape grows by at most fuel symbols.

theorem Turing.MultiTapePTM.RunsWords.length_emit_le {k : ℕ} {State Operation OracleState : Type} [DecidableEq Operation] {machine : MultiTapePTM k Bool State Operation} {x : List Bool} {ws₀ : Fin k → List Bool} {out₀ : List Bool} {time : ℕ} {α : Type} {program : Cslib.ProbOracleComp (fun (x : Operation × List Bool) => List Bool) α} {ws₁ : α → Fin k → List Bool} {emit : α → List Bool} (h : machine.RunsWords x ws₀ out₀ time program ws₁ emit) (oracle : Operation × List Bool → StateT OracleState PMF (List Bool)) (s : OracleState) {a : α} {s' : OracleState} (ha : (a, s') ∈ ((Cslib.OracleComp.interpret (Cslib.ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (Cslib.ProbComp.unifOracle n)) oracle) program).run s).support) : (emit a).length ≤ time

Any word emitted by a RunsWords phase has length at most time.

theorem Turing.MultiTapePTM.ComputesTidily.mono {k : ℕ} {State Operation : Type} [DecidableEq Operation] {machine : MultiTapePTM k Bool State Operation} {x : List Bool} {time time' : ℕ} {program : Cslib.ProbOracleComp (fun (x : Operation × List Bool) => List Bool) (List Bool)} (h : machine.ComputesTidily x time program) (hle : time ≤ time') : machine.ComputesTidily x time' program

Increasing the step budget preserves ComputesTidily.

theorem Turing.MultiTapePTM.ComputesTidily.congr {k : ℕ} {State Operation : Type} [DecidableEq Operation] {machine : MultiTapePTM k Bool State Operation} {x : List Bool} {time : ℕ} {program program' : Cslib.ProbOracleComp (fun (x : Operation × List Bool) => List Bool) (List Bool)} (h : machine.ComputesTidily x time program) (heq : ∀ (OracleState : Type) (oracle : Operation × List Bool → StateT OracleState PMF (List Bool)) (s : OracleState), (Cslib.OracleComp.interpret (Cslib.ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (Cslib.ProbComp.unifOracle n)) oracle) program).run s = (Cslib.OracleComp.interpret (Cslib.ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (Cslib.ProbComp.unifOracle n)) oracle) program').run s) : machine.ComputesTidily x time program'

Replace program by a stateful-distributionally equivalent program.

theorem Turing.MultiTapePTM.ComputesTidily.runOracle {k : ℕ} {State Operation OracleState : Type} [DecidableEq Operation] {machine : MultiTapePTM k Bool State Operation} {x : List Bool} {time : ℕ} {program : Cslib.ProbOracleComp (fun (x : Operation × List Bool) => List Bool) (List Bool)} (h : machine.ComputesTidily x time program) (oracle : Operation × List Bool → StateT OracleState PMF (List Bool)) (s : OracleState) : (Cslib.OracleComp.interpret (Cslib.ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (Cslib.ProbComp.unifOracle n)) oracle) (machine.runOracle time x)).run s = (Cslib.OracleComp.interpret (Cslib.ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (Cslib.ProbComp.unifOracle n)) oracle) program).run s

A tidy machine realizes program under runOracle from initialConfig.

theorem Turing.MultiTapePTM.ComputesTidily.of_deterministic {k : ℕ} {State Operation : Type} [DecidableEq Operation] {x : List Bool} {tm : MultiTapeTM k Bool State} {output : List Bool} {t s : ℕ} (htm : tm.ComputesTidilyInTimeAndSpace x output t s) : (ofDeterministic tm).ComputesTidily x t (pure output)

A deterministic tidy machine lifts directly to ComputesTidily via ofDeterministic.

theorem Turing.MultiTapePTM.ComputesTidily.length_output_le {k : ℕ} {State Operation OracleState : Type} [DecidableEq Operation] {machine : MultiTapePTM k Bool State Operation} {x : List Bool} {time : ℕ} {program : Cslib.ProbOracleComp (fun (x : Operation × List Bool) => List Bool) (List Bool)} (h : machine.ComputesTidily x time program) (oracle : Operation × List Bool → StateT OracleState PMF (List Bool)) (s : OracleState) {w : List Bool} {s' : OracleState} (hw : (w, s') ∈ ((Cslib.OracleComp.interpret (Cslib.ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (Cslib.ProbComp.unifOracle n)) oracle) program).run s).support) : w.length ≤ time

Any supported output of a ComputesTidily machine has length at most time.