Sequencing effectful machines

The first machine's halting transition transfers control to the second, retaining every tape and communication channel. The transition-choice mechanism only needs to support mapping its actions. Execution commutes with this mapping when the choice interpreter does; in particular, deterministic choices and sampling a supplied coin have this property.

Two actual halting bounds add even when stopping times depend on random choices or oracle answers. The distributional theorem retains the final configuration and private interpreter state. This is sequencing on shared tapes: supplying fresh encoded input and clean communication state is a separate obligation of a higher-level composition compiler.

Main definitions

• Turing.MultiTapeMachine.seq: sequential composition, with no extra handoff instruction.

Main results

• Turing.MultiTapeMachine.Sequential.runConfigFrom_right: after handoff the continuation's complete program is unchanged, up to embedding its control states.
• Turing.MultiTapeMachine.run_interpret_runConfigFrom_seq: the joint distribution of a sequential run is the monadic composition of the two phases.
• Turing.MultiTapeMachine.interpret_runConfigFrom_seq_list: exact List bind, including repeated equal configurations, under the two phase halting bounds.
• Turing.MultiTapeMachine.toTM_seq: the deterministic compiler is exactly upstream's seq.

References

Adapted from MultiTape/Oracle/Sequential.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8 to the common machine and typed program interface.

def Turing.MultiTapeMachine.Sequential.leftAction {k : ℕ} {Symbol State₀ State₁ Oracle : Type} (next : State₁) : Action k Symbol State₀ Oracle → Action k Symbol (State₀ ⊕ State₁) Oracle

Embed a first-phase action, transferring a halt directly to the continuation.

def Turing.MultiTapeMachine.Sequential.rightAction {k : ℕ} {Symbol State₀ State₁ Oracle : Type} : Action k Symbol State₁ Oracle → Action k Symbol (State₀ ⊕ State₁) Oracle

Embed a continuation's action, preserving halting.

def Turing.MultiTapeMachine.Sequential.left {k : ℕ} {Symbol State₀ State₁ Oracle : Type} {Choose : Type → Type v} {input : List Symbol} (second : MultiTapeMachine k Symbol State₁ Oracle Choose) (cfg : Config k Symbol State₀ Oracle input) : Config k Symbol (State₀ ⊕ State₁) Oracle input

Embed the first phase, dispatching its halt to the continuation's initial state.

def Turing.MultiTapeMachine.Sequential.start {k : ℕ} {Symbol State₀ State₁ Oracle : Type} {Choose : Type → Type v} {input : List Symbol} (second : MultiTapeMachine k Symbol State₁ Oracle Choose) (cfg : Config k Symbol State₀ Oracle input) : Config k Symbol State₁ Oracle input

Start the continuation on the complete tape and communication state left by the first phase.

def Turing.MultiTapeMachine.Sequential.right {k : ℕ} {Symbol State₀ State₁ Oracle : Type} {input : List Symbol} (cfg : Config k Symbol State₁ Oracle input) : Config k Symbol (State₀ ⊕ State₁) Oracle input

Embed a continuation's configuration, preserving halting and every tape.

theorem Turing.MultiTapeMachine.Sequential.left_halted {k : ℕ} {Symbol State₀ State₁ Oracle : Type} {Choose : Type → Type v} {input : List Symbol} (second : MultiTapeMachine k Symbol State₁ Oracle Choose) (cfg : Config k Symbol State₀ Oracle input) (h : cfg.tapes.state = none) : left second cfg = right (start second cfg)

def Turing.MultiTapeMachine.seq {k : ℕ} {Symbol State₀ State₁ Oracle : Type} {Choose : Type → Type v} [Functor Choose] (first : MultiTapeMachine k Symbol State₀ Oracle Choose) (second : MultiTapeMachine k Symbol State₁ Oracle Choose) : MultiTapeMachine k Symbol (State₀ ⊕ State₁) Oracle Choose

Transfer control when the first machine halts, retaining all tapes and oracle channels.

@[simp]

theorem Turing.MultiTapeMachine.seq_initial {k : ℕ} {Symbol State₀ State₁ Oracle : Type} {Choose : Type → Type v} [Functor Choose] (first : MultiTapeMachine k Symbol State₀ Oracle Choose) (second : MultiTapeMachine k Symbol State₁ Oracle Choose) : (first.seq second).initial = Sum.inl first.initial

theorem Turing.MultiTapeMachine.Sequential.runConfigFrom_one {k : ℕ} {Symbol State₀ State₁ Oracle : Type} {Query : Type u} {Choose : Type → Type v} {spec : Cslib.OracleSpec Query} {input : List Symbol} [Functor Choose] [DecidableEq Oracle] (first : MultiTapeMachine k Symbol State₀ Oracle Choose) (second : MultiTapeMachine k Symbol State₁ Oracle Choose) (choose : {α : Type} → Choose α → Cslib.OracleComp spec α) (hchoose : ∀ {α β : Type} (f : α → β) (choices : Choose α), choose (f <$> choices) = f <$> choose choices) (query : Oracle → List Symbol → Cslib.OracleComp spec (List Symbol)) (cfg : Config k Symbol State₀ Oracle input) (h : cfg.tapes.state ≠ none) : (first.seq second).runConfigFrom choose query 1 (left second cfg) = left second <$> first.runConfigFrom choose query 1 cfg

While the first phase is active, one instruction mirrors its complete program.

theorem Turing.MultiTapeMachine.Sequential.runConfigFrom_right {k : ℕ} {Symbol State₀ State₁ Oracle : Type} {Query : Type u} {Choose : Type → Type v} {spec : Cslib.OracleSpec Query} {input : List Symbol} [Functor Choose] [DecidableEq Oracle] (first : MultiTapeMachine k Symbol State₀ Oracle Choose) (second : MultiTapeMachine k Symbol State₁ Oracle Choose) (choose : {α : Type} → Choose α → Cslib.OracleComp spec α) (hchoose : ∀ {α β : Type} (f : α → β) (choices : Choose α), choose (f <$> choices) = f <$> choose choices) (query : Oracle → List Symbol → Cslib.OracleComp spec (List Symbol)) (fuel : ℕ) (cfg : Config k Symbol State₁ Oracle input) : (first.seq second).runConfigFrom choose query fuel (right cfg) = right <$> second.runConfigFrom choose query fuel cfg

After handoff, the continuation runs its unchanged program in right states.

theorem Turing.MultiTapeMachine.toTM_seq {k : ℕ} {Symbol State₀ State₁ : Type} (first : MultiTapeMachine k Symbol State₀ Empty Id) (second : MultiTapeMachine k Symbol State₁ Empty Id) : (first.seq second).toTM = first.toTM.seq second.toTM

In the deterministic effect-free case, this is exactly upstream's sequential compiler.

theorem Turing.MultiTapeMachine.interpret_runConfigFrom_seq_list {k : ℕ} {Symbol State₀ State₁ Oracle : Type} {Query : Type u} {Choose : Type → Type v} {spec : Cslib.OracleSpec Query} {input : List Symbol} [Functor Choose] [DecidableEq Oracle] (first : MultiTapeMachine k Symbol State₀ Oracle Choose) (second : MultiTapeMachine k Symbol State₁ Oracle Choose) (choose : {α : Type} → Choose α → Cslib.OracleComp spec α) (hchoose : ∀ {α β : Type} (f : α → β) (choices : Choose α), choose (f <$> choices) = f <$> choose choices) (query : Oracle → List Symbol → Cslib.OracleComp spec (List Symbol)) (oracle : (q : Query) → List (spec q)) (cfg : Config k Symbol State₀ Oracle input) (firstTime secondTime : ℕ) (hfirst : ∀ result ∈ Cslib.OracleComp.interpret oracle (first.runConfigFrom choose query firstTime cfg), result.tapes.state = none) (hsecond : ∀ result ∈ Cslib.OracleComp.interpret oracle (first.runConfigFrom choose query firstTime cfg), ∀ final ∈ Cslib.OracleComp.interpret oracle (second.runConfigFrom choose query secondTime (Sequential.start second result)), final.tapes.state = none) : Cslib.OracleComp.interpret oracle ((first.seq second).runConfigFrom choose query (firstTime + secondTime) (Sequential.left second cfg)) = List.flatMap (fun (result : Config k Symbol State₀ Oracle input) => List.map Sequential.right (Cslib.OracleComp.interpret oracle (second.runConfigFrom choose query secondTime (Sequential.start second result)))) (Cslib.OracleComp.interpret oracle (first.runConfigFrom choose query firstTime cfg))

List interpretation of sequencing is exact list bind, retaining repeated equal endpoints. The phase bounds are actual halting bounds. Excluding stuck branches is a separate obligation, since an empty interpreted choice has no endpoints.

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

Sequential halting bounds add even when the first stopping time depends on random choices. The equality retains the final configuration and the interpreter's private state.

theorem Turing.MultiTapeMachine.run_interpret_runConfigFrom_seq_pure {k : ℕ} {Symbol State₀ State₁ Oracle : Type} {Query : Type u} {Choose : Type → Type v} {spec : Cslib.OracleSpec Query} {input : List Symbol} [Functor Choose] [DecidableEq Oracle] (first : MultiTapeMachine k Symbol State₀ Oracle Choose) (second : MultiTapeMachine k Symbol State₁ Oracle Choose) (choose : {α : Type} → Choose α → Cslib.OracleComp spec α) (hchoose : ∀ {α β : Type} (f : α → β) (choices : Choose α), choose (f <$> choices) = f <$> choose choices) (query : Oracle → List Symbol → Cslib.OracleComp spec (List Symbol)) {OracleState : Type} (oracle : (q : Query) → StateT OracleState PMF (spec q)) (cfg ready : Config k Symbol State₀ Oracle input) (firstTime secondTime : ℕ) (s : OracleState) (hfirst : (Cslib.OracleComp.interpret oracle (first.runConfigFrom choose query firstTime cfg)).run s = PMF.pure (ready, s)) (hready : ready.tapes.state = none) (hsecond : ∀ final ∈ ((Cslib.OracleComp.interpret oracle (second.runConfigFrom choose query secondTime (Sequential.start second ready))).run s).support, final.1.tapes.state = none) : (Cslib.OracleComp.interpret oracle ((first.seq second).runConfigFrom choose query (firstTime + secondTime) (Sequential.left second cfg))).run s = PMF.map (fun (x : Config k Symbol State₁ Oracle input × OracleState) => match x with | (final, s') => (Sequential.right final, s')) ((Cslib.OracleComp.interpret oracle (second.runConfigFrom choose query secondTime (Sequential.start second ready))).run s)

A deterministic preparation phase hands its exact restored configuration to the continuation.

theorem Turing.MultiTapeMachine.run_interpret_runFrom_seq {k : ℕ} {Symbol State₀ State₁ Oracle : Type} {Query : Type u} {Choose : Type → Type v} {spec : Cslib.OracleSpec Query} {input : List Symbol} [Functor Choose] [DecidableEq Oracle] (first : MultiTapeMachine k Symbol State₀ Oracle Choose) (second : MultiTapeMachine k Symbol State₁ Oracle Choose) (choose : {α : Type} → Choose α → Cslib.OracleComp spec α) (hchoose : ∀ {α β : Type} (f : α → β) (choices : Choose α), choose (f <$> choices) = f <$> choose choices) (query : Oracle → List Symbol → Cslib.OracleComp spec (List Symbol)) {OracleState : Type} (oracle : (q : Query) → StateT OracleState PMF (spec q)) (cfg : Config k Symbol State₀ Oracle input) (firstTime secondTime : ℕ) (s : OracleState) (hfirst : ∀ result ∈ ((Cslib.OracleComp.interpret oracle (first.runConfigFrom choose query firstTime cfg)).run s).support, result.1.tapes.state = none) (hsecond : ∀ result ∈ ((Cslib.OracleComp.interpret oracle (first.runConfigFrom choose query firstTime cfg)).run s).support, ∀ final ∈ ((Cslib.OracleComp.interpret oracle (second.runConfigFrom choose query secondTime (Sequential.start second result.1))).run result.2).support, final.1.tapes.state = none) : (Cslib.OracleComp.interpret oracle ((first.seq second).runFrom choose query (firstTime + secondTime) (Sequential.left second cfg))).run s = ((Cslib.OracleComp.interpret oracle (first.runConfigFrom choose query firstTime cfg)).run s).bind fun (result : Config k Symbol State₀ Oracle input × OracleState) => (Cslib.OracleComp.interpret oracle (second.runFrom choose query secondTime (Sequential.start second result.1))).run result.2

Observing only the output gives the usual monadic sequencing law under the same bounds.