Sequencing fair-coin machines

Sampling a coin commutes with mapping the selected action. Thus the common machine sequencing theorem applies directly, without an additional probabilistic compiler or interpreter. The coin program is explicit: the result also applies to stateful, nonuniform coin sources.

Main definitions

• Turing.MultiTapePTM.seq: the common compiler specialized to Boolean-indexed transitions.

Main results

• Turing.MultiTapePTM.run_interpret_runConfigFrom_seq: two halting bounds add while preserving the whole joint distribution of configuration and private interpreter state.

References

The common proof in MultiTape.Machine.Sequential adapts the cslib crypto branch's MultiTape/Oracle/Sequential.lean at 5ff69ca93402e7c947208dc56396d6d86203ccd8.

@[reducible, inline]

abbrev Turing.MultiTapePTM.seq {k : ℕ} {Symbol State₀ State₁ Oracle : Type} (first : MultiTapePTM k Symbol State₀ Oracle) (second : MultiTapePTM k Symbol State₁ Oracle) : MultiTapePTM k Symbol (State₀ ⊕ State₁) Oracle

The common sequential compiler specialized to Boolean-indexed transitions.

theorem Turing.MultiTapePTM.run_interpret_runConfigFrom_seq {k : ℕ} {Symbol State₀ State₁ Oracle Query OracleState : Type} {spec : Cslib.OracleSpec Query} {input : List Symbol} [DecidableEq Oracle] (first : MultiTapePTM k Symbol State₀ Oracle) (second : MultiTapePTM k Symbol State₁ Oracle) (coin : Cslib.OracleComp spec Bool) (query : Oracle → List Symbol → Cslib.OracleComp spec (List Symbol)) (oracle : (q : Query) → StateT OracleState PMF (spec q)) (cfg : MultiTapeMachine.Config k Symbol State₀ Oracle input) (firstTime secondTime : ℕ) (s : OracleState) (hfirst : ∀ result ∈ ((Cslib.OracleComp.interpret oracle (first.runConfigFrom coin query firstTime cfg)).run s).support, result.1.tapes.state = none) (hsecond : ∀ result ∈ ((Cslib.OracleComp.interpret oracle (first.runConfigFrom coin query firstTime cfg)).run s).support, ∀ final ∈ ((Cslib.OracleComp.interpret oracle (second.runConfigFrom coin query secondTime (MultiTapeMachine.Sequential.start second result.1))).run result.2).support, final.1.tapes.state = none) : (Cslib.OracleComp.interpret oracle ((first.seq second).runConfigFrom coin query (firstTime + secondTime) (MultiTapeMachine.Sequential.left second cfg))).run s = ((Cslib.OracleComp.interpret oracle (first.runConfigFrom coin query firstTime cfg)).run s).bind fun (result : MultiTapeMachine.Config k Symbol State₀ Oracle input × OracleState) => PMF.map (fun (x : MultiTapeMachine.Config k Symbol State₁ Oracle input × OracleState) => match x with | (final, s') => (MultiTapeMachine.Sequential.right final, s')) ((Cslib.OracleComp.interpret oracle (second.runConfigFrom coin query secondTime (MultiTapeMachine.Sequential.start second result.1))).run result.2)

Sequencing retains every tape and private state, even for random stopping times. Both phases must actually halt within their bounds; clock exhaustion alone is insufficient.