Reserving work tapes for effectful machines

Reindexing the source's tapes leaves every additional tape and head unchanged. The construction uses upstream's configuration embedding and preserves the entire typed execution program, hence also the joint distribution of configuration and private interpreter state. It requires only that the choice interpreter commute with mapping; coin draws may be stateful.

Main definitions

• Turing.MultiTapeMachine.extendTapes: run on tapes selected by an embedding.
• Turing.MultiTapeMachine.Config.embed: retain arbitrary data on the additional tapes.

Main results

• Turing.MultiTapeMachine.runConfigFrom_embed: reindexing preserves the full clocked program.
• Turing.MultiTapeMachine.toTM_extendTapes: agreement with upstream's deterministic compiler.

References

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

def Turing.MultiTapeMachine.extendAction {k k' : ℕ} {Symbol State : Type} (action : Turing.Action k Symbol State) (e : Fin k ↪ Fin k') : Turing.Action k' Symbol State

Reindex a tape action, leaving every additional tape and head untouched.

def Turing.MultiTapeMachine.Action.extendTapes {k k' : ℕ} {Symbol State Oracle : Type} (e : Fin k ↪ Fin k') : Action k Symbol State Oracle → Action k' Symbol State Oracle

Reindex ordinary tapes while retaining communication instructions verbatim.

def Turing.MultiTapeMachine.extendTapes {k k' : ℕ} {Symbol State Oracle : Type} {Choose : Type → Type v} [Functor Choose] (machine : MultiTapeMachine k Symbol State Oracle Choose) (e : Fin k ↪ Fin k') : MultiTapeMachine k' Symbol State Oracle Choose

Run on the tapes selected by e, preserving all other tapes and every oracle interaction.

@[simp]

theorem Turing.MultiTapeMachine.extendTapes_initial {k k' : ℕ} {Symbol State Oracle : Type} {Choose : Type → Type v} [Functor Choose] (machine : MultiTapeMachine k Symbol State Oracle Choose) (e : Fin k ↪ Fin k') : (machine.extendTapes e).initial = machine.initial

theorem Turing.MultiTapeMachine.extendTapes_tr {k k' : ℕ} {Symbol State Oracle : Type} {Choose : Type → Type v} [Functor Choose] (machine : MultiTapeMachine k Symbol State Oracle Choose) (e : Fin k ↪ Fin k') (state : State) (symbol : Option Symbol) (work : Fin k' → Option Symbol) (answer : Oracle → Option Symbol) : (machine.extendTapes e).tr state symbol work answer = Action.extendTapes e <$> machine.tr state symbol (fun (i : Fin k) => work (e i)) answer

Unfold a reindexed transition without unfolding its machine in a recursive continuation.

def Turing.MultiTapeMachine.Config.embed {k k' : ℕ} {Symbol State Oracle : Type} {input : List Symbol} (cfg : Config k Symbol State Oracle input) (e : Fin k ↪ Fin k') (extraTapes : Fin k' → ℤ → Option Symbol) (extraPos : Fin k' → ℤ) : Config k' Symbol State Oracle input

A source configuration with arbitrary contents and head positions on additional tapes.

@[simp]

theorem Turing.MultiTapeMachine.Config.embed_state {k k' : ℕ} {Symbol State Oracle : Type} {input : List Symbol} (cfg : Config k Symbol State Oracle input) (e : Fin k ↪ Fin k') (extraTapes : Fin k' → ℤ → Option Symbol) (extraPos : Fin k' → ℤ) : (cfg.embed e extraTapes extraPos).tapes.state = cfg.tapes.state

@[simp]

theorem Turing.MultiTapeMachine.Config.embed_inputSymbol {k k' : ℕ} {Symbol State Oracle : Type} {input : List Symbol} (cfg : Config k Symbol State Oracle input) (e : Fin k ↪ Fin k') (extraTapes : Fin k' → ℤ → Option Symbol) (extraPos : Fin k' → ℤ) : (cfg.embed e extraTapes extraPos).tapes.inputSymbol = cfg.tapes.inputSymbol

@[simp]

theorem Turing.MultiTapeMachine.Config.embed_workTapeSymbols {k k' : ℕ} {Symbol State Oracle : Type} {input : List Symbol} (cfg : Config k Symbol State Oracle input) (e : Fin k ↪ Fin k') (extraTapes : Fin k' → ℤ → Option Symbol) (extraPos : Fin k' → ℤ) (i : Fin k) : (cfg.embed e extraTapes extraPos).tapes.workTapeSymbols (e i) = cfg.tapes.workTapeSymbols i

@[simp]

theorem Turing.MultiTapeMachine.Config.embed_channels {k k' : ℕ} {Symbol State Oracle : Type} {input : List Symbol} (cfg : Config k Symbol State Oracle input) (e : Fin k ↪ Fin k') (extraTapes : Fin k' → ℤ → Option Symbol) (extraPos : Fin k' → ℤ) : (cfg.embed e extraTapes extraPos).channels = cfg.channels

@[simp]

theorem Turing.MultiTapeMachine.Config.embed_answerSymbols {k k' : ℕ} {Symbol State Oracle : Type} {input : List Symbol} (cfg : Config k Symbol State Oracle input) (e : Fin k ↪ Fin k') (extraTapes : Fin k' → ℤ → Option Symbol) (extraPos : Fin k' → ℤ) : (cfg.embed e extraTapes extraPos).answerSymbols = cfg.answerSymbols

@[simp]

theorem Turing.MultiTapeMachine.Config.embed_output {k k' : ℕ} {Symbol State Oracle : Type} {input : List Symbol} (cfg : Config k Symbol State Oracle input) (e : Fin k ↪ Fin k') (extraTapes : Fin k' → ℤ → Option Symbol) (extraPos : Fin k' → ℤ) : (cfg.embed e extraTapes extraPos).tapes.output = cfg.tapes.output

theorem Turing.MultiTapeMachine.Config.step_embed {k k' : ℕ} {Symbol State Oracle : Type} {input : List Symbol} (cfg : Config k Symbol State Oracle input) (e : Fin k ↪ Fin k') (extraTapes : Fin k' → ℤ → Option Symbol) (extraPos : Fin k' → ℤ) (action : Turing.Action k Symbol State) (symbol : Oracle → Option Symbol) (move : Oracle → SignType) : (cfg.embed e extraTapes extraPos).step (extendAction action e) symbol move = (cfg.step action symbol move).embed e extraTapes extraPos

theorem Turing.MultiTapeMachine.Config.receive_embed {k k' : ℕ} {Symbol State Oracle : Type} {input : List Symbol} [DecidableEq Oracle] (cfg : Config k Symbol State Oracle input) (e : Fin k ↪ Fin k') (extraTapes : Fin k' → ℤ → Option Symbol) (extraPos : Fin k' → ℤ) (oracle : Oracle) (next : State) (answer : List Symbol) : (cfg.embed e extraTapes extraPos).receive oracle next answer = (cfg.receive oracle next answer).embed e extraTapes extraPos

theorem Turing.MultiTapeMachine.runConfigFrom_embed {k k' : ℕ} {Symbol State Oracle : Type} {Query : Type u} {Choose : Type → Type v} {spec : Cslib.OracleSpec Query} {input : List Symbol} [Functor Choose] [DecidableEq Oracle] (machine : MultiTapeMachine k Symbol State Oracle Choose) (e : Fin k ↪ Fin k') (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) (extraTapes : Fin k' → ℤ → Option Symbol) (extraPos : Fin k' → ℤ) (fuel : ℕ) : (machine.extendTapes e).runConfigFrom choose query fuel (cfg.embed e extraTapes extraPos) = (fun (final : Config k Symbol State Oracle input) => final.embed e extraTapes extraPos) <$> machine.runConfigFrom choose query fuel cfg

Reindexing preserves the entire program, including all unused tape contents and heads.

theorem Turing.MultiTapeMachine.runFrom_embed {k k' : ℕ} {Symbol State Oracle : Type} {Query : Type u} {Choose : Type → Type v} {spec : Cslib.OracleSpec Query} {input : List Symbol} [Functor Choose] [DecidableEq Oracle] (machine : MultiTapeMachine k Symbol State Oracle Choose) (e : Fin k ↪ Fin k') (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) (extraTapes : Fin k' → ℤ → Option Symbol) (extraPos : Fin k' → ℤ) (fuel : ℕ) : (machine.extendTapes e).runFrom choose query fuel (cfg.embed e extraTapes extraPos) = machine.runFrom choose query fuel cfg

The additional work tapes do not affect the observable output program.

theorem Turing.MultiTapeMachine.initialConfig_extendTapes {k k' : ℕ} {Symbol State Oracle : Type} {Choose : Type → Type v} [Functor Choose] (machine : MultiTapeMachine k Symbol State Oracle Choose) (e : Fin k ↪ Fin k') (input : List Symbol) : (machine.extendTapes e).initialConfig input = (machine.initialConfig input).embed e (fun (x : Fin k') (x_1 : ℤ) => none) fun (x : Fin k') => 0

Reserving additional tapes starts them blank, with every work head at zero.

theorem Turing.MultiTapeMachine.run_extendTapes {k k' : ℕ} {Symbol State Oracle : Type} {Query : Type u} {Choose : Type → Type v} {spec : Cslib.OracleSpec Query} [Functor Choose] [DecidableEq Oracle] (machine : MultiTapeMachine k Symbol State Oracle Choose) (e : Fin k ↪ Fin k') (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 : ℕ) (input : List Symbol) : (machine.extendTapes e).run choose query fuel input = machine.run choose query fuel input

Reserving blank scratch tapes preserves the clocked output program.

theorem Turing.MultiTapeMachine.HaltsWithin.extendTapes {k k' : ℕ} {Symbol State Oracle : Type} {Query : Type u} {Choose : Type → Type v} {spec : Cslib.OracleSpec Query} [Functor Choose] [DecidableEq Oracle] (machine : MultiTapeMachine k Symbol State Oracle Choose) (e : Fin k ↪ Fin k') (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 : ℕ} {input : List Symbol} (h : machine.HaltsWithin choose query fuel input) : (machine.extendTapes e).HaltsWithin choose query fuel input

Tape extension preserves a halting bound against every stateful interpreter.

theorem Turing.MultiTapeMachine.toTM_extendTapes {k k' : ℕ} {Symbol State : Type} (e : Fin k ↪ Fin k') (machine : MultiTapeMachine k Symbol State Empty Id) : (machine.extendTapes e).toTM = machine.toTM.extendTapes e

In the effect-free deterministic case, tape extension is exactly upstream's compiler.